Flexible heuristics for simplification with conditional lemmas by marking formulas as forbidden, mandatory, obligatory, and generous

Authors: Tobias Schmidt-Samoa
Title: Flexible Heuristics for Simplification with Conditional Lemmas by Marking Formulas as Forbidden, Mandatory, Obligatory, and Generous
In: Journal of Applied Non-Classical Logics 2006, 16(1-2):209-239:
DOI 10.3166/jancl.16.209-239,
Bibtex Entry
Copyright Owner: Editions Hermes-Lavoisier
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.
Full paper: Local replacement for disfunct official DOI and ONLINE access