×

Theorema: Towards computer-aided mathematical theory exploration. (English) Zbl 1107.68095

Summary: Theorema is a project that aims at supporting the entire process of mathematical theory exploration within one coherent logic and software system. This survey paper illustrates the style of Theorema-supported mathematical theory exploration by a case study (the automated synthesis of an algorithm for the construction of Gröbner bases) and gives an overview on some reasoners and organizational tools for theory exploration developed in the Theorema project.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
13P10 Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Asperti, A.; Padovani, L.; Sacerdoti Coen, C.; Guidi, F.; Schena, I., Mathematical knowledge management in HELM, Ann. Math. Artificial Intelligence, 38, 1, 27-46 (2003) · Zbl 1025.68080
[2] Bachmair, L.; Dershowitz, N.; Plaisted, D., Completion without failure, (Aït-Kaci, H.; Nivat, M., Resolution of Equations in Algebraic Structures, vol. 2 (1989), Elsevier Science: Elsevier Science Amsterdam), 1-30
[3] Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Nilsson, J. F., Synthesis of programs in computational logic, (Bruynooghe, M.; Lau, K.-K., Program Development in Computational Logic. Program Development in Computational Logic, Lecture Notes in Comput. Sci., vol. 3049 (2004), Springer: Springer Berlin), 30-65 · Zbl 1080.68562
[4] Bertot, Y.; Castèran, P., Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions, Texts in Theoretical Computer Science, An EATCS Series (2004), Springer: Springer Berlin · Zbl 1069.68095
[5] Bledsoe, W., Challenge problems in elementary analysis, J. Automat. Reason., 6, 341-359 (1990) · Zbl 0702.68092
[6] A. Buch, T. Hillenbrand, Waldmeister: Development of a high preformance completion based theorem prover, SEKI-Report SR-96-01, University of Kaiserslautern, Germany, 1996; A. Buch, T. Hillenbrand, Waldmeister: Development of a high preformance completion based theorem prover, SEKI-Report SR-96-01, University of Kaiserslautern, Germany, 1996
[7] B. Buchberger, An algorithm for finding the basis elements in the residue class ring modulo a zero dimensional polynomial ideal, PhD thesis, Mathematical Institute, University of Innsbruck, Austria, 1965, in German; B. Buchberger, An algorithm for finding the basis elements in the residue class ring modulo a zero dimensional polynomial ideal, PhD thesis, Mathematical Institute, University of Innsbruck, Austria, 1965, in German · Zbl 1245.13020
[8] Buchberger, B., Gröbner-bases: An algorithmic method in polynomial ideal theory, (Bose, N. K., Multidimensional Systems Theory (1985), Reidel Publishing Company: Reidel Publishing Company Dordrecht), 184-232 · Zbl 0587.13009
[9] Buchberger, B., Symbolic computation: Computer algebra and logic, (Baader, F.; Schulz, K. U., Frontiers of Combining Systems. Frontiers of Combining Systems, Applied Logic Series, vol. 3 (1996), Kluwer Academic Publishers: Kluwer Academic Publishers Dordrecht), 193-219 · Zbl 0894.68086
[10] B. Buchberger, Introduction to Gröbner bases, in: [21]; B. Buchberger, Introduction to Gröbner bases, in: [21] · Zbl 0941.13017
[11] Buchberger, B., Theory exploration versus theorem proving, (Armando, A.; Jebelean, T., Proc. of Calculemus’99. Proc. of Calculemus’99, ENTCS, vol. 23 (1999), Elsevier: Elsevier Amsterdam) · Zbl 0958.68156
[12] Buchberger, B., Theory exploration with Theorema, Analele Universităţii din Timişoara, Ser. Matematică-Informatică, 38, 2, 9-32 (2000) · Zbl 1004.68589
[13] B. Buchberger, Algorithm invention and verification by Lazy Thinking, in: [65]; B. Buchberger, Algorithm invention and verification by Lazy Thinking, in: [65] · Zbl 1073.68814
[14] B. Buchberger, Algorithm-supported mathematical theory exploration: A personal view and strategy, in: [16]; B. Buchberger, Algorithm-supported mathematical theory exploration: A personal view and strategy, in: [16] · Zbl 1109.68664
[15] Buchberger, B., Towards the automated synthesis of a Gröbner bases algorithm, RACSAM (Review of the Spanish Royal Academy of Sciences), 98, 1, 65-75 (2004) · Zbl 1088.68187
[16] (Buchberger, B.; Campbell, J. A., Proc. of the 7th Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC’04, Hagenberg, Austria. Proc. of the 7th Int. Conf. on Artificial Intelligence and Symbolic Computation, AISC’04, Hagenberg, Austria, Lecture Notes in Artif. Intell., vol. 3249 (2004), Springer: Springer Berlin)
[17] Buchberger, B.; Crăciun, A., Algorithm synthesis by Lazy Thinking: Examples and implementation in Theorema, (Kamareddine, F., Proc. of the Mathematical Knowledge Management Workshop, Edinburgh. Proc. of the Mathematical Knowledge Management Workshop, Edinburgh, ENTCS, vol. 93 (2003), Elsevier: Elsevier Amsterdam), 24-59 · Zbl 1271.68208
[18] B. Buchberger, A. Crăciun, Algorithm synthesis by Lazy Thinking: Using problem schemes, in: [66]; B. Buchberger, A. Crăciun, Algorithm synthesis by Lazy Thinking: Using problem schemes, in: [66]
[19] B. Buchberger, C. Dupré, T. Jebelean, F. Kriftner, K. Nakagawa, D. Văsaru, W. Windsteiger, The Theorema project: A progress report, in: [44]; B. Buchberger, C. Dupré, T. Jebelean, F. Kriftner, K. Nakagawa, D. Văsaru, W. Windsteiger, The Theorema project: A progress report, in: [44] · Zbl 1017.68110
[20] Buchberger, B.; Jebelean, T.; Kriftner, F.; Marin, M.; Tomuţa, E.; Văsaru, D., A survey of the Theorema project, (Küchlin, W., Proc. of the Int. Symposium on Symbolic and Algebraic Computation ISSAC’97 (1997), ACM Press: ACM Press New York), 384-391 · Zbl 0926.68131
[21] Buchberger, B.; Winkler, F., Gröbner Bases and Applications (1998), Cambridge University Press: Cambridge University Press Cambridge, UK, Proc. of the Int. Conf. “33 Years of Gröbner Bases”, RISC, Austria, London Mathematical Society Lecture Note Series, vol. 251, 1998
[22] Caprotti, O.; Carlisle, D., OpenMath and MathML: Semantic mark up for mathematics, ACM Crossroads, 6, 2 (1999), special issue on Markup Languages
[23] Chou, S. C., Mechanical Geometry Theorem Proving (1975), Reidel: Reidel Dordrecht, Boston
[24] Chou, S. C.; Gao, X. S.; Zhang, J. Z., Automated production of traditional proofs in euclidian geometry, (Proc. of 8th IEEE Symposium on Logic in Computer Science (1993), IEEE Computer Society Press), 48-56
[25] Coddington, E. A.; Levinson, N., Theory of Ordinary Differential Equations (1955), McGraw-Hill Book Company: McGraw-Hill Book Company New York · Zbl 0064.33002
[26] Collins, G. E., Quantifier elimination for real closed fields by cylindrical algebraic decomposition, (Second GI Conf. on Authomata Theory and Formal Languages. Second GI Conf. on Authomata Theory and Formal Languages, Lecture Notes in Comput. Sci., vol. 33 (1975), Springer: Springer Berlin), 134-183
[27] Constable, R., Implementing Mathematics Using the Nuprl Proof Development System (1986), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ
[28] A. Crăciun, B. Buchberger, Preprocessed Lazy Thinking: Synthesis of sorting algorithms, Technical Report 04-17, RISC, Linz, Austria, 2004; A. Crăciun, B. Buchberger, Preprocessed Lazy Thinking: Synthesis of sorting algorithms, Technical Report 04-17, RISC, Linz, Austria, 2004
[29] J. W. de Bakker, D. Scott, A theory of programs, in: IBM Seminar, Vienna, Austria, 1969; J. W. de Bakker, D. Scott, A theory of programs, in: IBM Seminar, Vienna, Austria, 1969
[30] de Nivelle, H., Bliksem resolution prover (1999), Available to download from
[31] J. Denzinger, S. Schulz, Analysis and representation of equational proofs generated by a distributed completion based proof system, SEKI-Report SR-94-05, University of Kaiserslautern, Germany, 1994; J. Denzinger, S. Schulz, Analysis and representation of equational proofs generated by a distributed completion based proof system, SEKI-Report SR-94-05, University of Kaiserslautern, Germany, 1994
[32] Dijkstra, E. W., A Discipline of Programming (1976), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ · Zbl 0368.68005
[33] B. Elspas, M.W. Green, K.N. Lewitt, R.J. Waldinger, Research in interactive program—proving techniques, Technical Report, Stanford Research Institute, Menlo Park, CA, USA, May 1972; B. Elspas, M.W. Green, K.N. Lewitt, R.J. Waldinger, Research in interactive program—proving techniques, Technical Report, Stanford Research Institute, Menlo Park, CA, USA, May 1972
[34] Flener, P.; Lau, K.-K.; Ornaghi, M.; Richardson, J. D.C., An abstract formalization of correct schemas for program synthesis, J. Symbolic Comput., 30, 1, 93-127 (2000) · Zbl 0959.68013
[35] (Ganzinger, H., Proc. of the 16th Int. Conf. on Automated Deduction, CADE’99, Trento, Italy. Proc. of the 16th Int. Conf. on Automated Deduction, CADE’99, Trento, Italy, Lecture Notes in Artif. Intell., vol. 1632 (1999), Springer: Springer Berlin)
[36] Gosper, R. W., Decision procedures for indefinite hypergeometric summation, Proc. Nat. Acad. Sci. USA, 75, 5-6, 40-42 (1978) · Zbl 0384.40001
[37] J. Harrison, Metatheory and reflection in theorem proving: A survey and critique, Technical Report CRC-053, SRI Cambridge, UK, 1995; J. Harrison, Metatheory and reflection in theorem proving: A survey and critique, Technical Report CRC-053, SRI Cambridge, UK, 1995
[38] K. Hodgson, J. Slaney, Semantic guidance for saturation-based theorem proving, TR-ARP 04-2000, Automated Reasoning Project, Australian National University, Canberra, Australia, 2000; K. Hodgson, J. Slaney, Semantic guidance for saturation-based theorem proving, TR-ARP 04-2000, Automated Reasoning Project, Australian National University, Canberra, Australia, 2000
[39] Ireland, A.; Bundy, A., Productive use of failure in inductive proof, J. Automat. Reason., 16, 1-2, 79-111 (1996) · Zbl 0847.68103
[40] T. Jebelean, Natural proofs in elementary analysis by S-decomposition, Technical Report 01-33, RISC, Linz, Austria, 2001; T. Jebelean, Natural proofs in elementary analysis by S-decomposition, Technical Report 01-33, RISC, Linz, Austria, 2001 · Zbl 1110.68495
[41] T. Jebelean, L. Kovács, N. Popov, Experimental program verification in Theorema, in: Proc. of the 1st Int. Symposium on Leveraging Applications of Formal Methods, ISOLA’04, 2004; T. Jebelean, L. Kovács, N. Popov, Experimental program verification in Theorema, in: Proc. of the 1st Int. Symposium on Leveraging Applications of Formal Methods, ISOLA’04, 2004
[42] Kamke, E., Differentialgleichungen und Lösungsmethoden, vol. 1 (1983), Teubner: Teubner Stuttgart · Zbl 0026.31801
[43] Kapur, D., Using Gröbner bases to reason about geometry problems, J. Symbolic Computation, 2, 399-408 (1986) · Zbl 0629.68087
[44] M. Kerber, M. Kohlhase (Eds.), Proc. of Calculemus’2000, St. Andrews, UK, 2000; M. Kerber, M. Kohlhase (Eds.), Proc. of Calculemus’2000, St. Andrews, UK, 2000
[45] M. Kirchner, Program verification with the mathematical software system Theorem, Technical Report 99-16, RISC, Linz, Austria, 1999; M. Kirchner, Program verification with the mathematical software system Theorem, Technical Report 99-16, RISC, Linz, Austria, 1999
[46] Kohlhase, M., OMDoc: An infrastructure for OpenMath content dictionary information, ACM SIGSAM Bull., 34, 2, 43-48 (2000)
[47] B. Konev, T. Jebelean, Using meta-variables for natural deduction in Theorema, in: [44]; B. Konev, T. Jebelean, Using meta-variables for natural deduction in Theorema, in: [44] · Zbl 0986.68131
[48] L. Kovács, T. Jebelean, Automated generation of loop invariants by recurrence solving in Theorema, in: [66]; L. Kovács, T. Jebelean, Automated generation of loop invariants by recurrence solving in Theorema, in: [66]
[49] Kraan, I.; Basin, D.; Bundy, A., Middle-out reasoning for synthesis and induction, J. Automat. Reason., 16, 1-2, 113-145 (1996) · Zbl 0847.68104
[50] Krall, A. M., Applied Analysis (1986), D. Reidel Publishing Company: D. Reidel Publishing Company Dordrecht · Zbl 0618.46001
[51] Kutsia, T., Equational prover of Theorema, (Nieuwenhuis, R., Proc. of the 14th Int. Conf. on Rewriting Techniques and Applications, RTA’03, Valencia, Spain. Proc. of the 14th Int. Conf. on Rewriting Techniques and Applications, RTA’03, Valencia, Spain, Lecture Notes in Comput. Sci., vol. 2706 (2003), Springer: Springer Berlin), 367-379 · Zbl 1038.68570
[52] T. Kutsia, Solving equations involving sequence variables and sequence functions, in: [16]; T. Kutsia, Solving equations involving sequence variables and sequence functions, in: [16] · Zbl 1109.68579
[53] Kutsia, T.; Buchberger, B., Predicate logic with sequence variables and sequence function symbols, (Asperti, A.; Bancerek, G.; Trybulec, A., Proc. of the 3rd Int. Conf. on Mathematical Knowledge Management. Proc. of the 3rd Int. Conf. on Mathematical Knowledge Management, Lecture Notes in Comput. Sci., vol. 3119 (2004), Springer: Springer Berlin), 205-219 · Zbl 1109.68111
[54] T. Kutsia, K. Nakagawa, An interface between Theorema and external automated deduction systems, Technical Report 00-29, RISC, Linz, 2000; T. Kutsia, K. Nakagawa, An interface between Theorema and external automated deduction systems, Technical Report 00-29, RISC, Linz, 2000
[55] Kutzler, B.; Stifter, S., On the application of Buchberger’s Algorithm to automated geometry theorem proving, J. Symbolic Comput., 2, 389-397 (1986) · Zbl 0629.68086
[56] Letz, R.; Schumann, J.; Bayerl, S.; Bibel, W., Setheo: A high-performance theorem prover, J. Automat. Reason., 8, 2, 183-212 (1992) · Zbl 0759.68080
[57] Loeckx, J.; Sieber, K., The Foundations of Program Verification (1987), Teubner: Teubner Stuttgart · Zbl 0625.68017
[58] W. McCune, Otter 3.0 reference manual and guide, ANL-TR 94/6, Argonne National Laboratory, Argonne, USA, 1994; W. McCune, Otter 3.0 reference manual and guide, ANL-TR 94/6, Argonne National Laboratory, Argonne, USA, 1994
[59] McCune, W., EQP (1999), Available from
[60] W. McCune, Mace 2.0 user manual and guide, Technical memorandum ANL/MCS-TM 249, Argonne National Laboratory, Argonne, USA, 2001; W. McCune, Mace 2.0 user manual and guide, Technical memorandum ANL/MCS-TM 249, Argonne National Laboratory, Argonne, USA, 2001
[61] Mellis, E.; Siekmann, J., Knowledge-based proof planning, Artificial Intelligence, 115, 1, 65-105 (1999) · Zbl 0939.68822
[62] K. Nakagawa, Supporting user-friendliness in the mathematical software system Theorema, PhD thesis, RISC, Johannes Kepler University, Linz, Austria, 2002; K. Nakagawa, Supporting user-friendliness in the mathematical software system Theorema, PhD thesis, RISC, Johannes Kepler University, Linz, Austria, 2002
[63] (Nashed, M. Z., Generalized Inverses and Applications, Proc. of an Advanced Seminar Sponsored by the Mathematics Research Center (1976), Academic Press: Academic Press New York) · Zbl 0346.15001
[64] Paule, P.; Schorn, M., A Mathematica version of Zeilberger’s algorithm for proving binomial coefficient identities, J. Symbolic Comput., 20, 5-6, 673-698 (1995) · Zbl 0851.68052
[65] (Petcu, D.; Negru, V.; Zaharie, D.; Jebelean, T., Proc. of SYNASC’03, 5th Int. Workshop on Symbolic and Numeric Algorithms for Scientific Computing, Timişoara, Romania (2003), Mirton)
[66] (Petcu, D.; Negru, V.; Zaharie, D.; Jebelean, T., Proc. of SYNASC’04, 6th Int. Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timişoara, Romania (2004), Mirton)
[67] F. Piroi, Tools for using automated provers in mathematical theory exploration, PhD thesis, RISC, Johannes Kepler University, Linz, Austria, August 2004; F. Piroi, Tools for using automated provers in mathematical theory exploration, PhD thesis, RISC, Johannes Kepler University, Linz, Austria, August 2004
[68] F. Piroi, B. Buchberger, An environment for building mathematical knowledge libraries, in: C. Benzmüller, W. Windsteiger (Eds.), Proc. of the first Workshop on Computer-Supported Mathematical Theory Development, IJCAR’04, Cork, Ireland, 2004, pp. 19-29; F. Piroi, B. Buchberger, An environment for building mathematical knowledge libraries, in: C. Benzmüller, W. Windsteiger (Eds.), Proc. of the first Workshop on Computer-Supported Mathematical Theory Development, IJCAR’04, Cork, Ireland, 2004, pp. 19-29
[69] F. Piroi, B. Buchberger, Label management in mathematical theories, Technical Report 2004-16, RICAM, Linz, Austria, 2004; F. Piroi, B. Buchberger, Label management in mathematical theories, Technical Report 2004-16, RICAM, Linz, Austria, 2004
[70] N. Popov, Verification of simple recursive programs: Sufficient conditions, Technical Report 04-06, RISC, Linz, Austria, 2004; N. Popov, Verification of simple recursive programs: Sufficient conditions, Technical Report 04-06, RISC, Linz, Austria, 2004
[71] A. Riazanov, A. Voronkov, Vampire, in: [35]; A. Riazanov, A. Voronkov, Vampire, in: [35]
[72] J. Robu, Systematic exploration of geometric configurations using Theorema based on Mathematica, in: Proc. of 3rd Int. Workshop on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC’01, Timişoara, Romania, 2001, pp. 209-216; J. Robu, Systematic exploration of geometric configurations using Theorema based on Mathematica, in: Proc. of 3rd Int. Workshop on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC’01, Timişoara, Romania, 2001, pp. 209-216 · Zbl 1048.68596
[73] J. Robu, Automated geometric theorem proving, PhD thesis, RISC, Johannes Kepler University, Linz, Austria, 2002; J. Robu, Automated geometric theorem proving, PhD thesis, RISC, Johannes Kepler University, Linz, Austria, 2002
[74] Rodriguez-Carbonell, E.; Kapur, D., Automatic generation of polynomial loop invariants: Algebraic foundations, (Proc. of the Int. Symposium on Symbolic and Algebraic Computation, ISSAC’04, Santander, Spain (2004), ACM Press, New York), 266-273 · Zbl 1108.13310
[75] M. Rosenkranz, A polynomial approach to linear boundary value problems, PhD thesis, RISC, Johannes Kepler University, Linz, Austria, September 2003; M. Rosenkranz, A polynomial approach to linear boundary value problems, PhD thesis, RISC, Johannes Kepler University, Linz, Austria, September 2003
[76] M. Rosenkranz, The algorithmization of physics: Math between science and engineering, in: [16]; M. Rosenkranz, The algorithmization of physics: Math between science and engineering, in: [16] · Zbl 1109.68698
[77] Rosenkranz, M., A new symbolic method for solving linear two-point boundary value problems on the level of operators, J. Symbolic Comput., 39, 2, 171-199 (2005) · Zbl 1126.68104
[78] M. Rosenkranz, B. Buchberger, H.W. Engl, A symbolic algorithm for solving two-point BVPs on the operator, SFB Report 2003-41, Johannes Kepler University, Linz, Austria, 2003; M. Rosenkranz, B. Buchberger, H.W. Engl, A symbolic algorithm for solving two-point BVPs on the operator, SFB Report 2003-41, Johannes Kepler University, Linz, Austria, 2003
[79] Sandhu, P., The MathML Handbook (2002), Charles River Media
[80] Schulz, S., E—a brainiac theorem prover, J. AI Comm., 15, 2/3, 111-126 (2002) · Zbl 1020.68084
[81] Siekmann, J.; Benzmüller, C., Omega: Computer supported mathematics, (Biundo, S.; Frühwirth, T.; Palm, G., Proc. of the 27th German Conf. on Artificial Intelligence, KI’04, Ulm, Germany. Proc. of the 27th German Conf. on Artificial Intelligence, KI’04, Ulm, Germany, Lecture Notes in Comput. Sci., vol. 3238 (2004), Springer: Springer Berlin), 3-28 · Zbl 1132.68682
[82] 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: Lovely Omega User Interface, Formal Aspects of Computing, 11, 3, 326-342 (1999)
[83] Smith, D. R., Mechanizing the development of software, (Broy, M.; Steinbrueggen, R., Calculational System Design, Proc. of the NATO Advanced Study Institute (1999), IOS Press: IOS Press Amsterdam), 251-292 · Zbl 0945.68023
[84] Stakgold, I., Green’s Functions and Boundary Value Problems (1979), John Wiley & Sons: John Wiley & Sons New York · Zbl 0421.34027
[85] Stanley, R. P., Differentiably finite power series, European J. Combin., 1, 2, 175-188 (1980) · Zbl 0445.05012
[86] Sutcliffe, G.; Suttner, C., The TPTP problem library: CNF Release v1.2.1, J. Automat. Reason., 21, 2, 177-203 (1998) · Zbl 0910.68197
[87] Tammet, T., Gandalf, J. Automat. Reason., 18, 2, 199-204 (1997)
[88] Trybulec, A.; Blair, H. A., Computer aider reasoning, (Parikh, R., Proc. of the Conf. Logic of Programs. Proc. of the Conf. Logic of Programs, Lecture Notes in Comput. Sci., vol. 193 (1985), Springer: Springer Berlin), 406-412
[89] Warren, D. H.D., Higher-order extensions of Prolog: are they needed?, (Machine Intelligence, vol. 10 (1982), Edinburgh University Press: Edinburgh University Press Edinburgh, UK), 441-454
[90] C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, T. Engel, E. Keen, C. Theobalt, D. Topic, System abstract: Spass version 1.0.0. in: [35]; C. Weidenbach, B. Afshordel, U. Brahm, C. Cohrs, T. Engel, E. Keen, C. Theobalt, D. Topic, System abstract: Spass version 1.0.0. in: [35]
[91] Wiedijk, F., Comparing mathematical provers, (Asperti, A.; Buchberger, B.; Davenport, J. H., Proc. of the Second Int. Conf. on Mathematical Knowledge Management, Bertinoro, Italy (2003), Springer: Springer Berlin), 188-202 · Zbl 1022.68623
[92] W. Windsteiger, A set theory prover in Theorema: Implementation and practical applications, PhD thesis, RISC, Johannes Kepler University, Linz, Austria, May 2001; W. Windsteiger, A set theory prover in Theorema: Implementation and practical applications, PhD thesis, RISC, Johannes Kepler University, Linz, Austria, May 2001 · Zbl 1023.68662
[93] Wolfram, S., The Mathematica Book (2003), Wolfram Media Inc.
[94] Wu, W. T., Basic principles of mechanical theorem proving in elementary geometries, J. Automat. Reason., 2, 221-252 (1986) · Zbl 0642.68163
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.