Deletion-directed search in resolution-based proof procedures
David Gelperin · International Joint Conference on Artificial Intelligence · 1973
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 set of retained clauses. E-representation, a new clause deletion rule which is fundamental to the operation of the search strategy, is also described.