@MastersThesis{Fuchs:Darwin:Thesis:2004,
  author = 	 {Alexander Fuchs},
  title = 	 {{D}arwin: {A} {T}heorem {P}rover for the {M}odel {E}volution
		  {C}alculus},
  school = 	 {University of Koblenz-Landau},
  year = 	 2004,
  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.}
}