Operational issues in automated theorem proving using matings
Sunil Issar · 1991
Much research in automated theorem proving has focused on improving the efficiency of procedures based on Robinson's resolution principle. The mating paradigm for automated theorem provers was proposed by Andrews and a similar approach called the connection method was suggested by Bibel to avoid converting a well-formed formula (wff) to clause form, which introduces redundancy and impedes analysis of the logical structure of the wff. In this thesis, we address various operational issues that arise in implementations of mating search and discuss techniques for improving the performance of mating search when searching for a refutation of a wff of first-order logic; for example, we address two crucial issues that arise in the search for refutations and are inadequately handled in current implementations: when and how to expand the search space. Two of these techniques--path-focused duplication and path enumeration--that have been implemented significantly improve the performance of search for refutations in TPS. Some other of these strategies significantly improve the performance of a propositional calculus prover that is based on the mating method; In fact, our performance on the pigeon hole problems is comparable to that of the best provers in the field. All our techniques are applicable to any wff W of first-order logic; we neither assume that W is in conjunctive normal form nor convert W to conjunctive normal form. We also discuss modifications of the unification algorithms that ensure the acyclicity of the imbedding relation, which provides an alternative to Skolemization. We incorporate the essential ideas of Cox's work on intelligent backtracking into mating search. This is a non trivial task, since an effective strategy must also efficiently handle the dynamically growing and shrinking search space introduced by path-focused duplication. Murray and Rosenthal introduced path dissolution inference rule, which removes unsatisfiable paths from a wff and is strongly complete. In this thesis, we provide an alternate characterization of this rule, which simplifies a criterion that determines the applicability of path-dissolution as well as the exposition of the path-dissolution inference rule.