Superposition with simplification as a decision procedure for the monadic class with equality
Ganzinger, H., Bachmair, L., Uwe Waldmann · MPG.PuRe (Max Planck Society) · 1993
We show that strict superposition, a restricted form of paramodulation, can be combined with specifically designed simplification rules such that it becomes a decision procedure for the monadic class with equality. The completeness of the method follows from a general notion of redundancy for clauses and superposition inferences.