## Abstract

Observing is the process of obtaining new knowledge, expressed in language, by bringing the senses in contact with reality. Reasoning, in contrast, is the process of obtaining new knowledge from given knowledge, by applying certain general transformation rules that depend only on the *form* of the knowledge and can be done exclusively in the brain without involving the senses. Observation and reasoning, together, form the basis of the scientific method for explaining reality. Automated reasoning is the science of establishing methods that allow to replace human step-wise reasoning by procedures that perform individual reasoning steps mechanically and are able to find, automatically, suitable sequences of reasoning steps for deriving new knowledge from given one.

## Keywords

Theorem Prove Function Symbol Symbolic Computation Symbolic Execution Theorema Project## References

- [AH77]K. Appel and W. Haken. Solution of the four color map problem.
*Scientific American*, 237:108–121, October 1977.MathSciNetCrossRefGoogle Scholar - [BB04]C. Barrett and S. Berezin. CVC Lite: A New Implementation of the Cooperating Validity Checker. In
*Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, July 13–17, 2004*, volume 3114 of*LNCS*, pages 515–518. Springer, 2004.Google Scholar - [BCJ+06]B. Buchberger, A. Craciun, T. Jebelean, L. Kovacs, T. Kutsia, K. Nakagawa, F. Piroi, N. Popov, J. Robu, M. Rosenkranz, and W. Windsteiger. Theorema: Towards Computer-Aided Mathematical Theory Exploration.
*Journal of Applied Logic*, 4(4):470–504, 2006.zbMATHCrossRefMathSciNetGoogle Scholar - [BDF+04]D. Basin, Y. Deville, P. Flener, A. Hamfelt, and J. F. Nilsson. Synthesis of Programs in Computational Logic. In M. Bruynooghe and K. K. Lau, editors,
*Program Development in Computational Logic*, volume 3049 of*Lecture Notes in Computer Science*, pages 30–65. Springer, 2004.Google Scholar - [BDJ+00]B. Buchberger, C. Dupre, T. Jebelean, F. Kriftner, K. Nakagawa, D. Vasaru, and W. Windsteiger. The Theorema Project: A Progress Report. In M. Kerber and M. Kohlhase, editors,
*Symbolic Computation and Automated Reasoning (Proceedings of CALCULEMUS 2000, Symposium on the Integration of Symbolic Computation and Mechanized Reasoning)*, pages 98–113. St. Andrews, Scotland, Copyright: A.K. Peters, Natick, Massachusetts, 6-7 August 2000.Google Scholar - [BHS07]Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt, editors.
*Verification of Object-Oriented Software: The KeY Approach*. Springer, 2007.Google Scholar - [BJK+97]B. Buchberger, T. Jebelean, F. Kriftner, M. Marin, E. Tomuta, and D. Vasaru. A Survey of the Theorema Project. In W. Kuechlin, editor,
*Proceedings of ISSAC’97 (International Symposium on Symbolic and Algebraic Computation, Maui, Hawaii, July 21-23, 1997)*, pages 384–391. ACM Press, 1997.Google Scholar - [BL81]B. Buchberger and F. Lichtenberger.
*Mathematics for Computer Science I - The Method of Mathematics (in German)*. Springer, 2nd edition, 1981.Google Scholar - [BS96]F. Baader and K. U. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures.
*Journal of Symbolic Computation*, 21(2):211–244, 1996.zbMATHCrossRefMathSciNetGoogle Scholar - [Buc65]B. Buchberger.
*An Algorithm for Finding the Basis Elements in the Residue Class Ring Modulo a Zero Dimensional Polynomial Ideal*. PhD thesis, University Innsbruck, Mathematical Institute, 1965. German, English translation in: J. of Symbolic Computation, Special Issue on Logic, Mathematics, and Computer Science: Interactions. Volume 41, Number 3–4, Pages 475–511, 2006.Google Scholar - [Buc96a]B. Buchberger. Mathematica as a Rewrite Language. In T. Ida, A. Ohori, and M. Takeichi, editors,
*Functional and Logic Programming (Proceedings of the 2nd Fuji International Workshop on Functional and Logic Programming,**November 1-4, 1996, Shonan Village Center)*, pages 1–13. Copyright: World Scientific, Singapore - New Jersey - London - Hong Kong, 1996.Google Scholar - [Buc96b]B. Buchberger. Symbolic Computation: Computer Algebra and Logic. In F. Bader and K.U. Schulz, editors,
*Frontiers of Combining Systems, Proceedings of FROCOS 1996 (1st International Workshop on Frontiers of Combining Systems), March 26-28, 1996, Munich*, volume Vol.3 of*Applied Logic Series*, pages 193–220. Kluwer Academic Publisher, Dordrecht - Boston - London, The Netherlands, 1996.Google Scholar - [Buc96c]B. Buchberger. Using Mathematica for Doing Simple Mathematical Proofs. In
*Proceedings of the 4th Mathematica Users’ Conference, Tokyo, November 2, 1996.*, pages 80–96. Copyright: Wolfram Media Publishing, 1996.Google Scholar - [Buc97]B. Buchberger. Mathematica: Doing Mathematics by Computer? In A. Miola and M. Temperini, editors,
*Advances in the Design of Symbolic Computation Systems*, pages 2–20. Springer Vienna, 1997. RISC Book Series on Symbolic Computation.Google Scholar - [Buc99]Bruno Buchberger. Theory Exploration Versus Theorem Proving. Technical Report 99-46, RISC Report Series, University of Linz, Austria, July 1999. Also available as SFB Report No. 99-38, Johannes Kepler University Linz, Spezialforschungsbereich F013, December 1999.Google Scholar
- [Buc01]B. Buchberger. The PCS Prover in Theorema. In R. Moreno-Diaz, B. Buchberger, and J.L. Freire, editors,
*Proceedings of EUROCAST 2001 (8th International Conference on Computer Aided Systems Theory – Formal Methods and Tools for Computer Science)*, Lecture Notes in Computer Science 2178, pages 469–478. Las Palmas de Gran Canaria, Copyright: Springer - Verlag Berlin, 19-23 February 2001.Google Scholar - [Buc03]B. Buchberger. Algorithm Invention and Verification by Lazy Thinking. In D. Petcu, V. Negru, D. Zaharie, and T. Jebelean, editors,
*Proceedings of SYNASC 2003, 5th International Workshop on Symbolic and Numeric Algorithms for Scientific Computing Timisoara*, pages 2–26, Timisoara, Romania, 1-4 October 2003. Copyright: Mirton Publisher.Google Scholar - [Buc04]B. Buchberger. Towards the Automated Synthesis of a Gröbner Bases Algorithm.
*RACSAM (Rev. Acad. Cienc., Spanish Royal Academy of Science)*, 98(1):65–75, 2004.zbMATHMathSciNetGoogle Scholar - [Buc06]B. Buchberger. Mathematical Theory Exploration, August 17-20 2006. Invited talk at IJCAR, Seattle, USA.Google Scholar
- [CFK07]J. Coelho, M. Florido, and T. Kutsia. Sequence disunification and its application in collaborative schema construction. In M. Weske, M.-S. Hacid, and C. Godart, editors,
*Web Information Systems – WISE 2007 Workshops*, volume 4832 of*LNCS*, pages 91–102. Springer, 2007.Google Scholar - [Col75]G. E. Collins. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In
*Second GI Conference on Authomata Theory and Formal Languages*, volume 33 of*LNCS*, pages 134–183. Springer, 1975.Google Scholar - [Com91]H. Comon. Completion of rewrite systems with membership constraints. Rapport de Recherche 699, L.R.I., Université de Paris-Sud, 1991.Google Scholar
- [Com98]H. Comon. Completion of rewrite systems with membership constraints. Part II: Constraint solving.
*Journal of Symbolic Computation*, 25(4):421–453, 1998.zbMATHCrossRefMathSciNetGoogle Scholar - [Cra08]A. Craciun.
*Lazy Thinking Algorithm Synthesis in Gröbner Bases Theory*. PhD thesis, RISC, Johannes Kepler University Linz, Austria, April 2008.Google Scholar - [EJ08]M. Erascu and T. Jebelean. Practical Program Verification by Forward Symbolic Execution: Correctness and Examples. In B. Buchberger, T. Ida, and T. Kutsia, editors,
*Austrian-Japan Workshop on Symbolic Computation in Software Science*, pages 47–56, 2008.Google Scholar - [Fei05]Ingo Feinerer. Formal Program Verification: A Comparison of Selected Tools and Their Theoretical Foundations. Master’s thesis, Theory and Logic Group, Institute of Computer Languages, Vienna University of Technology, Vienna, Austria, January 2005.Google Scholar
- [Hoa69]C. A. R. Hoare. An Axiomatic Basis for Computer Programming.
*Comm. ACM*, 12, 1969.Google Scholar - [Hoa03]C. A. R. Hoare. The verifying compiler: A grand challenge for computing research.
*Journal of ACM*, 50:63–69, 2003.CrossRefGoogle Scholar - [Jeb01]T. Jebelean. Natural proofs in elementary analysis by S-Decomposition. Technical Report 01-33, RISC, Johannes Kepler University, Linz, Austria, 2001.Google Scholar
- [KJ00]B. Konev and T. Jebelean. Using meta-variables for natural deduction in theorema. In M. Kerber and M. Kohlhase, editors,
*Proceedings of the CALCULEMUS 2000 8th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning*, pages 160–175, St. Andrews, Scotland, August 6-7 2000.Google Scholar - [KLV07]T. Kutsia, J. Levy, and M. Villaret. Sequence unification through currying. In Franz Baader, editor,
*Proc. of the 18th Int. Conference on Rewriting Techniques and Applications, RTA’07*, volume 4533 of*Lecture Notes in Computer Science*, pages 288–302. Springer, 2007.Google Scholar - [KM05]T. Kutsia and M. Marin. Matching with regular constraints. In G. Sutcliffe and A. Voronkov, editors,
*Logic for Programming, Artificial Intelligence, and Reasoning. Proceedings of the 12th International Conference, LPAR’05*, volume 3835 of*LNAI*, pages 215–229. Springer, 2005.Google Scholar - [Kov07]L. Kovacs.
*Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema*. PhD thesis, RISC, Johannes Kepler University Linz, Austria, October 2007. RISC Technical Report No. 07-16.Google Scholar - [KPJ05]L. Kovacs, N. Popov, and T. Jebelean. Verification Environment in Theorema.
*Annals of Mathematics, Computing and Teleinformatics (AMCT)*, 1(2):27–34, 2005.Google Scholar - [KPJ06]L. Kovacs, N. Popov, and T. Jebelean. Combining Logic and Algebraic Techniques for Program Verification in Theorema. In T. Margaria and B. Steffen, editors,
*Proceedings ISOLA 2006*, Paphos, Cyprus, November 2006. To appear.Google Scholar - [Kut03]T. Kutsia. Equational prover of Theorema. In R. Nieuwenhuis, editor,
*Proc. of the 14th Int. Conference on Rewriting Techniques and Applications, RTA’03*, volume 2706 of*LNCS*, pages 367–379. Springer, 2003.Google Scholar - [Kut06]T. Kutsia. Context sequence matching for XML.
*Electronic Notes on Theoretical Computer Science*, 157(2):47–65, 2006.CrossRefGoogle Scholar - [Kut07]T. Kutsia. Solving equations with sequence variables and sequence functions.
*Journal of Symbolic Computation*, 42(3):352–388, 2007.zbMATHCrossRefMathSciNetGoogle Scholar - [Kut08]T. Kutsia. Flat matching.
*Journal of Symbolic Computation*, 43(12):858–873, 2008.zbMATHCrossRefMathSciNetGoogle Scholar - [Lev96]J. Levy. Linear second-order unification. In Harald Ganzinger, editor,
*Proc. of the 7th Int. Conference Conference on Rewriting Techniques and Applications, RTA’96*, volume 1103 of*LNCS*, pages 332–346. Springer, 1996.Google Scholar - [LNV05]J. Levy, J. Niehren, and M. Villaret. Well-nested context unification. In R. Nieuwenhuis, editor,
*Proc. of the 20th Int. Conference on Automated Deduction, CADE-20*, volume 3632 of*LNAI*, pages 149–163. Springer, 2005.Google Scholar - [LS87]J. Loeckx and K. Sieber.
*The Foundations of Program Verification*. Teubner, second edition, 1987.Google Scholar - [LV02]J. Levy and M. Villaret. Currying second-order unification problems. In S. Tison, editor,
*Proc. of the 13th Int. Conference on Rewriting Techniques and Applications, RTA’02*, volume 2378 of*LNCS*, pages 326–339, Copenhagen, Denmark, 2002. Springer.Google Scholar - [Mak77]G. S. Makanin. The problem of solvability of equations in a free semigroup.
*Math. USSR Sbornik*, 32(2):129–198, 1977.zbMATHCrossRefGoogle Scholar - [McC97]W. McCune. Solution of the robbins problem.
*Journal of Automatic Reasoning*, 19:263–276, 1997.zbMATHCrossRefMathSciNetGoogle Scholar - [MK06]M. Marin and T. Kutsia. Foundations of the rule-based system RhoLog.
*Journal of Applied Non-Classical Logics*, 16(1–2):151–168, 2006.CrossRefMathSciNetzbMATHGoogle Scholar - [ORS92]S. Owre, J. M. Rushby, and N. Shankar. PVS: A Prototype Verification System. In Deepak Kapur, editor,
*11th International Conference on Automated Deduction (CADE)*, volume 607 of*Lecture Notes in Artificial Intelligence*, pages 748–752, Saratoga, NY, June 14–18, 1992. Springer.Google Scholar - [PB02]F. Piroi and B. Buchberger. Focus Windows: A New Technique for Proof Presentation. In H. Kredel and W. Seiler, editors,
*Proceedings of the 8th Rhine Workshop on Computer Algebra, Mannheim, Germany*, pages 297–313, 2002.Google Scholar - [PK05]Florina Piroi and Temur Kutsia. The Theorema Environment for Interactive Proof Development, December 3 2005. Contributed talk at 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’05.Google Scholar
- [RIS06]The RISC ProofNavigator, 2006. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria, http://www.risc.unilinz.ac.at/research/formal/software/ProofNavigator.Google Scholar
- [Rob02]Judit Robu. Geometry Theorem Proving in the Frame of the Theorema Project. Technical Report 02-23, RISC Report Series, University of Linz, Austria, September 2002. PhD Thesis.Google Scholar
- [Sch06]W. Schreiner. The RISC ProofNavigator — Tutorial and Manual. Technical report, Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria, July 2006.Google Scholar
- [Sch08a]W. Schreiner. A Program Calculus. Technical report, Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria, September 2008.Google Scholar
- [Sch08b]W. Schreiner. The RISC ProofNavigator: A Proving Assistant for Program Verification in the Classroom.
*Formal Aspects of Computing*, April 2008. DOI 10.1007/s00165-008-0069-4.Google Scholar - [SMT06]SMT-LIB — The Satisfiability Modulo Theories Library, 2006. University of Iowa, Iowa City, IA, http://combination.cs.uiowa.edu/smtlib.Google Scholar
- [SS94]M. Schmidt-Schauß. Unification of stratified second-order terms. Internal Report 12/24, Johann-Wolfgang-Goethe-Universität, Frankfurt, Germany, 1994.Google Scholar
- [SSS02]M. Schmidt-Schauß and Klaus U. Schulz. Solvability of context equations with two context variables is decidable.
*Journal of Symbolic Computation*, 33(1):77–122, 2002.zbMATHCrossRefMathSciNetGoogle Scholar - [Vil04]M. Villaret.
*On Some Variants of Second-Order Unification*. PhD thesis, Universitat Politècnica de Catalunya, Barcelona, 2004.Google Scholar - [VJB08]R. Vajda, T. Jebelean, and B. Buchberger. Combining Logical and Algebraic Techniques for Natural Style Proving in Elementary Analysis.
*Mathematics and Computers in Simulation*, 2008.Google Scholar - [WBR06]W. Windsteiger, B. Buchberger, and M. Rosenkranz. Theorema. In Freek Wiedijk, editor,
*The Seventeen Provers of the World*, volume 3600 of*LNAI*, pages 96–107. Springer Berlin Heidelberg New York, 2006.CrossRefGoogle Scholar - [Win01]W. Windsteiger.
*A Set Theory Prover in Theorema: Implementation and Practical Applications*. PhD thesis, RISC Institute, May 2001.Google Scholar - [Win06]W. Windsteiger. An Automated Prover for Zermelo-Fraenkel Set Theory in Theorema.
*JSC*, 41(3-4):435–470, 2006.zbMATHMathSciNetGoogle Scholar - [Wol03]S. Wolfram.
*The Mathematica Book*. Wolfram Media, 5th edition, 2003.Google Scholar