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
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.
91 ms
(Ver 3.3 (11022016))