Paper: Theorem Proving Using Rigid E-Unification Equational Matings (at LICS 1987)

Authors: Jean H. Gallier Stan Raatz Wayne Snyder

Abstract

In this paper we show that the method of matings due Andrews [1], can be extended to (first-order) languages with equality, and prove that this extension is both sound and complete. Recall that the method of matings applies to formulae in negation normal form, and that it was introduced with two motivations in mind: to avoid breaking a formula into parts, which can result in loss of information about the global structure, and to avoid transforming it to clausal form, which can result in an exponential increase in the number of literals due to the repeated use of the distributive law (P ∨ (Q ∧ R)) ≡ (( P ∨ Q ) ∧ (P ∨R)).

BibTeX

  @InProceedings{GallierRaatzSnyder-TheoremProvingUsing,
    author = 	 {Jean H. Gallier and Stan Raatz and Wayne Snyder},
    title = 	 {Theorem Proving Using Rigid E-Unification Equational Matings},
    booktitle =  {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)},
    year =	 {1987},
    month =	 {June}, 
    pages =      {338--346},
    location =   {Ithaca, NY, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }