Superposition with simplification as a decision procedure for the monadic class with equality

Leo Bachmair, Harald Ganzinger, and Uwe Waldmann

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.


Previous | Up | Next
Uwe Waldmann <uwe@mpi-inf.mpg.de>, 1997-10-02.
Imprint | Data Protection