The DOI matches its Crossref record.
GRAMY: A Geometry Theorem Prover Capable of Construction
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
“Current approaches to geometry, therefore, still primarily rely on symbolic methods and human-designed, hard-coded search heuristics10–14.”
From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [11]
In the citing paper
“Previous methods to generate them are based on hand-crafted templates and domain-specific heuristics8–12, and are, therefore, limited by a subset of human experiences expressible in hard-coded rules.”
From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [11]
In the citing paper
“Geometry theorem proving of today, however, is still relying on human-designed heuristics for auxiliary constructions10–14.”
From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [11]
Citations
Cites
No references could be resolved yet.
Research works printed but not linked: 22
- Anderson, J. R., Boyle, C. F., Corbett, A. T. and Lewis, M. W. (1990) Cognitive modeling and intelligent tutoring, Artificial Intelligence 42(1), 7-49. · DOI
- Anzai, Y., Ishibashi, N., Mitsuya, Y. and Ura, S. (1979) Knowledge-based problem solving by a labelled production system, IJCAI, pp. 22-24.
- Aref, M. N. and Wernick, W. (1968) Problems & Solutions in Euclidean Geometry, Dover Publications, New York.
- Chou, S.-C. and Gao, X.-S. (1989) A class of geometry statements of constructive type and geometry theorem proving, Technical Report TR-89-37, Department of Computer Science, University of Texas at Austin.
- Chou, S.-C., Gao, X.-S. and Zhang, J.-Z. (1996) Automated generation of readable proofs with geometric invariants, I. Multiple and shortest proof generation, J. Automated Reasoning 17, 325-347. · DOI
- Chou, S.-C., Gao, X.-S. and Zhang, J.-Z. (2000) A deductive database approach to automated geometry theorem proving and discovering, J. Automated Reasoning 25(3), 219-246. · DOI · Paper page
- Coelho, H. and Pereira, L. M. (1986) Automated reasoning in geometry theorem proving with Prolog, J. Automated Reasoning 2(4), 329-390. · DOI
- Coxford, A. F. and Usiskin, Z. P. (1971) Geometry: A Transformation Approach, Laidlay Brothers, Palo Alto, CA.
- Elcock, E. W. (1977) Representation of knowledge in geometry machine, in E. W. Elcock and D. Michie (eds.), Machine Intelligence, Vol. 8, Wiley, pp. 11-29.
- Gelernter, H. (1959) Realization of a geometry-theorem proving machine, in Proceedings of the International Conference on Information Processing, pp. 273-282.
- Gelernter, H., Hansen, J. R. and Loveland, D. W. (1963) Empirical explorations of the geometry theorem proving machine, in E. A. Feigenbaum and J. Feldman (eds.), Computers and Thought, McGraw-Hill, pp. 153-163.
- Greeno, J. G., Magone, M. E. and Chaiklin, S. (1979) Theory of constructions and set in problem solving, Memory and Cognition 7(6), 445-461. · DOI
- Haralick, R. M. and Elliott, G. L. (1980) Increasing tree search efficiency for constraint satisfaction problems, Artificial Intelligence 14(3), 263-313. · DOI
- Kapur, D. (1986) Using Gröbner bases to reason about geometry problems, J. Symbolic Comput. 2(4), 399-408. · DOI
- Koedinger, K. R. and Anderson, J. R. (1990) Abstract planning and perceptual chunks: Elements of expertise in geometry, Cognitive Science 14(4), 511-550. · DOI
- Larkin, J. H. and Simon, H. A. (1987) Why a diagram is (sometimes) worth ten thousand words, Cognitive Science 11(1), 65-100. · DOI
- Li, H. (2000) Clifford algebra approaches to mechanical geometry theorem proving, in X.-S. Gao and D. Wang (eds.), Mathematics Mechanization and Applications, Academic Press, San Diego, CA, pp. 205-299.
- Nevins, A. J. (1975) Plane geometry theorem proving using forward chaining, Artificial Intelligence 6(1), 1-23. · DOI
- Suwa, M. and Motoda, H. (1989) Acquisition of associative knowledge by the frustration-based learning method in an auxiliary-line problem, Knowledge Acquisition 1(1), 113-137. · DOI
- VanLehn, K., Lynch, C., Taylor, L., Weinstein, A., Shelby, R., Schulze, K., Treacy, D. and Wintersgill, M. (2002) Minimally invasive tutoring of complex physics problem solving, in S. A. Cerri, G. Gouarderes and F. Paraguacu (eds.), Proceedings of the 6th International Conference on Intelligent Tutoring Systems, pp. 367-376. · DOI
- Wang, D. (1995) Reasoning about geometric problems using an elimination method, in J. Pfalzgraf and D. Wang (eds.), Automated Practical Reasoning, Springer, New York, pp. 147-185. · DOI
- Wu, W.-T. (2000) The characteristic set method and its application, in X.-S. Gao and D. Wang (eds.), Mathematics Mechanization and Applications, Academic Press, San Diego, CA, pp. 3-41.
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
- Matsuda, N., & VanLehn, K.
- Affiliations
- University of Pittsburgh (US)
- Venue
- Journal of Automated Reasoning
- Published
- 2004-01
- Volume
- 32
- Issue
- 1
- Pages
- 3-33
- ISSN
- 0168-7433 (ISSN-L)
- 1573-0670
- OpenAlex
- W2073911647
- Cited by
- 43
- References
- 0
- Citations by year
- 2025: 1 · 2024: 1 · 2023: 2 · 2022: 1 · 2021: 2 · 2020: 2 · 2019: 1 · 2018: 2 · 2017: 4 · 2016: 1 · 2015: 3 · 2014: 2 · 2012: 3
- FWCI
- 3.50
- Type
- journal article
- Language
- en
- Open access
- closed
- Licence
- Locations
- Journal of Automated Reasoning (publishedVersion)
- Topics
- Physical Sciences › Mathematics › Geometry and Topology › Mathematics and Applications
- Physical Sciences › Computer Science › Computational Theory and Mathematics › Polynomial and algebraic computation
- Physical Sciences › Computer Science › Software › Logic, programming, and type systems
- Keywords
- Euclidean geometry, geometric construction, backward chaining
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
