hide
Free keywords:
-
Abstract:
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.