---
title: "Deletion-Directed Search in Resolution-Based Proof Procedures"
authors:
  - "David Gelperin"
doi: ""
url: "https://ijcai.org/proceedings/1973/7"
pdf: "https://ijcai.org/proceedings/1973/0007.pdf"
venue: "Proceedings of the Third International Joint Conference on Artificial Intelligence"
year: 1973
pages: "47-49"
track: "Theorem Proving and Logic: 1"
keywords:
---

# Deletion-Directed Search in Resolution-Based Proof Procedures

David Gelperin

*Proceedings of the Third International Joint Conference on Artificial Intelligence*, pages 47-49.

## Abstract

The operation of a deletion-directed search strategy for resolution-based proof procedures is discussed. The strategy attempts to determine the satisfiability of a set of input clauses while at the same time minimizing the cardinality of the s·et of retained clauses. E-representation, a new clause deletion rule which is fundamental to the operation of the search strategy, is also described.