Extending the Reach of Proof Planning by Randomization and Restart Techniques
Andreas Meier, Carla Pedro Gomes, Erica Melis⋆, Fachbereich Informatik · 2006
Proof planning provides a powerful theorem proving framework. In particular, the many different ways of encoding domain-specific knowledge has enabled the derivation of theorems that lay outside the scope of calculus logicbased theorem proving systems. However, acquiring appropriate domain knowledge has proven to be quite challenging. So far, existing applications often benefit from the existence of domain knowledge whose usage leads to very restricted search spaces. This facilitates the proving process for problems whose proofs are in this restricted search space, but it excludes many problems and strongly restricts the kinds of proofs that can be found for a given problem instance. Our proposal, supported by an empirical evaluation, is to make the proof planning process more general and more robust with regard to domain specific knowledge. Our work extends knowledge-based proof planning by incorporating a set of randomization rules into the planning strategies. Such an approach does not rely on finely tuned domain-specific control knowledge and is hence successful in domains that lack strong control information. The approach takes advantage of the surprising diversity in terms of the size and style of possible proofs. 1