Theorem Proving via General Matings

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.