E-Darwin -
A Theorem Prover for the Model Evolution Calculus with Equality

About E-Darwin

E-Darwin is an automated theorem prover for first-order clausal logic with equality. It accepts problems in tptp or tme syntax. Non-clausal input is clausified using the eprover (or soon a built-in clausifier).

E-Darwin implements the Model Evolution calculus and several variants thereof which include equality reasoning, see the papers. The system is a based on the Darwin prover. As Darwin is no longer actively maintained, E-Darwin will eventually subsume all of its functions. The development of E-Darwin forked off from Darwin 1.3, so at the moment E-Darwin still needs to catch up on the changes made between Darwin 1.3 and its last version, Darwin 1.4.5.


You can download the current (26-09-2011) version of E-Darwin here.

Some software requirements:


So far the majority of the relevant papers are for Darwin and the Model Evolution calculus. The following list is therefore mostly identical to the Darwin publications.


E-Darwin is maintained by Björn Pelzer.