- 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
- 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