Authors
Tobias Schmidt-Samoa
Title
Mandatory versus Forbidden Literals in Simplification with Conditional Lemmas
In
5th Int. Workshop on First-Order Theorem Proving (FTP 2005)
Bibtex Entry
Copyright Owner
Author
Abstract
Due to its practical importance, context-dependent simplification with conditional lemmas has been studied for three decades, mostly under the label ``contextual rewriting''. We develop novel heuristics restricting the relief of conditions with mandatory literals in the goals and obligatory literals in the lemmas. Our case studies in the field of rewrite-based inductive theorem proving are encouraging.
Review
By anonymous CADE referee (literal):
-------------------- review 106 --------------------
OVERALL RATING: 2 (accept)
CONFIDENCE: 3 (high)
----------------------- REVIEW --------------------
Summary: The author develops an approach for context-dependent simplification (of proof goals) with conditional lemmas. Novel heuristics for restricting the way conditions are verified, with "mandatory" literals in the goals and "obligatory" literals in the lemmas, are presented. Illustrating example are given, and a comparison with related approaches for this kind of contextual rewriting is sketched, based on case studies and an implementation in the author's inductive theorem prover QuodLibet. The experimental results seem to indicate that the new heuristics are comparable with ordinary contextual rewriting and, in some cases, are also clearly better. What is interesting in the paper, besides the quantitative aspects of the above comparison, is the abstract conceptual level used to define the heuristics, by introducing different types of literals in goals and lemmas. The progress that can be achieved with this approach doesn't seem to be dramatic. However, in view of the utmost important of context-dependent simplification (as fundamental operation) in automated deduction, the paper nevertheless represents solid and interesting work that deserves acceptance and publication.
Full paper