Issue No. 04 - April (1976 vol. 25)
D. Gelperin , National Car Rental
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. Distribution, a new clause deletion rule which is fundamental to the operation of the search strategy, is also described.
Automatic theorem proving, clause deletion, deletion-directed search, formal logic, heuristic search, mate tables, resolution.
D. Gelperin, "A Resolution-Based Proof Procedure Using Deletion-Directed Search," in IEEE Transactions on Computers, vol. 25, no. , pp. 323-327, 1976.