In many theorem proving applications, a proper treatment of equational theories or equality is mandatory. In this paper we show how to integrate a modern treatment of equality in the Model Evolution calculus (ME), a first-order version of the propositional DPLL procedure. The new calculus, MEE, is a proper extension of the ME calculus without equality. Like ME it maintains an explicit candidate model, which is searched for by DPLL-style splitting. For equational reasoning MEE uses an adapted version of the superposition inference rule, where equations used for superposition are drawn (only) from the candidate model. The calculus also features a generic, semantically justified simplification rule which covers many simplification techniques known from superposition-style theorem proving. Our main theoretical result is the correctness of the MEE calculus in the presence of very general redundancy elimination criteria. We also describe our implementation of the calculus, the E-Darwin system, and we report on practical experiments with it on the TPTP problems library.

The TPTP World is a well established infrastructure supporting research, development, and deployment of Automated Theorem Proving systems. Recently, the TPTP World has been extended to include a typed first-order logic, which in turn has enabled the integration of arithmetic. This paper describes these developments.

We describe an approach to modelling and reasoning about data-centric business processes and present a form of general model checking. Our technique extends existing approaches, which explore systems only from concrete initial states.

Specifically, we model business processes in terms of smaller fragments, whose possible interactions are constrained by first-order logic formulae. In turn, process fragments are connected graphs annotated with instructions to modify data. Correctness properties concerning the evolution of data with respect to processes can be stated in a first-order branching-time logic over built-in theories, such as linear integer arithmetic, records and arrays.

Solving general model checking problems over this logic is considerably harder than model checking when a concrete initial state is given. To this end, we present a tableau procedure that reduces these model checking problems to first-order logic over arithmetic. The resulting proof obligations are passed on to appropriate “off-the-shelf” theorem provers. We also detail our modelling approach, describe the reasoning components and report on first experiments.