Model evolution (ME) calculus is a promising new calculus for automated first-order theorem proving; this paper introduces ME.

The main motivation for ME can best be understood by first looking at the Davis-Putnam-Logemann-Loveland procedure (DPLL), which is the dominant method for building (complete) satisfiability (SAT) solvers (procedures that test propositional formulas for satisfiability). Efficient SAT solvers based on DPLL are used in industrial applications, for example, as the main inference engine in verification tools based on model checking. Though DPLL was originally devised as a proof procedure for first-order logic, it has been used almost exclusively for propositional logic so far. This is because of its inefficient treatment of quantifiers, which is based on instantiation into ground formulas.

One rationale behind ME is to address this issue by providing a direct lifting of the propositional core of DPLL, in the same sense as first-order resolution lifts propositional resolution. Another rationale is to adapt the powerful search heuristics that make DPLL so effective at the propositional level, thus capitalizing on the successful developments in that area over the last few years.

The technical contributions of the paper focus on the first-mentioned rationale (and refer to another paper for the second one). To this end, the paper recapitulates the DPLL calculus in a sequent-style notation as a basis for the lifted ME version. Sequents are of the form C ⊪ F, where C is called a context and F is the clause set currently under consideration. In the propositional case, C is a set of propositional literals, which (partially) represent a propositional interpretation. The calculus essentially searches for an interpretation (represented by a context C) that satisfies F.

Obviously, in ME, the set F can now be a set of first-order clauses. The main technical insight underlying the ME calculus is a lifted version of the propositional contexts. These contexts consist of first-order literals. Using a quite-sophisticated construction, they again induce an interpretation. The goal of the calculus is, as for DPLL, to search for a model of the clause set. The exact definition of these contexts and their use in inference rules is quite involved, and cannot be discussed in detail here. In effect, the way the contexts are defined justifies certain simplification and propagation rules, which are proven to be quite successful in the propositional case (DPLL). The main technical results proven in the paper are soundness and (strong) completeness in the presence of these rules. Implementation issues and related work are also discussed.

To sum up, the paper provides an in-depth presentation of the ME calculus. It should be of interest to researchers working on automated reasoning in first-order logic, and also to researchers from the SAT community.