非表示:
キーワード:
-
要旨:
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.