hide
Free keywords:
-
Abstract:
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 these two rather complementary calculi in a single
framework. In particular, 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 \emph{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. We also show how under certain assumptions the model
representation computed by a (finite and fair) derivation can be queried in an
effective way.
