DocumentCode
1132337
Title
A Resolution-Based Proof Procedure Using Deletion-Directed Search
Author
Gelperin, David
Author_Institution
National Car Rental
Issue
4
fYear
1976
fDate
4/1/1976 12:00:00 AM
Firstpage
323
Lastpage
327
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.
Keywords
Automatic theorem proving, clause deletion, deletion-directed search, formal logic, heuristic search, mate tables, resolution.; Inspection; Logic; Robots; Terminology; Turning; Automatic theorem proving, clause deletion, deletion-directed search, formal logic, heuristic search, mate tables, resolution.;
fLanguage
English
Journal_Title
Computers, IEEE Transactions on
Publisher
ieee
ISSN
0018-9340
Type
jour
DOI
10.1109/TC.1976.1674612
Filename
1674612
Link To Document