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", IEEE Transactions on Computers, vol.25, no. 4, pp. 323-327, April 1976, doi:10.1109/TC.1976.1674612