Automatizing geometric proofs and constructions

  • Beat Brüderlin
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 333)


The theory of Euclidean Geometry is the foundation of almost all Computer-Geometry applications. Also it is one of the first mathematical theories that has been axiomatized systematically by D. Hilbert, in the beginning of this century [HIL 71]. Nevertheless, for most algorithms of "Computational Geometry" the algebraic interpretation of Geometry is of greater importance (see, e.g. [SHA


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BUL 82]
    B. Buchberger and R. Loos. Algebraic Simplification. Computing, Suppl. 4, 11, (1982) pp. 11–43Google Scholar
  2. [BRU 86]
    B. Brüderlin. Constructing Three-Dimensional Geometric Objects Defined By Constraints. 1986 Workshop on Interactive 3D Graphics, Conference Proceedings, Chapel Hill, North Carolina, published by ACM Siggraph, 1986Google Scholar
  3. [BRU 87]
    B. Brüderlin. Rule-Based Geometric Modelling. Ph.D. thesis, ETH Zürich, Switzerland, Verlag der Fachvereine, vdf-Verlag, Zürich 1987 (ISBN 3 7281 1638)Google Scholar
  4. [CHO 84]
    Shang-Ching Chou. Proving Elementary Geometry Theorems Using Wu's Algorithm. Contemporary Mathematics, Volume 29, 1984, American Mathematical Society, pp 234–287Google Scholar
  5. [CHS 86]
    Shang-Ching Chou and William F. Schelter. Proving Geometry Theorems with Rewrite Rules. Journal of Automated Reasoning 2 (1986) pp. 253–373Google Scholar
  6. [CHO 86]
    Shang-Ching Chou. A Collection of Geometry Theorems Proved Mechanically. Technical Report 50, July 1986. Institute for Computing Science, University of Texas at AustinGoogle Scholar
  7. [CLM 81]
    W.F. Clocksin, C.S. Mellish. Programming in Prolog. Springer Verlag, Berlin, Heidelberg, New York 1981Google Scholar
  8. [COP 86]
    Helder Coelho, Luiz Moniz Pereira. Automated Reasoning in Geometry Theorem Proving with Prolog. Journal of Automated Reasoning 2 (1986)Google Scholar
  9. [COL 75]
    G.E. Collins. Quantifier Elimination for Real Closed Fields by Cylindrical Algebraic Decomposition. Lecture Notes in Computer Science No. 33, pp. 134–183, Springer Verlag, 1975Google Scholar
  10. [ENG 83]
    E. Engeler. Metamathematik der Elementarmathematik. Springer Verlag, Berlin, Heidelberg, New York 1983Google Scholar
  11. [GEL 59]
    H. Gelernter. Realization of a Theorem Proving Machine, 1959. Published in "Automation of Reasoning" Vol.1, Springer Verlag, 1983Google Scholar
  12. [GOS 83]
    James Gosling. Algebraic Constraints. Ph.D. thesis, Carnegie-Mellon University, May 1983Google Scholar
  13. [HIL 71]
    D. Hilbert. Foundations of Geometry. Open Court Publishing Company, La Salla, Illinois 1971Google Scholar
  14. [HUC 86]
    Ulrich Huckenbeck. Geometrische Maschinenmodelle (german). PhD. thesis, Universität Würzburg, Germany, 1986Google Scholar
  15. [HSI 83]
    Jieh Hsiang. Topics in Automated Theorem Proving and Program Generation. Ph.D. Thesis, Univ. of Illinois at Urbana-Champaign, 1983Google Scholar
  16. [HOA 69]
    C.A.R. Hoare. An Axiomatic Basis for Computer Programming. Communications of the ACM. Vol. 12 No. 10, 1969Google Scholar
  17. [KNB 70]
    D.E. Knuth, P.B. Bendix. Simple Word Problems in Universal Algebra. Computational Problems in Abstract Algebra. Conference Proceedings, Oxford 1967, J. Leech ed., Pergamon 1970Google Scholar
  18. [KOH 85]
    H.-P. Ko and M.A. Hussain. ALGE-PROVER. An Algebraic Geometry Theorem Proving Software. Report No. 85CRD139, july 1985. Technical Information Series, General ElectricGoogle Scholar
  19. [LIG 82]
    R. Light, D. Gossard. Modification of geometric models through variational geometry. CAD vo. 14, No. 4, Butterworth 1982Google Scholar
  20. [MUL 85]
    C. Muller. Modula — Prolog, User Manual. Rep. No. 63, July 1985. Inst. für Informatik, ETH Zürich, SwitzerlandGoogle Scholar
  21. [NEL 85]
    G. Nelson. Juno, a constraint-based graphics system. 1985 ACM Siggraph Conference ProceedingsGoogle Scholar
  22. [POP 86]
    R.J. Popplestone. The Edinburgh Designer System as a Framework for RoboticsGoogle Scholar
  23. [SCH 88]
    F. Schmid. A Symbolic Approach to Solving Formulas in Projective Geometry. Ph.D. Thesis, ETH, Switzerland To appear, 1988Google Scholar
  24. [SCH 75]
    Peter Schreiber. Theorie der geometrischen Konstruktionen (german). VEB Verlag der Wissenschaften, Berlin, 1975Google Scholar
  25. [SST 83]
    W. Schwabhäuser, W. Szmielev, A. Tarski. Metamathematische Methoden in der Geometrie (german). Springer Verlag Berlin, Heidelberg, New York 1983Google Scholar
  26. [SHA 78]
    Michael Ian Shamos. Computational Geometry. Ph.D. thesis, Yale University, New Haven, Connecticut, 1978Google Scholar
  27. [SUT 63]
    I. Sutherland. Sketchpad, A Man-Machine Graphical Communication System. Ph.D. thesis, MIT, January 1963Google Scholar
  28. [TAR 51]
    A. Tarski. A Decision Method for Elementary Algebra and Geometry. Univ. of Calif. Press, Berkeley, 1951Google Scholar
  29. [WIR 83]
    N. Wirth. Programming in Modula-2. Texts and Monographs in Computer Science. Springer Verlag Berlin, Heidelberg, New York 1983Google Scholar
  30. [WUW 84a]
    Wu Wen-tsün. Some Recent Advances in Mechanical Theorem Proving of Geometries. Contemporary Mathematics, Volume 29, 1984, American Mathematical Society, pp. 235–241Google Scholar
  31. [WUW 84b]
    Wu Wen-tsün. On the decision Problem and the mechanization of Theorem-Proving in Elementary Geometry. Contemporary Mathematics, Volume 29, 1984, American Mathematical Society, pp. 213–23Google Scholar
  32. [WUW 86]
    Wu Wen-tsün. Basic Principles of Mechanical Theorem Proving in Elementary Geometries. Journal of Automated Reasoning 2 (1986) pp. 221–252Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1988

Authors and Affiliations

  • Beat Brüderlin
    • 1
  1. 1.Institute for Computer ScienceSwiss Federal Institute of Technology, ETHZürichSwitzerland

Personalised recommendations