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.;
