Advertisement

Automated Reasoning

  • Tudor Jebelean
  • Bruno Buchberger
  • Temur Kutsia
  • Nikolaj Popov
  • Wolfgang Schreiner
  • Wolfgang Windsteiger
Chapter
  • 473 Downloads

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 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. [AH77]
    K. Appel and W. Haken. Solution of the four color map problem. Scientific American, 237:108–121, October 1977.MathSciNetCrossRefGoogle Scholar
  2. [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
  3. [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
  4. [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
  5. [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
  6. [BHS07]
    Bernhard Beckert, Reiner Hähnle, and Peter H. Schmitt, editors. Verification of Object-Oriented Software: The KeY Approach. Springer, 2007.Google Scholar
  7. [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
  8. [BL81]
    B. Buchberger and F. Lichtenberger. Mathematics for Computer Science I - The Method of Mathematics (in German). Springer, 2nd edition, 1981.Google Scholar
  9. [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
  10. [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
  11. [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
  12. [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
  13. [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
  14. [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
  15. [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
  16. [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
  17. [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
  18. [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
  19. [Buc06]
    B. Buchberger. Mathematical Theory Exploration, August 17-20 2006. Invited talk at IJCAR, Seattle, USA.Google Scholar
  20. [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
  21. [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
  22. [Com91]
    H. Comon. Completion of rewrite systems with membership constraints. Rapport de Recherche 699, L.R.I., Université de Paris-Sud, 1991.Google Scholar
  23. [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
  24. [Cra08]
    A. Craciun. Lazy Thinking Algorithm Synthesis in Gröbner Bases Theory. PhD thesis, RISC, Johannes Kepler University Linz, Austria, April 2008.Google Scholar
  25. [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
  26. [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
  27. [Hoa69]
    C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Comm. ACM, 12, 1969.Google Scholar
  28. [Hoa03]
    C. A. R. Hoare. The verifying compiler: A grand challenge for computing research. Journal of ACM, 50:63–69, 2003.CrossRefGoogle Scholar
  29. [Jeb01]
    T. Jebelean. Natural proofs in elementary analysis by S-Decomposition. Technical Report 01-33, RISC, Johannes Kepler University, Linz, Austria, 2001.Google Scholar
  30. [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
  31. [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
  32. [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
  33. [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
  34. [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
  35. [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
  36. [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
  37. [Kut06]
    T. Kutsia. Context sequence matching for XML. Electronic Notes on Theoretical Computer Science, 157(2):47–65, 2006.CrossRefGoogle Scholar
  38. [Kut07]
    T. Kutsia. Solving equations with sequence variables and sequence functions. Journal of Symbolic Computation, 42(3):352–388, 2007.zbMATHCrossRefMathSciNetGoogle Scholar
  39. [Kut08]
    T. Kutsia. Flat matching. Journal of Symbolic Computation, 43(12):858–873, 2008.zbMATHCrossRefMathSciNetGoogle Scholar
  40. [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
  41. [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
  42. [LS87]
    J. Loeckx and K. Sieber. The Foundations of Program Verification. Teubner, second edition, 1987.Google Scholar
  43. [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
  44. [Mak77]
    G. S. Makanin. The problem of solvability of equations in a free semigroup. Math. USSR Sbornik, 32(2):129–198, 1977.zbMATHCrossRefGoogle Scholar
  45. [McC97]
    W. McCune. Solution of the robbins problem. Journal of Automatic Reasoning, 19:263–276, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  46. [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
  47. [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
  48. [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
  49. [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
  50. [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
  51. [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
  52. [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
  53. [Sch08a]
    W. Schreiner. A Program Calculus. Technical report, Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria, September 2008.Google Scholar
  54. [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
  55. [SMT06]
    SMT-LIB — The Satisfiability Modulo Theories Library, 2006. University of Iowa, Iowa City, IA, http://combination.cs.uiowa.edu/smtlib.Google Scholar
  56. [SS94]
    M. Schmidt-Schauß. Unification of stratified second-order terms. Internal Report 12/24, Johann-Wolfgang-Goethe-Universität, Frankfurt, Germany, 1994.Google Scholar
  57. [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
  58. [Vil04]
    M. Villaret. On Some Variants of Second-Order Unification. PhD thesis, Universitat Politècnica de Catalunya, Barcelona, 2004.Google Scholar
  59. [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
  60. [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
  61. [Win01]
    W. Windsteiger. A Set Theory Prover in Theorema: Implementation and Practical Applications. PhD thesis, RISC Institute, May 2001.Google Scholar
  62. [Win06]
    W. Windsteiger. An Automated Prover for Zermelo-Fraenkel Set Theory in Theorema. JSC, 41(3-4):435–470, 2006.zbMATHMathSciNetGoogle Scholar
  63. [Wol03]
    S. Wolfram. The Mathematica Book. Wolfram Media, 5th edition, 2003.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Tudor Jebelean
    • 1
  • Bruno Buchberger
    • 1
  • Temur Kutsia
    • 1
  • Nikolaj Popov
    • 1
  • Wolfgang Schreiner
    • 1
  • Wolfgang Windsteiger
    • 1
  1. 1.Research Institute for Symbolic Computation (RISC)Johannes Kepler University Linz (JKU)LinzAustria

Personalised recommendations