Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Associative-commutative superposition

Bachmair, Leo and Ganzinger, Harald

MPI-I-93-267. December 1993, ? pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-93-267.pdfMPI-I-93-267.pdfMPI-I-93-267.dvi - MPI-I-93-267.dvi
67 KBytes; 123 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
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},