@InProceedings{	  Baumgartner:etal:Darwin:ESFOR:2004,
  author	= {Peter Baumgartner and Alexander Fuchs and Cesare Tinelli},
  title		= "{D}arwin: {A} {T}heorem {P}rover for the {M}odel {E}volution
		  {C}alculus",
  booktitle	= {IJCAR Workshop on Empirically Successful First Order
		  Reasoning (ESFOR (aka S4))},
  year		= {2004},
  url		= "http://goedel.cs.uiowa.edu/Darwin/papers/darwin-ESFOR.pdf",
  editor	= {Stephan Schulz and Geoff Sutcliffe and Tanel Tammet},
  series	= {Electronic Notes in Theoretical Computer Science},
  abstract	= "Darwin is the first implementation of the Model Evolution
		  Calculus by Baumgartner and Tinelli. The Model Evolution
		  Calculus lifts the DPLL procedure to first-order logic.
		  Darwin is meant to be a fast and clean implementation of
		  the calculus, showing its effectiveness and providing a
		  base for further improvements and extensions. Based on a
		  brief summary of the Model Evolution Calculus, we describe
		  in the main part of the paper Darwin's proof procedure and
		  its data structures and algorithms, discussing the main
		  design decisions and features that influence Darwin's
		  performance. We also report on practical experiments
		  carried out with problems from the CADE-18 and CADE-19
		  system competitions, as well as on results on parts of the
		  TPTP problem library.",
  note		= {To appear.}
}