@TechReport{	  baumgartner:tinelli:1:2003,
  author	= "Peter Baumgartner and Cesare Tinelli",
  title		= "{T}he {M}odel {E}volution {C}alculus",
  institution	= "{Universität Koblenz-Landau}",
  year		= "{2003}",
  type		= "Fachberichte Informatik",
  number	= "1--2003",
  language	= "english",
  address	= "Universität Koblenz-Landau, Institut für
		  Informatik, Rheinau 1, D-56075 Koblenz",
  url		= "http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-1-2003.pdf"
		  ,
  abstract	= "The DPLL procedure, due to Davis, Putnam, Logemann, and
		  Loveland, is the basis of some of the most successful
		  propositional satisfiability solvers to date. Although
		  originally devised as a proof-procedure for first-order
		  logic, it has been used almost exclusively for
		  propositional logic so far because of its highly
		  inefficient treatment of quantifiers, based on
		  instantiation into ground formulas. \par The recent FDPLL
		  calculus by Baumgartner was the first successful attempt to
		  lift the procedure to the first-order level without
		  recurring to ground instantiations. FDPLL lifts to the
		  first-order case the core of the DPLL procedure, the
		  splitting rule, but ignores other aspects of the procedure
		  that, although not necessary for completeness, are crucial
		  for its effectiveness in practice. \par In this paper, we
		  present a new calculus loosely based on FDPLL that lifts
		  these aspects as well. In addition to being a more faithful
		  litfing of the DPLL procedure, the new calculus contains a
		  more systematic treatment of {\em universal literals\/},
		  one of FDPLL's optimizations, and so has the potential of
		  leading to much faster implementations."
}