Computer supported mathematics with \(\Omega\)MEGA. (English) Zbl 1107.68101
Summary: Classical automated theorem proving of today is based on ingenious search techniques to find a proof for a given theorem in very large search spaces – often in the range of several billion clauses. But in spite of many successful attempts to prove even open mathematical problems automatically, their use in everyday mathematical practice is still limited.
The shift from search based methods to more abstract planning techniques however opened up a paradigm for mathematical reasoning on a computer and several systems of that kind now employ a mix of interactive, search based as well as proof planning techniques.
The \(\Omega\)MEGA system is at the core of several related and well-integrated research projects of the \(\Omega\)MEGA research group, whose aim is to develop system support for a working mathematician as well as a software engineer when employing formal methods for quality assurance. In particular, \(\Omega\)MEGA supports proof development at a human-oriented abstract level of proof granularity. It is a modular system with a central proof data structure and several supplementary subsystems including automated deduction and computer algebra systems. \(\Omega\)MEGA has many characteristics in common with systems like NUPRL, CoQ, HOL, PVS, and ISABELLE. However, it differs from these systems with respect to its focus on proof planning and in that respect it is more similar to the proof planning systems CLAM and \(\lambda\)CLAM at Edinburgh.
The shift from search based methods to more abstract planning techniques however opened up a paradigm for mathematical reasoning on a computer and several systems of that kind now employ a mix of interactive, search based as well as proof planning techniques.
The \(\Omega\)MEGA system is at the core of several related and well-integrated research projects of the \(\Omega\)MEGA research group, whose aim is to develop system support for a working mathematician as well as a software engineer when employing formal methods for quality assurance. In particular, \(\Omega\)MEGA supports proof development at a human-oriented abstract level of proof granularity. It is a modular system with a central proof data structure and several supplementary subsystems including automated deduction and computer algebra systems. \(\Omega\)MEGA has many characteristics in common with systems like NUPRL, CoQ, HOL, PVS, and ISABELLE. However, it differs from these systems with respect to its focus on proof planning and in that respect it is more similar to the proof planning systems CLAM and \(\lambda\)CLAM at Edinburgh.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68W30 | Symbolic computation and algebraic computation |
Keywords:
artificial intelligence; computer-supported mathematics; proof assistant systems; interactive and automated theorem-proving; proof planning; OmegaSoftware:
Bliksem; Lambda-Clam; Leo; Omega-ANTS; LOUI; Oyster; MAYA; CLAM; Multi; Waldmeister; TRAMP; PROTEIN; Isabelle/HOL; OTTER; MBase; Coq; TPS; ML; SPASS; SATCHMO; TeXmacs; HOL; MathWeb; GAP; PVS; ActiveMath; Isabelle; TPTP; VAMPIRE; Nuprl; P.rexReferences:
| [1] | S. Allen, R. Constable, R. Eaton, C. Kreitz, L. Lorigo, The Nuprl[59]; S. Allen, R. Constable, R. Eaton, C. Kreitz, L. Lorigo, The Nuprl[59] · Zbl 0963.68532 |
| [2] | Andrews, P. B.; Bishop, M.; Issar, S.; Nesmith, D.; Pfenning, F.; Xi, H., TPS: A theorem proving system for classical type theory, J. Automat. Reason., 16, 3, 321-353 (1996) · Zbl 0858.03017 |
| [3] | S. Autexier, Hierarchical contextual reasoning, PhD thesis, Computer Science Department, Saarland University, Saarbrücken, Germany, 2003; S. Autexier, Hierarchical contextual reasoning, PhD thesis, Computer Science Department, Saarland University, Saarbrücken, Germany, 2003 |
| [4] | Autexier, S., The CoRe calculus, (Nieuwenhuis, R., Proceedings of the 20th Conference on Automated Deduction (CADE-20), Tallinn, Estonia. Proceedings of the 20th Conference on Automated Deduction (CADE-20), Tallinn, Estonia, Lecture Notes in Artificial Intelligence, vol. 3632 (2005), Springer: Springer Berlin), 84-98 · Zbl 1135.68549 |
| [5] | Autexier, S.; Benzmüller, C.; Fiedler, A.; Horacek, H.; Bao Vo, Q., Assertion-level proof representation with under-specification, Electronic Notes in Theoret. Comput. Sci., 93, 5-23 (2003) · Zbl 1271.68207 |
| [6] | Autexier, S.; Hutter, D., Maintenance of formal software development by stratified verification, (Baaz, M.; Voronkov, A., Proceedings of LPAR’02, Tbilisi, Georgia. Proceedings of LPAR’02, Tbilisi, Georgia, Lecture Notes in Computer Science (2002), Springer: Springer Berlin) · Zbl 1023.03531 |
| [7] | Autexier, S.; Hutter, D.; Mossakowski, T.; Schairer, A., The development graph manager MAYA, (Kirchner, H.; Ringeissen, C., Proceedings 9th International Conference on Algebraic Methodology and Software Technology (AMAST’02). Proceedings 9th International Conference on Algebraic Methodology and Software Technology (AMAST’02), Lecture Notes in Computer Science, vol. 2422 (2002), Springer: Springer Berlin) |
| [8] | Autexier, S.; Mossakowski, T., Integrating HOL-CASL into the development graph manager MAYA, (Armando, A., Proceedings of FROCOS’02. Proceedings of FROCOS’02, Lecture Notes in Artificial Intelligence, vol. 2309 (2002), Springer: Springer Berlin), 2-17 · Zbl 1057.68678 |
| [9] | Bartle, R.; Sherbert, D., Introduction to Real Analysis (1982), Wiley: Wiley New York · Zbl 0494.26002 |
| [10] | P. Baumgartner, U. Furbach, PROTEIN, a PROver with a theory INterface, in: [27]; P. Baumgartner, U. Furbach, PROTEIN, a PROver with a theory INterface, in: [27] |
| [11] | C. Benzmüller, Equality and extensionality in higher-order theorem proving, PhD thesis, Department of Computer Science, Saarland University, Saarbrücken, Germany, 1999; C. Benzmüller, Equality and extensionality in higher-order theorem proving, PhD thesis, Department of Computer Science, Saarland University, Saarbrücken, Germany, 1999 |
| [12] | Benzmüller, C.; Bishop, M.; Sorge, V., Integrating TPS and Ωmega, J. Universal Comput. Sci., 5, 188-207 (1999) |
| [13] | C. Benzmüller, A. Fiedler, M. Gabsdil, H. Horacek, I. Kruijff-Korbayova, M. Pinkal, J. Siekmann, D. Tsovaltzi, B. Quoc Vo, M. Wolska, Tutorial dialogs on mathematical proofs, In: Proceedings of IJCAI-03 Workshop on Knowledge Representation and Automated Reasoning for E-Learning Systems, Acapulco, Mexico, 2003, pp. 12-22; C. Benzmüller, A. Fiedler, M. Gabsdil, H. Horacek, I. Kruijff-Korbayova, M. Pinkal, J. Siekmann, D. Tsovaltzi, B. Quoc Vo, M. Wolska, Tutorial dialogs on mathematical proofs, In: Proceedings of IJCAI-03 Workshop on Knowledge Representation and Automated Reasoning for E-Learning Systems, Acapulco, Mexico, 2003, pp. 12-22 |
| [14] | C. Benzmüller, A. Fiedler, A. Meier, M. Pollet, Irrationality of \(\sqrt{2} \textsc{mega} \); C. Benzmüller, A. Fiedler, A. Meier, M. Pollet, Irrationality of \(\sqrt{2} \textsc{mega} \) |
| [15] | Benzmüller, C.; Jamnik, M.; Kerber, M.; Sorge, V., Experiments with an agent-oriented reasoning system, (Baader, F.; Brewka, G.; Eiter, T., KI 2001: Advances in Artificial Intelligence, Proceedings of Joint German/Austrian Conference on AI, Vienna, Austria. KI 2001: Advances in Artificial Intelligence, Proceedings of Joint German/Austrian Conference on AI, Vienna, Austria, Lecture Notes in Artificial Intelligence, vol. 2174 (2001), Springer: Springer Berlin), 409-424 · Zbl 1007.68710 |
| [16] | C. Benzmüller, M. Kohlhase, LEO[54]; C. Benzmüller, M. Kohlhase, LEO[54] |
| [17] | Benzmüller, C.; Meier, A.; Sorge, V., Bridging theorem proving and mathematical knowledge retrieval, (Hutter, D.; Stephan, W., Festschrift in Honour of Jörg Siekmann’s 60s Birthday. Festschrift in Honour of Jörg Siekmann’s 60s Birthday, Lecture Notes in Artificial Intelligence, vol. 2605 (2004), Springer: Springer Berlin) · Zbl 1098.68696 |
| [18] | C. Benzmüller, V. Sorge, A blackboard architecture for guiding interactive proofs, in: [46]; C. Benzmüller, V. Sorge, A blackboard architecture for guiding interactive proofs, in: [46] |
| [19] | C. Benzmüller, V. Sorge, Ωants[53]; C. Benzmüller, V. Sorge, Ωants[53] |
| [20] | Benzmüller, C.; Sorge, V.; Jamnik, M.; Kerber, M., Can a higher-order and a first-order theorem prover cooperate?, (Baader, F.; Voronkov, A., Proceedings of the 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR). Proceedings of the 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR), Lecture Notes in Artificial Intelligence, vol. 3452 (2005), Springer: Springer Berlin), 415-431 · Zbl 1108.68570 |
| [21] | Benzmüller, C. E.; Vo, Q. B., Mathematical domain reasoning tasks in natural language tutorial dialog on proofs, (Veloso, M.; Kambhampati, S., Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI-05), Pittsburgh, PA (2005), AAAI Press/MIT Press), 516-522 |
| [22] | Benzmüller, C.; Sorge, V., Critical agents supporting interactive theorem proving, (Borahona, P.; Alferes, J. J., Proceedings of the 9th Portuguese Conference on Artificial Intelligence (EPIA’99), Evora, Portugal. Proceedings of the 9th Portuguese Conference on Artificial Intelligence (EPIA’99), Evora, Portugal, Lecture Notes in Artificial Intelligence, vol. 1695 (1999), Springer: Springer Berlin), 208-221 |
| [23] | Bledsoe, W., Challenge problems in elementary calculus, J. Automat. Reason., 6, 341-359 (1990) · Zbl 0702.68092 |
| [24] | Bourbaki, N., Theory of sets, Elements of Mathematics, vol. 1 (1968), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0175.27001 |
| [25] | A. Bundy, The use of explicit plans to guide inductive proofs, in: [57]; A. Bundy, The use of explicit plans to guide inductive proofs, in: [57] · Zbl 0656.68106 |
| [26] | Bundy, A., A science of reasoning, (Plotkin, G.; Lasser, J.-L., Computational Logic: Essays in Honor of Alan Robinson (1991), MIT Press: MIT Press Cambridge, MA), 178-199 · Zbl 0793.03002 |
| [27] | (Bundy, A., Proceedings of the 12th Conference on Automated Deduction. Proceedings of the 12th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 814 (1994), Springer: Springer Berlin) · Zbl 0875.00063 |
| [28] | Bundy, A., A critique of proof planning, (Computational Logic: Logic Programming and Beyond. Computational Logic: Logic Programming and Beyond, Lecture Notes in Computer Science, vol. 2408 (2002), Springer: Springer Berlin), 160-177 · Zbl 1012.68180 |
| [29] | Bundy, A.; van Harmelen, F.; Horn, C.; Smaill, A., The Oyster-Clam system, (Stickel, M., Proceedings of the 10th Conference on Automated Deduction, Kaiserslautern, Germany. Proceedings of the 10th Conference on Automated Deduction, Kaiserslautern, Germany, Lecture Notes in Computer Science, vol. 449 (1990), Springer: Springer Berlin), 647-648 · Zbl 1509.68299 |
| [30] | Char, B.; Geddes, K.; Gonnet, G.; Leong, B.; Monagan, M.; Watt, S., First Leaves: A Tutorial Introduction to Maple V (1992), Springer: Springer Berlin · Zbl 0758.68037 |
| [31] | L. Cheikhrouhou, J. Siekmann, Planning diagonalization proofs, in: [46]; L. Cheikhrouhou, J. Siekmann, Planning diagonalization proofs, in: [46] · Zbl 0929.03020 |
| [32] | L. Cheikhrouhou, 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, 2000; L. Cheikhrouhou, 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, 2000 |
| [33] | Church, A., A formulation of the simple theory of types, J. Symbolic Logic, 5, 56-68 (1940) · JFM 66.1192.06 |
| [34] | Coq Development Team, The Coq proof assistant reference manual, INRIA, 1999-2003, see http://coq.inria.fr/doc/main.html; Coq Development Team, The Coq proof assistant reference manual, INRIA, 1999-2003, see http://coq.inria.fr/doc/main.html |
| [35] | Davis, M., The prehistory and early history of automated deduction, (Siekmann, J.; Wrightson, G., Automation of Reasoning, vol. 2, Classical Papers on Computational Logic 1967-1970 of Symbolic Computation (1983), Springer: Springer Berlin) |
| [36] | Davis, M., The early history of automated deduction, (Robinson, A.; Voronkov, A., Handbook of Automated Reasoning, vol. I (2001), Elsevier Science: Elsevier Science Amsterdam), 3-15, Chapter 1 · Zbl 1011.68511 |
| [37] | (Davis, M., The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions (2004), Dover Publications: Dover Publications New York) · Zbl 1099.03002 |
| [38] | H. de Nivelle, Bliksem 1.10 user manual, Technical Report, Max-Planck-Institut für Informatik, 1999; H. de Nivelle, Bliksem 1.10 user manual, Technical Report, Max-Planck-Institut für Informatik, 1999 |
| [39] | Fiedler, A., Dialog-driven adaptation of explanations of proofs, (Nebel, B., Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI), Seattle, WA (2001), Morgan Kaufmann: Morgan Kaufmann San Mateo, CA), 1295-1300 |
| [40] | A. Fiedler, P.rex: An interactive proof explainer, in: [48]; A. Fiedler, P.rex: An interactive proof explainer, in: [48] · Zbl 0988.68596 |
| [41] | A. Fiedler, User-adaptive proof explanation, PhD thesis, Department of Computer Science, Saarland University, Saarbrücken, Germany, 2001; A. Fiedler, User-adaptive proof explanation, PhD thesis, Department of Computer Science, Saarland University, Saarbrücken, Germany, 2001 |
| [42] | A. Franke, M. Kohlhase, System description: MBase, an open mathematical knowledge base, in: [59]; A. Franke, M. Kohlhase, System description: MBase, an open mathematical knowledge base, in: [59] · Zbl 0963.68543 |
| [43] | A. Franke, M. Kohlhase, System description: Mbase, an open mathematical knowledge base, in: [59]; A. Franke, M. Kohlhase, System description: Mbase, an open mathematical knowledge base, in: [59] · Zbl 0963.68543 |
| [44] | (Ganzinger, H., Proceedings of the 16th Conference on Automated Deduction. Proceedings of the 16th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 1632 (1999), Springer: Springer Berlin) · Zbl 0917.00015 |
| [45] | H. Gebhard, Beweisplanung für die Beweise der Vollständigkeit verschiedener Resolutionskalküle in Ωmega; H. Gebhard, Beweisplanung für die Beweise der Vollständigkeit verschiedener Resolutionskalküle in Ωmega |
| [46] | (Giunchiglia, F., Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA’98). Proceedings of 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA’98), Lecture Notes in Artificial Intelligence, vol. 1480 (1998), Springer: Springer Berlin) · Zbl 0903.00073 |
| [47] | Gordon, M.; Melham, T., Introduction to HOL—A Theorem Proving Environment for Higher Order Logic (1993), Cambridge University Press: Cambridge University Press Cambridge · Zbl 0779.68007 |
| [48] | (Goré, R.; Leitsch, A.; Nipkow, T., Automated Reasoning—1st International Joint Conference, IJCAR 2001. Automated Reasoning—1st International Joint Conference, IJCAR 2001, Lecture Notes in Artificial Intelligence, vol. 2083 (2001), Springer: Springer Berlin) · Zbl 0968.00052 |
| [49] | Hadamard, J., The Psychology of Invention in the Mathematical Field (1949), Dover Publications: Dover Publications New York, 1944 · Zbl 0063.03651 |
| [50] | Th. Hillenbrand, A. Jaeger, B. Löchner, System description: Waldmeister—improvements in performance and ease of use, in: [44]; Th. Hillenbrand, A. Jaeger, B. Löchner, System description: Waldmeister—improvements in performance and ease of use, in: [44] |
| [51] | X. Huang, Reconstructing proofs at the assertion level, in: [27]; X. Huang, Reconstructing proofs at the assertion level, in: [27] |
| [52] | Hutter, D., Management of change in structured verification, (Proceedings of Automated Software Engineering, ASE-2000 (2000), IEEE) |
| [53] | (Kerber, M.; Kohlhase, M., 8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning (Calculemus-2000) (2000), AK Peters) · Zbl 0962.00008 |
| [54] | (Kirchner, C.; Kirchner, H., Proceedings of the 15th Conference on Automated Deduction. Proceedings of the 15th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 1421 (1998), Springer: Springer Berlin) · Zbl 0892.00047 |
| [55] | (Kirchner, H.; Ringeissen, C., Frontiers of Combining systems: Third International Workshop, FroCoS 2000. Frontiers of Combining systems: Third International Workshop, FroCoS 2000, Lecture Notes in Artificial Intelligence, vol. 1794 (2000), Springer: Springer Berlin) · Zbl 0935.00044 |
| [56] | Kohlhase, M.; Franke, A., MBase: Representing knowledge and context for the integration of mathematical software systems, J. Symbolic Comput., 32, 4, 365-402 (2001), (special issue on the Integration of Computer Algebra and Deduction Systems) · Zbl 0981.68153 |
| [57] | (Lusk, E.; Overbeek, R., Proceedings of the 9th Conference on Automated Deduction, Argonne, Illinois. Proceedings of the 9th Conference on Automated Deduction, Argonne, Illinois, Lecture Notes in Computer Science, vol. 310 (1988), Springer: Springer Berlin) · Zbl 0638.00038 |
| [58] | R. Manthey, F. Bry, SATCHMO: A theorem prover implemented in Prolog, in: [57]; R. Manthey, F. Bry, SATCHMO: A theorem prover implemented in Prolog, in: [57] · Zbl 0668.68104 |
| [59] | (McAllester, D., Proceedings of the 17th Conference on Automated Deduction. Proceedings of the 17th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 1831 (2000), Springer: Springer Berlin) · Zbl 0939.00024 |
| [60] | McCune, W., Solution of the Robbins problem, J. Automat. Reason., 19, 3, 263-276 (1997) · Zbl 0883.06011 |
| [61] | W.W. McCune, Otter 3.0 reference manual and guide, Technical Report ANL-94-6, Argonne National Laboratory, Argonne, IL 60439, USA, 1994; W.W. McCune, Otter 3.0 reference manual and guide, Technical Report ANL-94-6, Argonne National Laboratory, Argonne, IL 60439, USA, 1994 |
| [62] | A. Meier, TRAMP: Transformation of machine-found proofs into natural deduction proofs at the assertion level, in: [59]; A. Meier, TRAMP: Transformation of machine-found proofs into natural deduction proofs at the assertion level, in: [59] · Zbl 0963.68537 |
| [63] | A. Meier, Proof planning with multiple strategies, PhD thesis, Department of Computer Science, Saarland University, Saarbrücken, Germany, 2004; A. Meier, Proof planning with multiple strategies, PhD thesis, Department of Computer Science, Saarland University, Saarbrücken, Germany, 2004 · Zbl 0983.68531 |
| [64] | Meier, A.; Melis, E., Multi: A multi-strategy proof planner (system description), (Nieuwenhuis, R., Proceedings of the 20th Conference on Automated Deduction (CADE-20), Tallinn, Estonia. Proceedings of the 20th Conference on Automated Deduction (CADE-20), Tallinn, Estonia, Lecture Notes in Artificial Intelligence, vol. 3632 (2005), Springer: Springer Berlin), 250-254 · Zbl 1135.68557 |
| [65] | A. Meier, E. Melis, M. Pollet, Towards extending domain representations, Seki Report SR-02-01, Department of Computer Science, Saarland University, Saarbrücken, Germany, 2002; A. Meier, E. Melis, M. Pollet, Towards extending domain representations, Seki Report SR-02-01, Department of Computer Science, Saarland University, Saarbrücken, Germany, 2002 |
| [66] | Meier, A.; Pollet, M.; Sorge, V., Classifying isomorphic residue classes, (Moreno-Diaz, R.; Buchberger, B.; Freire, L., A Selection of Papers from the 8th International Workshop on Computer Aided Systems Theory (EuroCAST 2001). A Selection of Papers from the 8th International Workshop on Computer Aided Systems Theory (EuroCAST 2001), Lecture Notes in Computer Science, vol. 2178 (2001), Springer: Springer Berlin), 494-508 · Zbl 1023.68883 |
| [67] | Meier, A.; Pollet, M.; Sorge, V.; Linton, S.; Sebastiani, R., Comparing approaches to the exploration of the domain of residue classes, J. Symbolic Comput., 34, 4, 287-306 (2002), (special issue on the Integration of Automated Reasoning and Computer Algebra Systems) · Zbl 1038.68110 |
| [68] | A. Meier, V. Sorge, Exploring properties of residue classes, in: [53]; A. Meier, V. Sorge, Exploring properties of residue classes, in: [53] · Zbl 0986.68132 |
| [69] | A. Meier, E. Melis, J. Siekmann, Proof planning with multiple strategies, Artificial Intelligence, submitted for publication; A. Meier, E. Melis, J. Siekmann, Proof planning with multiple strategies, Artificial Intelligence, submitted for publication · Zbl 1182.68259 |
| [70] | E. Melis, Island planning and refinement, Seki-Report SR-96-10, Department of Computer Science, Saarland University, Saarbrücken, Germany, 1996; E. Melis, Island planning and refinement, Seki-Report SR-96-10, Department of Computer Science, Saarland University, Saarbrücken, Germany, 1996 |
| [71] | Melis, E., AI-techniques in proof planning, (Prade, H., Proceedings of the 13th European Conference on Artificial Intelligence, Brighton, UK (1998), John Wiley & Sons: John Wiley & Sons Chichester, UK), 494-498 |
| [72] | Melis, E., AI-techniques in proof planning, (European Conference on Artificial Intelligence, Brighton, UK (1998), Kluwer, Dordrecht), 494-498 |
| [73] | Melis, E.; Meier, A., Proof planning with multiple strategies, (Loyd, J.; Dahl, V.; Furbach, U.; Kerber, M.; Lau, K.; Palamidessi, C.; Pereira, L. M.; Sagivand, Y.; Stuckey, P., First International Conference on Computational Logic (CL-2000), London, UK. First International Conference on Computational Logic (CL-2000), London, UK, Lecture Notes in Artificial Intelligence, vol. 1861 (2000), Springer: Springer Berlin), 644-659 · Zbl 0983.68531 |
| [74] | Melis, E.; Siekmann, J., Knowledge-based proof planning, Artificial Intelligence, 115, 1, 65-105 (1999) · Zbl 0939.68822 |
| [75] | Melis, E.; Siekmann, J., Activemath: An Intelligent Tutoring System for Mathematics, vol. 3070 (2004), Springer: Springer Berlin, pp. 91-101 · Zbl 1058.97500 |
| [76] | E. Melis, J. Zimmer, T. Müller, Integrating constraint solving into proof planning, in: [55]; E. Melis, J. Zimmer, T. Müller, Integrating constraint solving into proof planning, in: [55] · Zbl 0962.68151 |
| [77] | Mossakowski, T.; Autexier, S.; Hutter, D., Extending development graphs with hiding, (Hussmann, H., Proceedings of Fundamental Approaches to Software Engineering (FASE 2001), Genova. Proceedings of Fundamental Approaches to Software Engineering (FASE 2001), Genova, Lecture Notes in Computer Science, vol. 2029 (2001), Springer: Springer Berlin), 269-283 · Zbl 0977.68657 |
| [78] | Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-Order Logic, (Lecture Notes in Computer Science, vol. 2283 (2002), Springer: Springer Berlin) · Zbl 0994.68131 |
| [79] | Owre, S.; Rajan, S.; Rushby, J. M.; Shankar, N.; Srivas, M., PVS: Combining specification, proof checking, and model checking, (Alur, R.; Henzinger, T., Computer-Aided Verification, CAV ’96, New Brunswick, NJ. Computer-Aided Verification, CAV ’96, New Brunswick, NJ, Lecture Notes in Computer Science, vol. 1102 (1996), Springer: Springer Berlin), 411-414 |
| [80] | Paulson, L., Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol. 828 (1994), Springer: Springer Berlin · Zbl 0825.68059 |
| [81] | Polya, G., How to Solve it (1973), Princeton University Press: Princeton University Press Princeton, NJ · Zbl 1109.00301 |
| [82] | A. Riazanov, A. Voronkov, Vampire 1.1 (system description), in: [48]; A. Riazanov, A. Voronkov, Vampire 1.1 (system description), in: [48] · Zbl 0988.68607 |
| [83] | J. Richardson, A. Smaill, I. Green, System description: Proof planning in higher-order logic with Λ;[54]; J. Richardson, A. Smaill, I. Green, System description: Proof planning in higher-order logic with Λ;[54] |
| [84] | Robinson, J. A., A machine-oriented logic based on the resolution principle, J. ACM, 12, 1, 23-41 (1965) · Zbl 0139.12303 |
| [85] | Schönert, M., GAP—Groups, Algorithms, Programming, Lehrstuhl D für Mathematik (1995), Rheinisch Westfälische Technische Hochschule: Rheinisch Westfälische Technische Hochschule Aachen, Germany |
| [86] | Siekmann, J., Geschichte des Automatischen Beweisens, (Deduktionssysteme, Automatisierung des Logischen Denkens (1992), R. Oldenbourg Verlag), also in English with Elsewood |
| [87] | Siekmann, J., History of computational logic, (Gabbay, D.; Woods, J., The Handbook of the History of Logic, vols. I-IX (2004), Elsevier: Elsevier Amsterdam) · Zbl 0112.40802 |
| [88] | Siekmann, J.; Benzmüller, C.; Fiedler, A.; Meier, A.; Normann, I.; Pollet, M., Proof development in OMEGA: The irrationality of square root of 2, (Kamareddine, F., Thirty Five Years of Automating Mathematics. Thirty Five Years of Automating Mathematics, Kluwer Applied Logic Series, vol. 28 (2003), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht), 271-314 · Zbl 1063.68093 |
| [89] | Siekmann, J.; Benzmüller, C.; Fiedler, A.; Meier, A.; Pollet, M., Proof development with OMEGA: Sqrt(2) is irrational, (Baaz, M.; Voronkov, A., Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002. Logic for Programming, Artificial Intelligence, and Reasoning, 9th International Conference, LPAR 2002, Lecture Notes in Artificial Intelligence, vol. 2514 (2002), Springer: Springer Berlin), 367-387 · Zbl 1023.68660 |
| [90] | Siekmann, J.; Hess, S.; Benzmüller, C.; Cheikhrouhou, L.; Fiedler, A.; Horacek, H.; Kohlhase, M.; Konrad, K.; Meier, A.; Melis, E.; Pollet, M.; Sorge, V., \(LOUI\): \(L\) ovely Ω \(\textsc{mega}U\) ser \(I\) nterface, Formal Aspects of Computing, 11, 326-342 (1999) |
| [91] | V. Sorge, Non-trivial computations in proof planning, in: [55]; V. Sorge, Non-trivial computations in proof planning, in: [55] · Zbl 0962.68152 |
| [92] | V. Sorge, ΩANTS; V. Sorge, ΩANTS |
| [93] | G. Sutcliffe, C. Suttner, T. Yemenis, The TPTP problem library, in: [27]; G. Sutcliffe, C. Suttner, T. Yemenis, The TPTP problem library, in: [27] · Zbl 0910.68197 |
| [94] | J. van der Hoeven, GNU TeXmacs: A free, structured, wysiwyg and technical text editor, in: Actes du congrès Gutenberg, Metz, Actes du congrès Gutenberg, vols. 39-40, May 2001, pp. 39-50; J. van der Hoeven, GNU TeXmacs: A free, structured, wysiwyg and technical text editor, in: Actes du congrès Gutenberg, Metz, Actes du congrès Gutenberg, vols. 39-40, May 2001, pp. 39-50 |
| [95] | C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, Th. Engel, E. Keen, C. Theobalt, D. Topic, System description: SPASS version 1.0.0, in: [44]; C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, Th. Engel, E. Keen, C. Theobalt, D. Topic, System description: SPASS version 1.0.0, in: [44] |
| [96] | Weld, D., An introduction to least commitment planning, AI Magazine, 15, 4, 27-61 (1994) |
| [97] | F. Wiedijk, The Seventeen Provers of the World, in: Lecture Notes in Artificial Intelligence, Springer, Berlin, 2005, in press; F. Wiedijk, The Seventeen Provers of the World, in: Lecture Notes in Artificial Intelligence, Springer, Berlin, 2005, in press · Zbl 1084.68119 |
| [98] | Zhang, J.; Zhang, H., SEM: A system for enumerating models, (Mellish, C. S., Proceedings of the 14th International Joint Conference on Artificial Intelligence (IJCAI), Montreal, Canada (1995), Morgan Kaufmann: Morgan Kaufmann San Mateo, CA), 298-303 |
| [99] | Zimmer, J.; Kohlhase, M., System description: The Mathweb software bus for distributed mathematical reasoning, (Voronkov, A., Proceedings of the 18th International Conference on Automated Deduction. Proceedings of the 18th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 2392 (2002), Springer: Springer Berlin), 138-142 · Zbl 1072.68601 |
| [100] | Zimmer, J.; Melis, E., Constraint solving for proof planning, J. Automat. Reason., 33, 51-88 (2004) · Zbl 1071.68093 |
| [101] | Zimmer, J., A framework for agent-based brokering of reasoning services, (Monroy, R.; Arroyo-Figueroa, G.; Sucar, L. E.; Azuela, J. H.S., MICAI. MICAI, Lecture Notes in Computer Science, vol. 2972 (2004), Springer: Springer Berlin) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
