In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, LNCS 713, pages 83-96, Brno, Czech Republic, August 24-27, 1993. Springer-Verlag.
Earlier version: Technical Report MPI-I-93-204, Max-Planck-Institut für Informatik, Saarbrücken, February 1993.
Abstract: We show that 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.