Abstract
The well-known theorem asserting the irrationality of \(\sqrt 2\) was proposed as a case study for a comparison of fifteen (interactive) theorem proving systems [Wiedijk, 2002]. This represents an important shift of emphasis in the field of automated deduction away from the somehow artificial problems of the past back to real mathematical challenges.
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.
Bibliography
S. Allen, R. Constable, R. Eaton, C. Kreitz, and L. Lorigo. The Nupri open logical environment. In McAllester [ 2000 ].
P. Andrews, M. Bishop, S. Issar, D Nesmith, F. Pfenning, and H. Xi. TPS: A theorem proving system for classical type theory. Journal of Automated Reasoning, 16 (3): 321–353, 1996.
R. Bartle and D. Sherbert. Introduction to Real Analysis. Wiley, 2nd edition, 1982.
P. Baumgartner and U. Furbach. PROTEIN, a PROver with a Theory INterface. In Bundy [ 1994 ], pages 769–773.
C. Benzmüller and M. Kohlhase. LEO — a higher-order theorem prover. In Kirchner and Kirchner [ 1998 ].
C. Benzmüller and V. Sorge. A blackboard architecture for guiding interactive proofs. In Giunchiglia [ 1998 ].
C. Benzmüller and V. Sorge. SZ-ANTS - An open approach at combining Interactive and Automated Theorem Proving. In Kerber and Kohlhase [ 2000 ].
C. Benzmüller, M. Bishop, and V. Sorge. Integrating TPS and f2MEGA. Journal of Universal Computer Science, 5: 188–207, 1999.
Benzmüller et al.,2002] C. Benzmüller, A. Fiedler, A. Meier, and M. Pollet. Irrationality off — a case study in ftMEGA. Seki-Report SR-02–03, Department of Computer Science, Saarland University, Saarbrücken, Germany, 2002.
Benzmüller et al.,2003] C. Benzmüller, A. Meier, and V. Sorge. Bridging theorem proving and mathematical knowledge retrieval. In Festschrift in Honour of Jörg Siekmann’s 609 Birthday,LNAI. Springer, 2003. To appear.
C. Benzmüller. Equality and Extensionality in Higher-Order Theorem Proving. PhD thesis, Department of Computer Science, Saarland University, Saarbrücken, Germany, 1999.
M. Bishop and P. Andrews. Selectively instantiating definitions. In Kirchner and Kirchner [ 1998 ].
W. Bledsoe. Challenge problems in elementary calculus. Journal of Automated Reasoning, 6: 341–359, 1990.
N. Bourbaki. Theory of sets. His Elements of mathematics, 1. Paris, Hermann Reading Mass., Addison-Wesley, 1968.
Bundy et al.,1990] A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam System. In M. Stickel, editor, Proceedings of the 10th Conference on Automated Deduction,number 449 in LNCS, pages 647–648, Kaiserslautern, Germany, 1990. Springer.
A. Bundy. The use of explicit plans to guide inductive proofs. In Lusk and Overbeek [ 1988 ], pages 111–120.
A. Bundy, editor. Proceedings of the 12th Conference on Automated Deduction, number 814 in LNAI. Springer, 1994.
A. Bundy. A critique of proof planning. In Computational Logic: LogicProgramming and Beyond, number 2408 in LNCS, pages 160–177. Springer, 2002
Char et al.,1992] B. Char, K. Geddes, G. Gonnet, B. Leong, M. Monagan, and S. Watt. First leaves: a tutorial introduction to Maple V. Springer, 1992.
L. Cheikhrouhou and J. Siekmann. Planning diagonalization proofs. In Giunchiglia [ 1998 ], pages 167–180.
L. Cheikhrouhou and V. Sorge. PDS — A Three-Dimensional Data Structure for Proof Plans. In Proceedings of the International Conference on Artificial and Computational Intelligence for Decision, Control and Automation in Engineering and Industrial Applications (ACIDCA ‘2000), Monastir, Tunisia, 22–24 March 2000.
A. Church. A Formulation of the Simple Theory of Types. The Journal of Symbolic Logic, 5: 56–68, 1940.
Coq Development Team, 1999–2003] Coq Development Team. The Coq Proof Assistant Reference Manual. INRIA 1999–2003. See http://coq.inria.fr/doc/main.html.
H. de Nivelle. Bliksem 1.10 user manual. Technical report, MaxPlanck-Institut fr Informatik, 1999.
Doris, 2001] The Doris system is available at http://ww.cogsci.ed.ac.uk/~jbos/doris/.
M. Drummond. On precondition achievement and the computational economics of automatic planning. In Current Trends in AI Planning, pages 6–13. IOS Press, 1994.
A. Fiedler. R rex: An interactive proof explainer. In Goré et al. [ 2001 ].
A. Fiedler. Dialog-driven adaptation of explanations of proofs. In B. Nebel, editor, Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI), pages 1295–1300, Seattle, WA, 2001. Morgan Kaufmann.
A. Fiedler. User-adaptive proof explanation. PhD thesis, Department of Computer Science, Saarland University, Saarbrücken, Germany, 2001.
R.E. Fikes and N.J. Nilsson. STRIPS: A new approach to the application of theorem proving to problem solving. Artificial Intelligence, 2: 189–208, 1971.
R. R. Fikes, P. E. Hart, and N. J. Nilsson. Learning and executing generalized robot plans. Artificial Intelligence, 3: 251–288, 1972.
A. Franke and M. Kohlhase. System description: MBAsE, an open mathematical knowledge base. In McAllester [ 2000 ].
H. Ganzinger, editor. Proceedings of the 16th Conference on Automated Deduction, number 1632 in LNAI. Springer, 1999.
H. Gebhard. Beweisplanung für die Beweise der Vollständigkeit verschiedener Resolutionskalküle in SIMEGA. Master’s thesis, Department of Computer Science, Saarland University, Saarbrücken, Germany, 1999.
G. Gentzen. Untersuchungen über das logische Schließen I XXXXXX II. Mathematische Zeitschrift, 39: 176–210, 572–595, 1935.
F. Giunchiglia, editor. Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA’98), number 1480 in LNAI. Springer, 1998.
M. Gordon and T. Melham. Introduction to HOL - A theorem proving environment for higher order logic. Cambridge University Press, 1993.
R. Goré, A. Leitsch, and T. Nipkow, editors. Automated Reasoning — ist International Joint Conference, IJCAR 2001, number 2083 in LNAI. Springer, 2001.
J. Hadamard. The Psychology of Invention in the Mathematical Field. Dover Publications, New York, USA; edition 1949, 1944.
Th. Hillenbrand, A. Jaeger, and B. Löchner. System description: Waldmeister — improvements in performance and ease of use. In Ganzinger [ 1999 ], pages 232–236.
X. Huang. Reconstructing Proofs at the Assertion Level. In Bundy [ 1994 ], pages 738–752.
A. Ireland and A. Bundy. Productive use of failure in inductive proof. Journal of Automated Reasoning, 16 (1–2): 79–111, 1996.
M. Kerber and M. Kohlhase, editors. 8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus2000). AK Peters, 2000.
C. Kirchner and H. Kirchner, editors. Proceedings of the 15th Conference on Automated Deduction, number 1421 in LNAI. Springer, 1998.
H. Kirchner and C. Ringeissen, editors. Frontiers of combining systems: Third International Workshop, FroCoS 2000, volume 1794 of LNAL Springer, 2000.
M. Kohlhase and A. Franke. MBAsE: Representing knowledge and context for the integration of mathematical software systems. Journal of Symbolic Computation; Special Issue on the Integration of Computer Algebra and Deduction Systems, 32 (4): 365–402, September 2001.
E. Lusk and R. Overbeek, editors. Proceedings of the 9th Conference on Automated Deduction, number 310 in LNCS, Argonne, Illinois, USA, 1988. Springer.
R. Manthey and F. Bry. SATCHMO: A theorem prover implemented in Prolog. In Lusk and Overbeek [ 1988 ], pages 415–434.
D. McAllester, editor. Proceedings of the 17th Conference on Automated Deduction, number 1831 in LNAI. Springer, 2000.
W. W. McCune. Otter 3.0 reference manual and guide. Technical Report ANL-94–6, Argonne National Laboratory, Argonne, Illinois 60439, USA, 1994.
W. McCune. Solution of the Robbins problem. Journal of AutomatedReasoning, 19 (3): 263–276, 1997.
A. Meier and V. Sorge. Exploring properties of residue classes. In Kerber and Kohlhase [ 2000 ].
A. Meier, M. Pollet, and V. Sorge. Classifying Isomorphic Residue Classes. In R. Moreno-Diaz, B. Buchberger, and J.-L. Freire, editors, A Selection of Papers from the 8th International Workshop on Computer Aided Systems Theory (EuroCAST 2001), number 2178 in LNCS, pages 494–508. Springer, 2001.
A. Meier, E. Melis, and M. Pollet. Towards extending domain representations. Seki Report SR-02–01, Department of Computer Science, Saarland University, Saarbrücken, Germany, 2002.
A. Meier, M. Pollet, and V. Sorge. Comparing Approaches to the Exploration of the Domain of Residue Classes. Journal of Symbolic Computation, Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems, 34(4):287–306, October 2002. Steve Linton and Roberto Sebastiani, eds.
A. Meier. TRAMP: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level. In McAllester [ 2000 ].
A. Meier. Proof Planning with Multiple Strategies. PhD thesis, Department of Computer Science, Saarland University, Saarbrücken, Germany, 2003.
E. Melis and A. Meier. Proof planning with multiple strategies. In J. Loyd, V. Dahl, U. Furbach, M. Kerber, K. Lau, C. Palamidessi, L.M. Pereira, Y. Sagivand, and P. Stuckey, editors, First International Conference on Computational Logic (CL-2000), number 1861 in LNAI, pages 644–659, London, UK, 2000. Springer.
E. Melia and J. Siekmann. Knowledge-based proof planning. Artificial Intelligence, 115 (1): 65–105, 1999.
E. Melia, J. Zimmer, and T. Müller. Integrating constraint solving into proof planning. In Kirchner and Ringeissen [ 2000 ].
E. Melia. Island planning and refinement. Seki-Report SR-96–10, Department of Computer Science, Saarland University, Saarbrücken, Germany, 1996.
Erica Melis. AI-techniques in proof planning. In H. Prade, editor, Proceedings of the 13th European Conference on Artifical Intelligence, pages 494–498, Brighton, UK, 1998. John Wiley XXXXXX Sons, Chichester, UK.
A. Newell and H. Simon. GPS: A program that simulates human thought. In E. Feigenbaum and J. Feldman, editors, Computers and Thought, pages 279–296. McGraw-Hill, New York, NY, 1963.
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Number 2283 in LNCS. Springer, 2002.
Owre et al.,1996] S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T. Hen-zinger, editors, Computer-Aided Verification, CAV ‘86,number 1102 in LNCS, pages 411–414, New Brunswick, NJ, 1996. Springer.
L. Paulson. Isabelle: A Generic Theorem Prover. Number 828 in LNCS. Springer, 1994.
G. Polya. How to Solve it. Princeton University Press, 1973.
A. Riazanov and A. Voronkov. Vampire 1.1 (system description). In Goré et al. [ 2001 ].
J. Richardson, A. Smaill, and I. Green. System description: Proof planning in higher-order logic with AClam. In Kirchner and Kirchner [ 1998 ].
M. Schönert et al. GAP - Groups, Algorithms, and Programming. Lehrstuhl D für Mathematik, Rheinisch Westfälische Technische Hochschule, Aachen, Germany, 1995.
J. Siekmann, S. Hess, C. Benzmüller, L. Cheikhrouhou, A. Fiedler, H. Horacek, M. Kohlhase, K. Konrad, A. Meier, E. Melis, M. Pollet, and V. Sorge. LOUT: Lovely S2MEGA User Interface. Formal Aspects of Computing, 11: 326–342, 1999.
Siekmann et al.,2002] J. Siekmann, C. Benzmüller, V. Brezhnev, L. Cheikhrouhou, A. Fiedler, A. Franke, H. Horacek, M. Kohlhase, A. Meier, E. Melis, M. Moschner, I. Normann, M. Pollet, V. Sorge, C. Ullrich, C.-P. Wirth, and J. Zimmer. Proof development with S1MEGA. In Voronkov [2002], pages 143–148.
V. Sorge. Non-Trivial Computations in Proof Planning. In Kirchner and Ringeissen [ 2000 ].
V. Sorge. fl-ANTS — A Blackboard Architecture for the Integration of Reasoning Techniques into Proof Planning. PhD thesis, Department of Computer Science, Saarland University, Saarbrücken, Germany, 2001.
G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In Bundy [ 1994 ].
Voetal., 2003] B. Quoc Vo, C. Benzmüller, and S. Autexier. Assertion application in theorem proving and proof planning. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI),Acapulco, Mexico, 2003. (poster description).
A. Voronkov, editor. Proceedings of the 18th International Conference on Automated Deduction, number 2392 in LNAI. Springer, 2002.
C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, Th. Engel, E. Keen, C. Theobalt, and D. Topic. System description: SPASS version 1.0.0. In Ganzinger [ 1999 ], pages 378–382.
D. Weld. An introduction to least commitment planning. AI Magazine, 15 (4): 27–61, 1994.
F. Wiedijk. The fifteen provers of the world. Unpublished Draft, 2002.
J. Zhang and H. Zhang. SEM: A system for enumerating models. In C. S. Mellish, editor, Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI), pages 298–303, Montreal, Canada, 1995. Morgan Kaufmann, San Mateo, California, USA.
J. Zimmer and M. Kohlhase. System description: The Mathweb Software Bus for distributed mathematical reasoning. In Voronkov [ 2002 ], pages 138–142.
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Siekmann, J., Benzmüller, C., Fiedler, A., Meier, A., Normann, I., Pollet, M. (2003). Proof Development with Ωmega: The Irrationality of \(\sqrt 2\) . In: Kamareddine, F.D. (eds) Thirty Five Years of Automating Mathematics. Applied Logic Series, vol 28. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0253-9_11
Download citation
DOI: https://doi.org/10.1007/978-94-017-0253-9_11
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-6440-0
Online ISBN: 978-94-017-0253-9
eBook Packages: Springer Book Archive