Francisco Botana, Markus Hohenwarter, Predrag Janiči\'c, Zoltán Kovács, Ivan Petrovi\'c, Tomás Recio & Simon Weitzhofer (2015):
Automated Theorem Proving in GeoGebra: Current Achievements.
Journal of Automated Reasoning 55(1),
pp. 39–59,
doi:10.1007/s10817-015-9326-4.
Francisco Botana & Pedro Quaresma (2015):
Automated Deduction in Geometry, 10th International Workshop, ADG 2014.
Lecture Notes in Artificial Intelligence 9201.
Springer,
doi:10.1007/978-3-319-21362-0.
Pierre Boutry, Julien Narboux, Pascal Schreck & Gabriel Braun (2014):
Using small scale automation to improve both accessibility and readability of formal proofs in geometry.
In: Francisco Botana & Pedro Quaresma: Preliminary Proceedings of the 10th International Workshop on Automated Deduction in Geometry, ADG 2014, Coimbra, Portugal, 9–11 July, 2014,
CISUC Tech Reports TR 2014/01,
pp. 31–49.
Available at https://www.cisuc.uc.pt/ckfinder/userfiles/files/TR 2014-01.pdf.
Nicolaas Govert de Bruijn (1994):
A Survey of the Project Automath, chapter A Survey of the Project Automath,
pp. 141–161,
Studies in Logic and the Foundations of Mathematics 133.
North Holland,
doi:10.1016/S0049-237X(08)70203-9.
S.C. Chou (1985):
Proving and discovering geometry theorems using Wu's method.
The University of Texas, Austin.
Shang-Ching Chou (1988):
Mechanical Geometry Theorem Proving.
Mathematics and Its Applications 41.
D. Reidel Publishing Company.
Shang-Ching Chou, Xiao-Shan Gao & Jing-Zhong Zhang (1994):
A Collection of 110 Geometry Theorems and Their Machine Produced Proofs Using Full-Angles.
Technical Report TR-94-4.
Department of Computer Science, Wichita State University.
Available at https://www.researchgate.net/publication/239564904.
Shang-Ching Chou, Xiao-Shan Gao & Jing-Zhong Zhang (1996):
Automated Generation of Readable Proofs with Geometric Invariants: I. Multiple and Shortest Proof Generation.
Journal of Automated Reasoning 17(3),
pp. 325–347,
doi:10.1007/bf00283133.
Shang-Ching Chou, Xiao-Shan Gao & Jing-Zhong Zhang (1996):
Automated Generation of Readable Proofs with Geometric Invariants: II. Theorem Proving With Full-Angles.
Journal of Automated Reasoning 17(3),
pp. 349–370,
doi:10.1007/BF00283134.
Shang-Ching Chou, Xiao-Shan Gao & Jing-Zhong Zhang (2000):
A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering.
Journal of Automated Reasoning 25(3),
pp. 219–246,
doi:10.1023/A:1006171315513.
Helder Coelho & Luis Moniz Pereira (1986):
Automated Reasoning in Geometry Theorem Proving with Prolog.
Journal of Automated Reasoning 2(4),
pp. 329–390,
doi:10.1007/BF00248249.
H. Gelernter (1995):
Realization of a geometry-theorem proving machine.
In: Computers & thought.
MIT Press,
Cambridge, MA, USA,
pp. 134–152 * .
Predrag Janiči\'c, Julien Narboux & Pedro Quaresma (2012):
The Area Method: A Recapitulation.
Journal of Automated Reasoning 48(4),
pp. 489–532,
doi:10.1007/s10817-010-9209-7.
Predrag Janiči\'c & Pedro Quaresma (2006):
System Description: GCLCprover + GeoThms.
In: Ulrich Furbach & Natarajan Shankar: Automated Reasoning: Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17–20, 2006, Proceedings,
Lecture Notes in Artificial Intelligence 4130.
Springer,
pp. 145–150,
doi:10.1007/11814771_13.
Predrag Janiči\'c & Pedro Quaresma (2007):
Automatic Verification of Regular Constructions in Dynamic Geometry Systems.
In: Francisco Botana & Tomás Recio: Automated Deduction in Geometry: 6th International Workshop, ADG 2006, Pontevedra, Spain, August 31–September 2, 2006, Revised Papers,
Lecture Notes in Artificial Intelligence 4869.
Springer,
pp. 39–51,
doi:10.1007/978-3-540-77356-6_3.
Jianguo Jiang & Jingzhong Zhang (2012):
A review and prospect of readable machine proofs for geometry theorems.
Journal of Systems Science and Complexity 25(4),
pp. 802–820,
doi:10.1007/s11424-012-2048-3.
Deepak Kapur (1986):
Using Gröbner bases to reason about geometry problems.
Journal of Symbolic Computation 2(4),
pp. 399–408,
doi:10.1016/S0747-7171(86)80007-4.
Zoltán Kovács (2015):
The Relation Tool in GeoGebra 5,
pp. 53–71,
Lecture Notes in Artificial Intelligence 9201.
Springer International Publishing,
doi:10.1007/978-3-319-21362-0_4.
H. Li (2000):
Clifford algebra approaches to mechanical geometry theorem proving.
In: X.-S. Gao & D. Wang: Mathematics Mechanization and Applications.
Academic Press,
San Diego, CA,
pp. 205–299,
doi:10.1016/B978-012734760-8/50009-0.
Julien Narboux (2009):
Formalization of the Area Method.
Coq user contribution.
http://dpt-info.u-strasbg.fr/~narboux/area_method.html.
Juan Paneque, Pedro Cobo, Josep Fortuny & Philippe R. Richard (2016):
Argumentative Effects of a Geometric Construction Tutorial System in Solving Problems of Proof.
In: Proceedings of the 4th International Workshop on Theorem proving components for Educational software July 15, 2015 Washington, D.C., USA,
CISUC Technical Reports 2016-001,
pp. 13–35.
Available at https://www.cisuc.uc.pt/ckfinder/userfiles/files/TR 2016-01.pdf.
Pedro Quaresma (2011):
Thousands of Geometric Problems for Geometric Theorem Provers (TGTP).
In: Pascal Schreck, Julien Narboux & Jürgen Richter-Gebert: Automated Deduction in Geometry,
Lecture Notes in Computer Science 6877.
Springer,
pp. 169–181,
doi:10.1007/978-3-642-25070-5_10.
Pedro Quaresma (2017):
Towards an Intelligent and Dynamic Geometry Book.
Mathematics in Computer Science 11(3–4),
pp. 427–437,
doi:10.1007/s11786-017-0302-8.
Pedro Quaresma & Nuno Baeta (2015):
Current Status of the I2GATP Common Format.
In: Francisco Botana & Pedro Quaresma: Automated Deduction in Geometry: 10th International Workshop, ADG 2014, Coimbra, Portugal, July 9–1, 2014, Revised Selected Papers,
Lecture Notes in Artificial Intelligence 9201.
Springer,
pp. 119–128,
doi:10.1007/978-3-319-21362-0_8.
Pedro Quaresma, Vanda Santos, Pierluigi Graziani & Nuno Baeta (2019):
Taxonomies of geometric problems.
Journal of Symbolic Computation.
(in press),
doi:10.1016/j.jsc.2018.12.004.
Philippe Richard, Pedro Cobo, Josep Fortuny & Markus Hohenwarter (2009):
Training teachers to manage problem-solving classes with computer support.
Revista de Inform\begingroupłet [Pleaseinsert\PrerenderUnicodeáintopreamble]tica Aplicada / Journal of Applied Computing 5(1),
pp. 38–50,
doi:10.13037/rasvol5n1.
Mary Budd Rowe (1972):
Wait-Time and Rewards as Instructional Variables: Their Influence on Language, Logic, and Fate Control.
Technical Report.
National Association for Research in Science Teaching.
Available at https://files.eric.ed.gov/fulltext/ED061103.pdf.
Sana Stojanovi\'c, Vesna Pavlovi\'c & Predrag Janiči\'c (2011):
A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs.
In: Pascal Schreck, Julien Narboux & Jürgen Richter-Gebert: Automated Deduction in Geometry: 8th International Workshop, ADG 2010, Munich, Germany, July 22-24, 2010, Revised Selected Papers,
Lecture Notes in Artificial Intelligence 6877.
Springer,
pp. 201–220,
doi:10.1007/978-3-642-25070-5_12.
Geoffrey Sutcliffe (2016):
The 8th IJCAR automated theorem proving system competition - CASC-J8.
AI Communications 29(5),
pp. 607–619,
doi:10.3233/AIC-160709.
D. Wang (1995):
Reasoning about geometric problems using an elimination method.
In: J. Pfalzgraf & D. Wang: Automated Pratical Reasoning.
Springer,
New York,
pp. 147–185,
doi:10.1007/978-3-7091-6604-8_8.
Freek Wiedijk (2000):
The de Bruijn factor.
Poster at International Conference on Theorem Proving in Higher Order Logics (TPHOL2000).
Portland, Oregon, USA, 14-18 August 2000.
W.T. Wu (1984):
Automated Theorem Proving: After 25 Years, chapter On the decision problem and the mechanization of theorem proving in elementary geometry,
pp. 213–234 29.
American Mathematical Society,
doi:10.1090/conm/029.
Zheng Ye, Shang-Ching Chou & Xiao-Shan Gao (2010):
Visually Dynamic Presentation of Proofs in Plane Geometry: Part 1. Basic Features and the Manual Input Method.
Journal of Automated Reasoning 45(3),
pp. 213–241,
doi:10.1007/s10817-009-9162-5.
Zheng Ye, Shang-Ching Chou & Xiao-Shan Gao (2010):
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(3),
pp. 243–266,
doi:10.1007/s10817-009-9163-4.
Zheng Ye, Shang-Ching Chou & Xiao-Shan Gao (2011):
An Introduction to Java Geometry Expert.
In: Thomas Sturm & Christoph Zengler: Automated Deduction in Geometry,
Lecture Notes in Computer Science 6301.
Springer Berlin Heidelberg,
pp. 189–195,
doi:10.1007/978-3-642-21046-4_10.
Jing-Zhong Zhang, Shang-Ching Chou & Xiao-Shan Gao (1995):
Automated production of traditional proofs for theorems in Euclidean geometry: I. The Hilbert intersection point theorems.
Annals of Mathematics and Artificial Intelligence 13(1–2),
pp. 109–137,
doi:10.1007/BF01531326.