Darwin - A Theorem Prover for the Model Evolution Calculus

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.