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