Abstract
We present a personal view and strategy for algorithm-supported mathematical theory exploration and draw some conclusions for the desirable functionality of future mathematical software systems. The main points of emphasis are: The use of schemes for bottom-up mathematical invention, the algorithmic generation of conjectures from failing proofs for top-down mathematical invention, and the possibility to program new reasoners within the logic on which the reasoners work (“meta-programming”).
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
An Interactive Mathematical Proof System, http://imps.mcmaster.ca/
The Coq Proof Assistant, http://coq.inria.fr/
The Mizar Project, http://www.mizar.org/
The Omega System, http://www.ags.uni-sb.de/~omega/
Asperti, A., Buchberger, B., Davenport, J.H. (eds.): MKM 2003. LNCS, vol. 2594. Springer, Heidelberg (2003)
Buchberger, B.: Groebner Rings in Theorema: A Case Study in Functors and Categories. Technical Report 2003-46, SFB (Special Research Area) Scientific Computing, Johannes Kepler University, Linz, Austria (2003)
Buchberger, B.: Towards the automated synthesis of a Gröbner bases algorithm. RACSAM (Review of the Spanish Royal Academy of Sciences) (2004) (to appear)
Buchberger, B., Craciun, A.: Algorithm synthesis by lazy thinking: Examples and implementation in Theorema. In: Proc. of the Mathematical Knowledge Management Symposium, Edunburgh, UK, November 25-29. ENTCS, vol. 93, pp. 24–59. Elsevier Science, Amsterdam (2003)
Buchberger, B., Dupré, C., Jebelean, T., Kriftner, F., Nakagawa, K., Vasaru, D., Windsteiger, W.: The Theorema project: A progress report. In: Kerber, M., Kohlhase, M. (eds.) Proc. of Calculemus 2000 Conference, St. Andrews, UK, August 6-7, pp. 98–113 (2000)
Buchberger, B., Gonnet, G., Hazewinkel, M. (eds.): Mathematical Knowledge Management: Special Issue of Annals of Mathematics and Artificial Intelligence, vol. 38. Kluwer Academic Publisher, Dordrecht (2003)
Constable, R.: Implementing Mathematics Using the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs (1986)
de Bruijn, N.G.: The mathematical language automath, its usage, and some of its extensions. In: Laudet, M., Lacombe, D., Nolin, L., Schützenberger, M. (eds.) Proc. of Symposium on Automatic Demonstration, Versailles, France. LN in Mathematics, vol. 125, pp. 29–61. Springer, Berlin (1970)
Gordon, M., Melham, T.: Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)
Harper, R.: Programming in Standard ML. Carnegie Mellon University (2001), www-2.cs.cmu.edu/~rwh/smlbook/online.pdf
Kohlhase, M.: OMDoc: Towards an internet standard for the administration, distribution and teaching of mathematical knowledge. In: Campbell, J., Roanes-Lozano, E. (eds.) AISC 2000. LNCS (LNAI), vol. 1930, pp. 32–52. Springer, Heidelberg (2001)
Kutsia, T., Buchberger, B.: Predicate logic with sequence variables and sequence function symbols. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 205–219. Springer, Heidelberg (2004) (to appear)
Luo, Z., Pollack, R.: Lego proof development system: User’s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh (1992)
Magnusson, L., Nordström, B.: The ALF proof editor and its proof engine. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 213–237. Springer, Heidelberg (1994)
Nakagawa, K.: Supporting user-friendliness in the mathematical software system Theorema. Technical Report 02-01, PhD Thesis. RISC, Johannes Kepler University, Linz, Austria (2002)
Paulson, L.: Isabelle: the next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and Computer Science, pp. 361–386. Academic Press, London (1990)
Pfenning, F.: Elf: A meta-language for deductive systems. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol. 814, pp. 811–815. Springer, Heidelberg (1994)
Pfenning, F.: Logical frameworks. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 17, pp. 1063–1147. Elsevier Science and MIT Press (2001)
Piroi, F., Buchberger, B.: An environment for building mathematical knowledge libraries. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) Proc. of the 3rd Int. Conference on Mathematical Knowledge Management, MKM 2004, Bialowieza, Poland, September 19-21. LNCS, Springer, Heidelberg (2004) (to appear)
Tomuta, E.: An architecture for combining provers and its applications in the Theorema system. Technical Report 98-14, PhD Thesis. RISC, Johannes Kepler University, Linz, Austria (1998)
Sato, M.: Theory of judgments and derivations. In: Arikawa, S., Shinohara, A. (eds.) Progress in Discovery Science. LNCS (LNAI), vol. 2281, pp. 78–122. Springer, Heidelberg (2002)
Sato, M., Sakurai, T., Kameyama, Y., Igarashi, A.: Calculi of meta-variables. In: Baaz, M., Makowsky, J.A. (eds.) CSL 2003. LNCS, vol. 2803, pp. 484–497. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Buchberger, B. (2004). Algorithm-Supported Mathematical Theory Exploration: A Personal View and Strategy. In: Buchberger, B., Campbell, J. (eds) Artificial Intelligence and Symbolic Computation. AISC 2004. Lecture Notes in Computer Science(), vol 3249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30210-0_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-30210-0_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23212-4
Online ISBN: 978-3-540-30210-0
eBook Packages: Springer Book Archive