MPI-INF/SWS Research Reports 1991-2021
1. Author,Editor - 3. with BibTeX cite keys
MPI-I-93-267
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.
Note:
Revised version in Proc.~CTRS, LNCS 968
-
MPI-I-93-267.pdf
- MPI-I-93-267.dvi
- Attachement: MPI-I-93-267.dvi (67 KBytes); MPI-I-93-267.pdf (123 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1993-267
BibTeX@TECHREPORT{BachmairGanzinger-93-mpii267,
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},
}