Abstract
Finding new theorems is essential for the general progress in mathematics. Apart from creating and proving completely new theorems progress can also be achieved by theorem reuse; i.e. by translating theorems from related theories into the target theory and proving its translated premises under which the theorem was proven. This approach is pursued by the ”little theories” and the development graph paradigms. This work suggests an improvement in this direction in two aspects: partial theory inclusions enhances theorem reuse and formula matching to support automated detection of theory inclusions. By representing theory axioms as facts and partial theories (i.e. theorems and their minimal set of premises) as horn clauses, reusable theorems correspond to derived facts such that model generator like KRHyper can be used for this task.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Autexier, S., Hutter, D.: Maintenance of formal software developments by stratified verification (2002), http://www.dfki.de/vse/papers/ah02.ps.gz
Autexier, S., Hutter, D., Mossakowski, T., Schairer, A.: The development graph manager MAYA (system description). In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, p. 495. Springer, Heidelberg (2002)
Farmer, W.M., Guttman, J.D., Thayer, F.J.: The imps user’s manual. Technical Report M-93B138, The mitre Corporation (1993)
Farmer, W., Guttman, J., Thayer, X.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567–581. Springer, Heidelberg (1992)
Goguen, J.A., Burstall, R.M.: Introducing institutions. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164. Springer, Heidelberg (1984)
Graf, P., Meyer, C.: Advanced indexing operations on substitution trees. In: Conference on Automated Deduction, pp. 553–567 (1996)
Manthey, R., Bry, F.: SATCHMO: A theorem prover implemented in Prolog. In: Lusk, E.L., Overbeek, R.A. (eds.) CADE 1988. LNCS, vol. 310, pp. 415–434. Springer, Heidelberg (1988)
Meseguer, J.: General logics. In: Logic Colloquium, vol. 87, pp. 275–329. North-Holland, Amsterdam (1989)
Normann, I.: Extended normalization for e-retrieval of formulae. In: Proceedings of Communicating Mathematics in the Digital Era (to appear, 2006)
Mossakowski, K.L.T., Maeder, C., Wölfl, S.: Hets, http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/
Wernhard, C.: System description: Krhyper (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Normann, I. (2006). Enhanced Theorem Reuse by Partial Theory Inclusions. In: Calmet, J., Ida, T., Wang, D. (eds) Artificial Intelligence and Symbolic Computation. AISC 2006. Lecture Notes in Computer Science(), vol 4120. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11856290_6
Download citation
DOI: https://doi.org/10.1007/11856290_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-39728-1
Online ISBN: 978-3-540-39730-4
eBook Packages: Computer ScienceComputer Science (R0)