MECHANIZED REASONING

We will define the notions of abstract theorem-proving graph, abstract theorem-proving problem g and search strategy E for g. These concepts generalize the usual tree (or graph) searching problem and admit Hart, Nilsson and Raphael (1968) and Pohl (1969) theories of heuristic search. In particular the admissibility and optimality theorems of Hart, Nilsson and Raphael generalize for the classes 0 and 0" of diagonal search strategies for abstract theorem-proving problems. In addition the subclass au of 0 is shown to be optimal for 2. Implementation of diagonal search is treated in some detail for theorem-proving by resolution rules (Robinson 1965). SEARCH STRATEGIES, COMPLETENESS AND EFFICIENCY Completeness and efficiency of proof procedures can be studied only in the context of search strategies. A system T of inference rules and axioms can be complete or incomplete for a given class of intended interpretations. Similarly a search strategy E for T may or may not be complete for ...