@Article{jancl,
author    ={Tobias Schmidt-Samoa},
title     ={Flexible Heuristics for Simplification with
            Conditional Lemmas by Marking Formulas as
            Forbidden, Mandatory, Obligatory, and Generous},
journal   ={Journal of Applied Non-Classical Logics},
year      ={2006},
pages     ={209--239},
volume    ={16},
number    ={1--2},
publisher ={{\'E}ditions Herm{\`e}s-Lavoisier},
note      ={{\url{http://jancl.revuesonline.com/resnum.jsp?editionId=758}},
            {\url{www.ags.uni-sb.de/~cp/p/jancl/welcome.html}}},
abstract  ={Due to its practical importance,
context-dependent simplification of goals with conditional lemmas 
has been studied for three decades, 
mostly under the label of ``contextual rewriting''.
We present a flexible framework for controlling the recursive relief
of conditions by marking formulas in goals and lemmas.
Within this framework, by marking goal formulas as forbidden,
we can simulate and improve the well-known approaches of 
contextual rewriting and case rewriting.
Furthermore, we develop novel heuristics which may mark goal formulas as
mandatory and lemma formulas as 
obligatory or generous.
Our case studies in the field of rewrite-based inductive theorem
proving are encouraging.}}