We present an associative-commutative paramodulation calculus that generalizes the associative-commutative completion procedure to firstorder clauses. The calculus is parametrized by a selection function (on negative literats) 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.
CITATION STYLE
Bachmair, L., & Ganzinger, H. (1995). Associative-commutative superposition. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 968, pp. 1–14). Springer Verlag. https://doi.org/10.1007/3-540-60381-6_1
Mendeley helps you to discover research relevant for your work.