Integration of reasoning and algebraic calculus in geometry

  • Stéphane Fèvre
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1360)


This paper presents a new framework for merging reasoning and algebraic calculus in elementary geometry. This approach is based on the use of algebraic constraints in clause-based calculi. These constraints are considered as contexts for reasoning. It allows to introduce new inference rules and to use the powerful algebraic methods which have been successful in geometry theorem proving. The semantics of classical first-order logic has been modified to correspond with this framework and classical results in proof theory such as Herbrand's theorem, lifting lemma and completeness are proved to remain true within it. Some examples give an idea of the possibilities provided by this framework. A few strategies are also discussed and a comparison with related techniques is done.


Inference Rule Theorem Prove Automate Reasoning Algebraic Computation Empty Clause 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bourely, C., Caferra, R. and Peltier, N.: A method for building models automatically: Experiments with an extension of OTTER. In: Proceedings of CADE-12, Springer Verlag, LNAI 814, 72–86, 1994.Google Scholar
  2. 2.
    Buchberger, B.: Gröbner bases: An algorithmic method in polynomial ideal theory. In: Multidimensional Systems Theory, Bose, N.K. ed., D. Reidel Publ. Comp., 184–232, 1985.Google Scholar
  3. 3.
    Caferra, R. and Herment, M.: A generic graphic framework for combining inference tools and editing proofs and formulae. Journal of Symbolic' Computation, 19, 217–243, 1995.CrossRefGoogle Scholar
  4. 4.
    Collins, G.E.: Quantifier elimination for the elementary geometry. In: Proceedings of 2nd G.I. Conference on Automata Theory and Formal Languages, Brakhage, H. ed., LNCS 33, 134–183, 1975.Google Scholar
  5. 5.
    Caferra, R. and Zabel, N.: A method for simultaneous search for refutations and models by equational constraint solving. Journal of Symbolic Computation, 13, 613–641, 1992.Google Scholar
  6. 6.
    Chang, C.-L. and Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York-London, 1973.Google Scholar
  7. 7.
    Chou, S-C., Gao, X-S. and Zhang, J-Z.: Automated generation of readable proofs with geometric invariants: I. Multiple and shortest proof generation. Journal of Automated Reasoning. 17, 325–347, 1996.Google Scholar
  8. 8.
    Chou, S-C., Gao, X-S. and Zhang, J-Z.: Automated generation of readable proofs with geometric invariants: II. Theorem proving with full-angles. Journal of Automated Reasoning, 17, 350–370, 1996.Google Scholar
  9. 9.
    Coelho, P. and Pereira, L.M.: Automated reasoning in geometry theorem proving with Prolog. Journal of Automated Reasoning, 2, 329–390, 1996.CrossRefMathSciNetGoogle Scholar
  10. 10.
    McCune, W.W.: OTTER 2.0. In: Proceedings of LADE-10, Springer-Verlag, LNAI 449, 663–664, 1990.Google Scholar
  11. 11.
    Fèvre, S.: A hybrid method for proving theorems in elementary geometry. In: Proceedings of ASCM'95, Scientists Incorporated, 113–123, 1995.Google Scholar
  12. 12.
    Kapur, D., Mundy, J.L. eds.: Geometric Reasoning. MIT Press, Cambridge, 1989.Google Scholar
  13. 13.
    Liu, Z. and Wu, J.: The remainder method for the first-order theorem proving. In: Proceedings of ASCM'95, Scientists Incorporated, 91–97, 1995.Google Scholar
  14. 14.
    Quaife, A.: Automated development of Tarski's geometry. Journal of Automated Reasoning, 5, 97–118, 1989.CrossRefGoogle Scholar
  15. 15.
    Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM, 12 23–41, 1965.CrossRefGoogle Scholar
  16. 16.
    Stickel, M.E.: Automated deduction by theory resolution. Journal of Automated Reasoning, 1 333–355, 1985.CrossRefGoogle Scholar
  17. 17.
    Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edition. University of California Press, Berkeley and Los Angeles, 1951.Google Scholar
  18. 18.
    Trainen, R.: A new method for undecidability proofs of first-order theories. Journal of Symbolic Computation, 14(5), 437–458, 1990.CrossRefGoogle Scholar
  19. 19.
    Wang, D.: Reasoning about geometric problems using an elimination method. In: Automated Practical Reasoning: Algebraic Approaches, Pfalzgraf, J., Wang, D. eds., Springer-Verlag, 147–185, 1996.Google Scholar
  20. 20.
    Wang, D.: An elimination method for polynomial systems. Journal of Symbolic Computation, 16, 83–114, 1993.CrossRefGoogle Scholar
  21. 21.
    Wu, W.: Basic principles of mechanical theorem proving in elementary geometries. Journal of Automated Reasoning, 2, 221–252, 1986.Google Scholar
  22. 22.
    Wu, W.: Mechanical Theorem Proving in Geometries: Basic Principles. SpringerVerlag, Wien-New York, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Stéphane Fèvre
    • 1
  1. 1.LEIBNIZ-IMAGGrenoble CedexFrance

Personalised recommendations