@Unpublished{	  Baumgartner:etal:ModelEvolutionLearning:2006,
  author	= {Peter Baumgartner and Alexander Fuchs and Cesare Tinelli},
  title         = {Lemma Learning in the Model Evolution Calculus},
  note          = {Long version of a conference submission},
  month         = {March},
  year          = {2006},
  abstract      = {The Model Evolution (ME) Calculus is a proper lifting 
                   to first-order logic of the DPLL procedure, 
                   a backtracking-based search procedure for propositional satisfiability.
                   Analogously to DPLL, the ME calculus is based on the idea of 
                   incrementally building a model of the input formula
                   by alternating constraint propagation steps with 
                   non-deterministic decision steps.
                   One of the major conceptual improvements over basic DPLL 
                   is lemma learning, 
                   a mechanism for generating new formulae
                   that prevent later in the search
                   combinations of decision steps guaranteed to lead to failure.

                   We introduce three lemma generation methods for 
                   ME proof procedures,
                   with various degrees of power, effectiveness in reducing search,
                   and computational overhead.
                   Even if formally correct, 
                   each of these methods presents complications 
                   that do not exist at the propositional level but need to be addressed
                   for learning to be effective in practice for ME.
                   We discuss some of these issues and then present 
                   initial experimental results on the performance
                   of an implementation within Darwin of the three learning procedures.},
  annote         = {unpublished}
}