More Web Proxy on the site http://driver.im/

Article

Free access

Examples of automatic theorem proving a real geometry

Authors:

Ahmed Guergueb,

Jean Mainguené,

Marie-Françoise RoyAuthors Info & Claims

ISSAC '94: Proceedings of the international symposium on Symbolic and algebraic computation

Pages 20 - 24

https://doi.org/10.1145/190347.190354

Published: 01 August 1994 Publication History

Abstract

In this paper we show that computer algebra methods in mechanical geometry theorem proving can also be applied to obtain new theorems involving inequalities. An interesting feature is that in real geometry, several cases can occur, none of them being more generic than the other. The examples we give come from the geometry of the triangle, more precisely comparing radii of circles defined in the triangle.

References

[1]

Arnon D. S., McCallum S. A polynomial-time algorithm for the topological type of a real algebraic curve. Journal of Symbolic Computation, 5, 1988.

Digital Library

[2]

: Buchberger B., Collins G.E., Kutzler B.-Algebraic methods for geometric reasoning - Annual review of computer science- 1988.

Digital Library

[3]

: Bochnak J., Coste M., Roy M.F.- G6om~trie alg6briqu r~elle- Ergebnisse der Mathem~tik- Springer Verlag- Berlin - 1987.

[4]

: Shang-ching Chou, Mechanical Geometry Theorem Proving- D. Reidel publishing company- Dordrecht- 1988.

Digital Library

[5]

Collins G. E. Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In Lecture Notes In Computer Science, pages 134- -183. Springer-Verlag, Berlin, 1975. Vol. 33.

Digital Library

[6]

: Coxeter H.S.M.- Introduction to geometry- John Wiley and sons- 1961.

[7]

: Gao Xiaoshan - Transcendental functions and mechanical theorem proving in elementary geometries- Mathematics Mechanization Research Preprints, Institute of Systems Science, N2- Academia Sinica- 1!}87.

[8]

Guergueb A. Exemples de d~monsl;ration automatique en g~omdtrie r~dle, Th~se, Universit~ de Kennes I.

[9]

: Gr6bner W.- Moderne algebraische Geometrie- Springer Verlag- Wien und innsbr6ck- 1949.

[10]

~toon ~tong: Efficient Method for Analyzing Topology of Plane Red Algebraic Curves. In IMACS-SC, 93, Lille, 1993.

Digital Library

[11]

Mainguen~ J. Feuerback vs Taylor, preprint, Universit~ de Rennes

[12]

Pinchon D. Oral communication

[13]

: Ritz J. F. Differential equations from the algebraic standpoint- American :'vlathema~ical Society - New York- 1932.

[14]

: Wu Wen-Tsun, On the decisic)n problem and the mechanization of theorem proving in eie:men~ary geometry- Scientia Sinica, 21(1978), re-published in Automated Theorem Proving after 25 years- Bledsoe and Loveland editors- Denver - 1984.

[15]

: Wu Wen-Tsun, A mechanization method of geometry and its application Mechanical proving of polynomial inequalities and equations solving- ~athematics Mechanization I~,esearch Preprints, Institute of Systems Science, N2 - Academia Sinica- 1987.

[16]

: Wang Dongming, Gao Xiaoshaal- Geometry theorems proved mechanically using Wus method Mathematics Mechamza~ion Research Preprints, Institute of Systems Science, N2- Academia Sinica- 1987.

Cited By

Brown CKovács ZRecio TVajda RVélez M(2022)Is Computer Algebra Ready for Conjecturing and Proving Geometric Inequalities in the Classroom?Mathematics in Computer Science10.1007/s11786-022-00532-916:4Online publication date: 6-Dec-2022
https://doi.org/10.1007/s11786-022-00532-9
Braun DMagaud NSchreck PChyzak FLabahn G(2021)Two New Ways to Formally Prove Dandelin-Gallucci's TheoremProceedings of the 2021 International Symposium on Symbolic and Algebraic Computation10.1145/3452143.3465550(59-66)Online publication date: 18-Jul-2021
https://dl.acm.org/doi/10.1145/3452143.3465550
Wang D(2005)Geometry machines: From AI to SMCArtificial Intelligence and Symbolic Mathematical Computation10.1007/3-540-61732-9_60(213-239)Online publication date: 2-Jun-2005
https://doi.org/10.1007/3-540-61732-9_60
Show More Cited By

Index Terms

Examples of automatic theorem proving a real geometry
1. Computing methodologies
  1. Symbolic and algebraic manipulation
    1. Symbolic and algebraic algorithms
      1. Algebraic algorithms
      2. Theorem proving algorithms
2. Theory of computation
  1. Models of computation
    1. Computability
  2. Randomness, geometry and discrete structures
    1. Computational geometry

Recommendations

On automatic theorem proving in conjugate geometries
A New Approach for Automatic Theorem Proving in Real Geometry

We present a new method for proving geometric theorems in the real plane or higher dimension. The method is derived from elimination set ideas for quantifier elimination in linear and quadratic formulas over the reals. In contrast to other approaches, our ...
Geometry images
SIGGRAPH '02: Proceedings of the 29th annual conference on Computer graphics and interactive techniques

Surface geometry is often modeled with irregular triangle meshes. The process of remeshing refers to approximating such geometry using a mesh with (semi)-regular connectivity, which has advantages for many graphics applications. However, current ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISSAC '94: Proceedings of the international symposium on Symbolic and algebraic computation

August 1994

359 pages

ISBN:0897916387

DOI:10.1145/190347

Chairman:
Malcolm MacCallum
QMW, London, UK

Copyright © 1994 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSAM: ACM Special Interest Group on Symbolic and Algebraic Manipulation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 August 1994

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

ISSAC94

Sponsor:

SIGSAM

ISSAC94: International Symposium on Symbolic and Algebraic Computation

July 20 - 22, 1994

Oxford, United Kingdom

Acceptance Rates

Overall Acceptance Rate 395 of 838 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
314
Total Downloads

Downloads (Last 12 months)44
Downloads (Last 6 weeks)9

Reflects downloads up to 03 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Brown CKovács ZRecio TVajda RVélez M(2022)Is Computer Algebra Ready for Conjecturing and Proving Geometric Inequalities in the Classroom?Mathematics in Computer Science10.1007/s11786-022-00532-916:4Online publication date: 6-Dec-2022
https://doi.org/10.1007/s11786-022-00532-9
Braun DMagaud NSchreck PChyzak FLabahn G(2021)Two New Ways to Formally Prove Dandelin-Gallucci's TheoremProceedings of the 2021 International Symposium on Symbolic and Algebraic Computation10.1145/3452143.3465550(59-66)Online publication date: 18-Jul-2021
https://dl.acm.org/doi/10.1145/3452143.3465550
Wang D(2005)Geometry machines: From AI to SMCArtificial Intelligence and Symbolic Mathematical Computation10.1007/3-540-61732-9_60(213-239)Online publication date: 2-Jun-2005
https://doi.org/10.1007/3-540-61732-9_60
Conti PTraverso C(2005)A case of automatic theorem proving in Euclidean geometry: the Maclane 83 theoremApplied Algebra, Algebraic Algorithms and Error-Correcting Codes10.1007/3-540-60114-7_14(183-193)Online publication date: 2-Jun-2005
https://doi.org/10.1007/3-540-60114-7_14

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents