Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
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.
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.
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.
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.
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.
Chang, C.-L. and Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York-London, 1973.
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.
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.
Coelho, P. and Pereira, L.M.: Automated reasoning in geometry theorem proving with Prolog. Journal of Automated Reasoning, 2, 329–390, 1996.
McCune, W.W.: OTTER 2.0. In: Proceedings of LADE-10, Springer-Verlag, LNAI 449, 663–664, 1990.
Fèvre, S.: A hybrid method for proving theorems in elementary geometry. In: Proceedings of ASCM'95, Scientists Incorporated, 113–123, 1995.
Kapur, D., Mundy, J.L. eds.: Geometric Reasoning. MIT Press, Cambridge, 1989.
Liu, Z. and Wu, J.: The remainder method for the first-order theorem proving. In: Proceedings of ASCM'95, Scientists Incorporated, 91–97, 1995.
Quaife, A.: Automated development of Tarski's geometry. Journal of Automated Reasoning, 5, 97–118, 1989.
Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM, 12 23–41, 1965.
Stickel, M.E.: Automated deduction by theory resolution. Journal of Automated Reasoning, 1 333–355, 1985.
Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edition. University of California Press, Berkeley and Los Angeles, 1951.
Trainen, R.: A new method for undecidability proofs of first-order theories. Journal of Symbolic Computation, 14(5), 437–458, 1990.
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.
Wang, D.: An elimination method for polynomial systems. Journal of Symbolic Computation, 16, 83–114, 1993.
Wu, W.: Basic principles of mechanical theorem proving in elementary geometries. Journal of Automated Reasoning, 2, 221–252, 1986.
Wu, W.: Mechanical Theorem Proving in Geometries: Basic Principles. SpringerVerlag, Wien-New York, 1994.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fèvre, S. (1998). Integration of reasoning and algebraic calculus in geometry. In: Wang, D. (eds) Automated Deduction in Geometry. ADG 1996. Lecture Notes in Computer Science, vol 1360. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022718
Download citation
DOI: https://doi.org/10.1007/BFb0022718
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64297-8
Online ISBN: 978-3-540-69717-6
eBook Packages: Springer Book Archive