Tobias Schmidt-Samoa
Flexible Heuristics for Simplification with Conditional Lemmas by Marking Formulas as Forbidden, Mandatory, Obligatory, and Generous
Journal of Applied Non-Classical Logics 2006, 16(1-2): pp. 209-239
Bibtex Entry
Copyright Owner
Editions Hermes-Lavoisier
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.
Full paper