Theorem Proving via General Matings

Abstract

An approach to automaUc theorem proving using matmgs of arbitrary sentences is discussed No use is made of conjunctive normal form (clauses) or prenex normal form, since these forms tend to introduce superfluous redundancy, complicate the search for a proof, and impede analysis of the essential logical structure of the proposed theorem. A complete exposition of the logical foundations of theorem proving via general matmgs is given, starting with proofs of appropriate versions of Herbrand's Theorem. It is shown that one may restrict quantifier duphcat,on to outermost quanUfiers without loss of completeness, though with possible loss of efficmncy. General matmgs could be used as the basis for a variety of theorem-proving procedures, and there are many opportunmes for research m this area. A procedure using the criterion of path acceptability for mattngs is discussed. This criterion is easily VlSUahzed m terms of a two-dimensional format for formulas. An implementation by Eve Cohen has yielded encouraging preliminary results. Some implementation issues are discussed. © 1981, ACM. All rights reserved.