@INPROCEEDINGS{BachmairGanzinger-95-ctrs,                      
        AUTHOR             = {Bachmair, L. and Ganzinger, H.},
        ADDRESS            = b,
        BOOKTITLE          = {Proc.\ 4th Int'l Workshop on Conditional and Typed Rewrite Systems, {\rm Jerusalem}},
        EDITOR             = {Dershowitz, N. and Lindenstrauss, N.},
        PAGES              = {1--14},
        PUBLISHER          = s,
        SERIES             = lncs,
	VOLUME		   = {968},
        TITLE              = {Associative-Commutative Superposition},
        YEAR               = {1995},
	NOTE		   = {Revised version of TR MPI-I-93-267, 1993},
        ABSTRACT = {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.
}
}