非表示:
キーワード:
-
要旨:
We present a new calculus for first-order theorem proving with equality,
ME+Sup, which generalizes both the Superposition calculus and the Model
Evolution calculus (with equality) by integrating their inference rules and
redundancy criteria in a non-trivial way. The main motivation is to combine the
advantageous features of both---rather complementary---calculi in a single
framework. For instance, Model Evolution, as a lifted version of the
propositional DPLL procedure, contributes a non-ground splitting rule that
effectively permits to split a clause into non variable disjoint subclauses. In
the paper we present the calculus in detail. Our main result is its
completeness under semantically justified redundancy criteria and
simplification rules.
