References

  1. Nuno Baeta & Pedro Quaresma (2013): The full angle method on the OpenGeoProver. In: Christoph Lange, David Aspinall, Jacques Carette, James Davenport, Andrea Kohlhase, Michael Kohlhase, Paul Libbrecht, Pedro Quaresma, Florian Rabe, Petr Sojka, Iain Whiteside & Wolfgang Windsteiger: MathUI, OpenMath, PLMMS and ThEdu Workshops and Work in Progress at the Conference on Intelligent Computer Mathematics, CEUR Workshop Proceedings 1010, Aachen. Available at http://ceur-ws.org/Vol-1010/paper-08.pdf.
  2. Nuno Baeta & Pedro Quaresma (2019): Towards Ranking Geometric Automated Theorem Provers. In: Pedro Quaresma & Walther Neuper: Proceedings 7th International Workshop on, Electronic Proceedings in Theoretical Computer Science 290. Open Publishing Association, pp. 30–37, doi:10.4204/EPTCS.290.3.
  3. Ezio Bartocci, Dirk Beyer, Paul E. Black, Grigory Fedyukovich, Hubert Garavel, Arnd Hartmanns, Marieke Huisman, Fabrice Kordon, Julian Nagele, Mihaela Sighireanu, Bernhard Steffen, Martin Suda, Geoff Sutcliffe, Tjark Weber & Akihisa Yamada (2019): TOOLympics 2019: An Overview of Competitions in Formal Methods. In: Dirk Beyer, Marieke Huisman, Fabrice Kordon & Bernhard Steffen: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 11429. Springer International Publishing, pp. 3–24, doi:10.1007/978-3-030-17502-3_1.
  4. Dirk Beyer, Marieke Huisman, Fabrice Kordon & Bernhard Steffen (2019): Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics. LNCS 11429. Springer, doi:10.1007/978-3-030-17462-0.
  5. 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.
  6. Francisco Botana & Zoltán Kovács (2014): A Singular web service for geometric computations. Annals of Mathematics and Artificial Intelligence, pp. 1–12, doi:10.1007/s10472-014-9438-2.
  7. Francisco Botana, Zoltán Kovács & Simon Weitzhofer (2012): Implementing theorem proving in GeoGebra by using a Singular webservice. In: Proceedings EACA 2012, Libro de Resúmenes del XIII Encuentro de Álgebra Computacional y Aplicaciones. Universidad de Alcalá, pp. 67–70. Available at https://www.researchgate.net/publication/277475035_Implementing_Theorem_Proving_in_GeoGebra_by_Using_a_Singular_Webservice.
  8. David Braun, Nicolas Magaud & Pascal Schreck (2018): Formalizing Some ``Small'' Finite Models of Projective Geometry in Coq. In: Jacques Fleuriot, Dongming Wang & Jacques Calmet: Artificial Intelligence and Symbolic Computation. LNCS 11110, pp. 54–69. Springer, Cham, doi:10.1007/978-3-319-99957-9_4.
  9. Shang-Ching Chou, Xiao-Shan Gao & Jing-Zhong Zhang (1994): Machine Proofs in Geometry. World Scientific, doi:10.1142/2196.
  10. 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(13), pp. 325–347, doi:10.1007/BF00283133.
  11. 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(13), pp. 349–370, doi:10.1007/BF00283134.
  12. Xiao-Shan Gao (1999): Building Dynamic Mathematical Models with Geometry Expert, III. A Geometry Deductive Database. In: Proceedings Of ATCM'99. ATCM Inc., USA, pp. 153–162.
  13. Xiao-Shan Gao, C. C. Zhu & Y. Huang (1998.): Building Dynamic Mathematical Models with Geometry Expert, II. Linkage. In: Z. B. Li: Proceedings of the Third Asian Symposium on Computer Mathematics. LanZhou University Press, pp. 15–22.
  14. Xiao-Shan Gao & Qiang Lin (2004): MMP/Geometer - A Software Package for Automated Geometric Reasoning. Lecture Notes in Computer Science 2930, pp. 44–66, doi:10.1007/978-3-540-24616-9_4.
  15. Xiao-Shan Gao, C. C. Zhu & Y. Huang (1998): Building Dynamic Visual and Logic Models with Geometry Expert I. In: W.C. Yang: Proceedings of the Third Asian Technology Conference in Mathematics. Springer, pp. 216–226.
  16. Jean-David Génevaux, Julien Narboux & Pascal Schreck (2011): Formalization of Wu's Simple Method in Coq. In: Jean-Pierre Jouannaud & Zhong Shao: Certified Programs and Proofs. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 71–86, doi:10.1007/978-3-642-25379-9_8.
  17. Benjamin Grégoire, Loïc Pottier & Laurent Théry (2011): Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving. In: Thomas Sturm & Christoph Zengler: Automated Deduction in Geometry. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 42–59, doi:10.1007/978-3-642-21046-4_3.
  18. Predrag Janiči\'c (2006): GCLC \begingroupłet [Pleaseinsert\PrerenderUnicode—intopreamble] A Tool for Constructive Euclidean Geometry and More Than That. In: Andrés Iglesias & Nobuki Takayama: Mathematical Software - ICMS 2006, Lecture Notes in Computer Science 4151. Springer, pp. 58–73, doi:10.1007/11832225_6.
  19. 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.
  20. Zoltán Kovács (2015): The Relation Tool in GeoGebra 5. In: Francisco Botana & Pedro Quaresma: Automated Deduction in Geometry, Lecture Notes in Computer Science 9201. Springer, pp. 53–71, doi:10.1007/978-3-319-21362-0_4.
  21. Zoltán Kovács & Bernard Parisse (2015): Giac and GeoGebra – Improved Gröbner Basis Computations. In: Jaime Gutierrez, Josef Schicho & Martin Weimann: Computer Algebra and Polynomials, Lecture Notes in Computer Science. Springer, pp. 126–138, doi:10.1007/978-3-319-15081-9_7.
  22. Zoltán Kovács, Tomás Recio & Simon Weitzhofer (2012): Implementing theorem proving in GeoGebra by using exact check of a statement in a bounded number of test cases. In: Proceedings EACA 2012, Libro de Resúmenes del XIII Encuentro de Álgebra Computacional y Aplicaciones. Universidad de Alcalá, pp. 123–126. Available at https://www.researchgate.net/publication/265059624_Implementing_Theorem_Proving_in_GeoGebra_by_Exact_Check_of_a_Statement_in_a_Bounded_Number_of_Test_Cases.
  23. Julien Narboux (2009): Formalization of the Area Method. Coq user contribution. http://dpt-info.u-strasbg.fr/~narboux/area_method.html.
  24. Mladen Nikoli\'c, Vesna Marinkovi\'c, Zoltán Kovács & Predrag Janiči\'c (2018): Portfolio theorem proving and prover runtime prediction for geometry. Annals of Mathematics and Artificial Intelligence, pp. 1–28, doi:10.1007/s10472-018-9598-6.
  25. Ivan Petrovi\'c & Predrag Janiči\'c (2012): Integration of OpenGeoProver with GeoGebra. Available at http://argo.matf.bg.ac.rs/events/2012/fatpa2012/slides/IvanPetrovic.pdf.
  26. Loïc Pottier & Laurent Théry (1998): gbcoq. http://www-sop.inria.fr/croap/CFC/Gbcoq.html..
  27. Loïc Pottier (2008): Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics. Knowledge Exchange: Automated Provers and Proof Assistants 418. Available at http://arxiv.org/abs/1007.3615.
  28. 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.
  29. Pedro Quaresma & Nuno Baeta (2015): Current Status of the I2GATP Common Format. In: Francisco Botana & Pedro Quaresma: Automated Deduction in Geometry, Lecture Notes in Artificial Intelligence 9201. Springer, pp. 119–128, doi:10.1007/978-3-319-21362-0_8.
  30. Pedro Quaresma & Vanda Santos (2019): Proof Technology in Mathematics Research and Teaching, chapter Computer-generated geometry proofs in a learning context. Springer, doi:10.1007/978-3-030-28483-1.
  31. Pedro Quaresma, Vanda Santos, Pierluigi Graziani & Nuno Baeta (2019): Taxonomies of geometric problems. Journal of Symbolic Computation 97, pp. 31–55. Elsevier, doi:10.1016/j.jsc.2018.12.004.
  32. 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.
  33. Robert J. Stahl (1994): Using ``Think-Time'' and ``Wait-Time'' Skillfully in the Classroom. Technical Report. ERIC Digest. Available at http://files.eric.ed.gov/fulltext/ED370885.pdf.
  34. Sana Stojanovi\begingroupłet [Pleaseinsert\PrerenderUnicodećintopreamble], Vesna Pavlovi\begingroupłet [Pleaseinsert\PrerenderUnicodećintopreamble] & Predrag Jani\begingroupłet [Pleaseinsert\PrerenderUnicodečintopreamble]i\begingroupłet [Pleaseinsert\PrerenderUnicodećintopreamble] (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, Lecture Notes in Computer Science 6877. Springer Berlin Heidelberg, pp. 201–220, doi:10.1007/978-3-642-25070-5_12.
  35. Aaron Stump, Geoff Sutcliffe & Cesare Tinelli (2014): StarExec: A Cross-Community Infrastructure for Logic Solving. In: Stéphane Demri, Deepak Kapur & Christoph Weidenbach: Automated Reasoning. Springer International Publishing, Cham, pp. 367–373, doi:10.1007/978-3-319-08587-6_28.
  36. Dongming Wang (2004): GEOTHER 1.1: Handling and Proving Geometric Theorems Automatically. In: Franz Winkler: Automated Deduction in Geometry, Lecture Notes in Computer Science 2930. Springer, Berlin, Heidelberg, pp. 194–215, doi:10.1007/978-3-540-24616-9_12.
  37. 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.
  38. Wen-Tsun 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, Contemporary Mathematics 29. American Mathematical Society, doi:10.1090/conm/029/12.
  39. 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.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org