MPI-INF/SWS Research Reports 1991-2017

2. Number - only D2


Associative-commutative superposition

Bachmair, Leo and Ganzinger, Harald

December 1993, ? pages.

Status: available - back from printing

We present an associative-commutative paramodulation calculus that generalizes the associative-commutative completion procedure to first-order clauses. The calculus is parametrized by a selection function (on negative literals) and a well-founded ordering on terms. It is compatible with an abstract notion of redundancy that covers such simplification techniques as tautology deletion, subsumption, and simplification by (associative-commutative) rewriting. The proof of refutational completeness of the calculus is comparatively simple, and the techniques employed may be of independent interest.
Revised version in Proc.~CTRS, LNCS 968

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Bachmair, Leo and Ganzinger, Harald},
  TITLE = {Associative-commutative superposition},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-93-267},
  MONTH = {December},
  YEAR = {1993},
  ISSN = {0946-011X},
  NOTE = {Revised version in Proc.~CTRS, LNCS 968},