@InProceedings{	  Baumgartner:etal:Darwin:IJAIT:2005,
  author        = {Peter Baumgartner and Alexander Fuchs and Cesare Tinelli},
  title	        = "{I}mplementing the {M}odel {E}volution {C}alculus",
  booktitle     = {{S}pecial {I}ssue of the {I}nternational {J}ournal of
                   {A}rtificial {I}ntelligence {T}ools ({IJAIT})},
  year	        = {2005},
  volume        = 15,
  number        = 1,
  url	        = "http://goedel.cs.uiowa.edu/Darwin/papers/darwin-IJAIT.pdf",
  editor        = {Stephan Schulz and Geoff Sutcliffe and Tanel Tammet},
  series        = {{I}nternational {J}ournal of {A}rtificial {I}ntelligence {T}ools},
  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
                   CASC-J2 system competition and parts of the TPTP Problem Library,
                   and compare the results with those of other state-of-the-art theorem provers.",
  note		= {Preprint.}
}