The DOI matches its Crossref record.
An Introduction to Java Geometry Expert
Overview
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
In the citing paper
“Because these methods often have large time and memory complexity, especially when processing IMO-sized problems, we report their result by assigning success to any problem that can be decided within 48 h using one of their existing implementations17.”
From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [17]
In the citing paper
“In geometry, the symbolic deduction engine is deductive database (refs. 10,17), with the ability to efficiently deduce new statements from the premises by means of geometric rules.”
From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [17]
In the citing paper
“On the set of geometry problems collected in JGEX17, which consists mainly of problems with moderate difficulty and well-known theorems, we find nearly 20 problems in the synthetic data.”
From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [17]
In the citing paper
“| Search (human-like) | DD + human-designed heuristics17 | 9 |”
From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [17]
In the citing paper
“DD (ref. 17) handles algebraic deductions by expressing them under a few limited deduction rules, therefore, it is unable to express more complex manipulations, leaving arithmetic inferences not covered.”
From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [17]
In the citing paper
“We use the method of structured DD10,17 for this purpose as it can find the deduction closure in just seconds on standard non-accelerator hardware.”
From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [17]
In the citing paper
“With the introduction of DD10,17, area methods61 and full-angle methods30, geometry solvers use higher-level deduction rules than Tarski’s or Hilbert’s axioms and are able to prove a larger number of more complex theorems than those operating in formal languages.”
From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [17]
Citations
Cites
No references could be resolved yet.
Research works printed but not linked: 12
- Chou, S., Gao, X., Zhang, J.: Automated generation of readable proofs with geometric invariants, II. Theorem proving with full-angles. Journal Automated Reasoning 17, 325–347 (1996) · DOI
- Chou, S.C.: Mechanical geometry theorem proving. Springer, Heidelberg (1988)
- Chou, S.C., Gao, X., Ye, Z.: Java Geometry Expert. In: Proceedings of the 10th Asian Technology Conference in Mathematics, pp. 78–84 (2005)
- Chou, S.C., Gao, X.S., Zhang, J.Z.: A deductive database approach to automated geometry theorem proving and discovering. Journal of Automated Reasoning 25(3), 219–246 (2000) · DOI · Paper page
- Dolzmann, A., Sturm, T., Weispfenning, V.: A new approach for automatic theorem proving in real geometry. Journal of Automated Reasoning 21(3), 357–380 (1998) · DOI
- Hongbo, L., Minde, C.: Proving theorems in elementary geometry with Glifford algebraic method. Chinese Math. Progress 26(4), 357–371 (1997)
- Li, H.: Some applications of Clifford algebra to geometries. Automated Deduction in Geometry, 156–179 (1999) · DOI
- Nelsen, R.: Proofs without words: Exercises in visual thinking. Mathematical Assn of Amer (1993) · DOI
- Nelsen, R., Alsina, C.: Math Made Visual: Creating Images for Understanding Mathematics. Mathematical Assn of Amer (2006) · DOI
- Wang, D.: Reasoning about geometric problems using an elimination method. Automatic Practical Reasoning, 147–185 (1989) · DOI
- Wen-Tsun, W.: On the decision problem and the mechanization of theorem proving in elementary geometry. Scientia Sinica 21(2), 159–172 (1978)
- Ye, Z., Chou, S.C., Gao, X.S.: Visually Dynamic Presentation of Proofs in Plane Geometry Part 2. Automated Generation of Visually Dynamic Presentations with the Full-Angle Method and the Deductive Database Method. Journal of Automated Reasoning 45, 1–24 (2010) · DOI
Cited by
Sorted by citations
Solving olympiad geometry without human demonstrations
Trinh, T. H., Wu, Y., Le, Q. V., He, H., & Luong, T. (2024) · Nature · doi:10.1038/s41586-023-06747-5 · Cited by 311
Metadata
- Authors
- Ye, Z., Chou, S.-C., & Gao, X.-S.
- Affiliations
- Zhejiang Gongshang University (CN)
- Wichita State University (US)
- Chinese Academy of Sciences (CN)
- Venue
- Lecture Notes in Computer Science
- Publisher
- Springer Berlin Heidelberg
- Published
- 2011
- Pages
- 189-195
- ISSN
- 0302-9743 (ISSN-L)
- 1611-3349
- OpenAlex
- W1431497170
- Cited by
- 50
- References
- 0
- Citations by year
- 2026: 1 · 2025: 2 · 2024: 6 · 2023: 6 · 2022: 5 · 2021: 7 · 2020: 4 · 2019: 4 · 2018: 5 · 2017: 2 · 2016: 1 · 2015: 2 · 2014: 1 · 2012: 1
- FWCI
- 3.86
- Type
- conference paper
- Language
- en
- Open access
- closed
- Locations
- Lecture notes in computer science (publishedVersion)
- Topics
- Physical Sciences › Mathematics › Geometry and Topology › Mathematics and Applications
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Polynomial and algebraic computation
- Social Sciences › Education › Mathematics Education and Teaching Techniques
- Keywords
- computer-aided geometry, plane geometry, proof automation, geometric drawing, geometric reasoning, interactive theorem proving
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
