This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
April 1976 (vol. 25 no. 4)
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.
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. 4, pp. 323-327, April 1976, doi:10.1109/TC.1976.1674612
Usage of this product signifies your acceptance of the Terms of Use.