Model evolution with equality -- revised and implemented (Q429586): Difference between revisions

The paper presents the revised and improved version of the model evolution calculus with equality. The authors extend the model evolution calculus by adding some inference rules for equality reasoning. These rules were centered around a version of the ordered paramodulation inference rules adapted to the model evolution calculus. The new calculus works with a set of literals, which are called a context, and a set of clauses. Correspondingly, it has two kinds of inference rules, one for modifying contexts, and one for deriving new clauses, with the latter consisting mostly on unit-superposition-style inference rule. As a result, this calculus features more powerful redundancy criteria and removes some nondeterminism from the calculus. The authors prove the soundness and completeness of the calculus and discuss its implementation in the \texttt{E-Darvin} theorem prover based on \texttt{Darvin}.