# Darwin - A Theorem Prover for the Model Evolution Calculus

Alexander Fuchs
### Abstract

The scope of this thesis is the theorem prover Darwin,
the first implementation of the Model Evolution calculus,
a lifting of the DPLL procedure to first-order logic
developed by Baumgartner and Tinelli.
Darwin provides an initial evaluation of the calculus' potential
and a clean basis for further improvement.
After the calculus is sketched
the proof procedure and the chosen data structures and algorithms are presented,
and it is proven that these constitute
a proper instantiation of the calculus preserving soundness and completeness.
Darwin is evaluated against the TPTP Problem Library
and the CASC competition,
thereby demonstrating that for the Bernays-Sch\"{o}nfinkel class
Darwin's performance is on par with that of the best provers.
Finally, promising ideas on how to improve on the current implementation are pointed out.

Alexander Fuchs
Last modified: Sun Mar 20 16:51:19 CST 2005