Abstract
We extend our framework of incremental proof planning. By employing nested sets of meta-rules the formulation of strategies may be structured. By switching to another meta-rule set the planner can adjust to a new situation within the proof. The new meta-rule set represents a more specialized strategy better suited for the current situation. We define the semantics of our framework by an inference system.
Preview
Unable to display preview. Download preview PDF.
References
Robert S. Boyer and J Strother Moore. A Computational Logic. ACM Monograph Series. Academic Press, 1979.
Alan Bundy. A science of reasoning. In J-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson, pages 178–198. MIT press, 1991.
Alan Bundy, Andrew Stevens, Frank van Harmelen, Alan Smaill, and Andrew Ireland. Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence, 62(2):185–253, August 1993.
R. L. Constable, T. B. Knoblock, and J. L. Bates. Writing programs that construct proofs. Journal of Automated Reasoning, 1:285–326, 1985.
Stefan Gerberding and Axel Noltemeier. Choosing induction relations within the INKA system (extended abstract). In Proceedings of the 19th German Annual Conference on Artificial Intelligence, Bielefeld, Germany, pages 329–331, 1995.
Stefan Gerberding and Axel Noltemeier. Incremental proof planning by metarules. In Douglas D. Dankel II, editor, Proceedings of the 10th FLAIRS Conference, Daytona Beach, Fa., pages 171–175. Florida AI Research Society, May 1997.
Xiaorong Huang, Manfred Kerber, Jörn Richts, and Arthur Sehn. Planning mathematical proofs with methods. SEKI Report SR-94-08, Universität Kaiserslautern, 1994.
Andrew Ireland and Alan Bundy. Productive use of failure in inductive proofs. Journal of Automated Reasoning, 16:79–111, 1996.
Axel Noltemeier. Inkrementelle Beweisplanung mit Metaregeln. Diploma Thesis, University of Darmstadt, 1996.
Brigitte Pientka. Strukturierung der Beweisplanung lurch Metaregelmengen. Diploma Thesis, University of Darmstadt, 1997.
Martin Protzen. Lazy generation of induction hypotheses. In Proceedings of the 12th International Conference on Automated Deduction, Nancy, France, LNAI vol. 814, pages 42–56. Springer, 1994.
Inger Sonntag and Jörg Denzinger. Extending automated theorem proving by planning. SEKI Report SR-93-02, Universität Kaiserslautern, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gerberding, S., Pientka, B. (1997). Structured incremental proof planning. In: Brewka, G., Habel, C., Nebel, B. (eds) KI-97: Advances in Artificial Intelligence. KI 1997. Lecture Notes in Computer Science, vol 1303. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3540634932_4
Download citation
DOI: https://doi.org/10.1007/3540634932_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63493-5
Online ISBN: 978-3-540-69582-0
eBook Packages: Springer Book Archive