Abstract
In this paper we describe a first experiment with a new approach for building theorem provers that can formalize themselves, reason about themselves, and safely extend themselves with new inference procedures. Within the GETFOL system we have built a pair of functions that operate between the system's implementation and a theory about this implementation. The first function lifts the actual inference rules to axioms that comprise a theory of GETFOL's inference capabilities. This allows us to turn the prover upon itself whereby we may formally reason about its inference rules and derive new rules. The second function flattens new rules back into the underlying system. This provides a novel means of safe system self-extension and an efficient way of executing derived rules.
Preview
Unable to display preview. Download preview PDF.
References
D. Basin, F. Giunchiglia, and P. Traverso. Meta-theory as the dual of system implementation. Technical Report 9103-015, IRST, Trento, Italy, 1991.
R.S. Boyer and J.S. Moore. Metafunctions: proving them correct and using them efficiently as new proof procedures. In R.S. Boyer and J.S. Moore, editors, The correctness problem in computer science, pages 103–184. Academic Press, 1981.
R.L. Constable, S.F. Allen, H.M. Bromley, et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice Hall, 1986.
F. Giunchiglia and P. Traverso. Plan formation and execution in an uniform architecture of declarative metatheories. In M. Bruynooghe, editor, Proc. Workshop on Meta-Programming in Logic, 1990. Also available as IRST Technical Report 9003-12.
F. Giunchiglia and P. Traverso. GETFOL User Manual — version 1 release 1. Technical report, IRST, Trento, Italy, 1991.
F. Giunchiglia and P. Traverso. Reflective reasoning with and between a declarative metatheory and the implementation code. In Proceedings of the International Joint Conference in Artificial Intelligenge (IJCAI), 1991. Also IRST-Technical Report no. 9012-03.
L. Paulson. The fundation of a generic theorem prover. Journal of Automated Reasoning, 5:363–396, 1989.
D. Prawitz. Natural Deduction — A proof theoretical study. Almquist and Wiksell, Stockholm, 1965.
B.C. Smith. Reflection and Sematincs in LISP. In Proc. 11th ACM POPL, pages 23–35, 1983.
R.W. Weyhrauch. Prolegomena to a theory of Mechanized Formal Reasoning. Artificial Intelligence. Special Issue on Non-monotonic Logic, 13(1), 1980.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Basin, D., Giunchiglia, F., Traverso, P. (1991). Automating meta-theory creation and system extension. In: Ardizzone, E., Gaglio, S., Sorbello, F. (eds) Trends in Artificial Intelligence. AI*IA 1991. Lecture Notes in Computer Science, vol 549. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-54712-6_217
Download citation
DOI: https://doi.org/10.1007/3-540-54712-6_217
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54712-9
Online ISBN: 978-3-540-46443-3
eBook Packages: Springer Book Archive