The Community for Technology Leaders
Green Image
Issue No. 04 - April (1976 vol. 25)
ISSN: 0018-9340
pp: 323-327
D. Gelperin , National Car Rental
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 set of retained clauses. Distribution, a new clause deletion rule which is fundamental to the operation of the search strategy, is also described.
INDEX TERMS
Automatic theorem proving, clause deletion, deletion-directed search, formal logic, heuristic search, mate tables, resolution.
CITATION
D. Gelperin, "A Resolution-Based Proof Procedure Using Deletion-Directed Search", IEEE Transactions on Computers, vol. 25, no. , pp. 323-327, April 1976, doi:10.1109/TC.1976.1674612
176 ms
(Ver 3.3 (11022016))