References

  1. Ahmed Amerkad, Yves Bertot, Loïc Pottier & Laurence Rideau (2001): Mathematics and Proof Presentation in Pcoq. In: Workshop Proof Transformation and Presentation and Proof Complexities in connection with IJCAR 2001, Siena.
  2. Jeremy Avigad, Edward Dean & John Mumma (2009): A Formal System for Euclid's Elements. The Review of Symbolic Logic 2, pp. 700–768, doi:10.1017/S1755020309990098.
  3. Michael Beeson, Julien Narboux & Freek Wiedijk (2019): Proof-checking Euclid. Annals of Mathematics and Artificial Intelligence 85(2-4), pp. 213–257, doi:10.1007/s10472-018-9606-x. Publisher: Springer.
  4. Yves Bertot, Frédérique Guilhot & Loïc Pottier (2004): Visualizing Geometrical Statements with GeoView. Proceedings of the Workshop User Interfaces for Theorem Provers 2003 103, pp. 49–65, doi:10.1016/j.entcs.2004.09.013.
  5. Yves Bertot & Laurent Thery (1998): A Generic Approach to Building User Interfaces for Theorem Provers. The Journal of Symbolic Computation 25, pp. 161–194, doi:10.1006/jsco.1997.0171.
  6. Marc Bezem & Thierry Coquand (2005): Automating Coherent Logic. In: Geoff Sutcliffe & Andrei Voronkov: 12th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning LPAR 2005, Lecture Notes in Computer Science 3835. Springer-Verlag, pp. 246–260, doi:10.1007/11591191_18.
  7. 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.
  8. Shang-Ching Chou, Xiao-Shan Gao & Ji 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.
  9. Coq development team, The (2010): The Coq proof assistant reference manual, Version 8.3. LogiCal Project. Available at http://coq.inria.fr.
  10. Roy Dyckhoff & Sara Negri (2015): Geometrization of first-order logic. The Bulletin of Symbolic Logic 21, pp. 123–163, doi:10.1017/bsl.2015.7.
  11. M. Ganesalingam & W. T. Gowers (2013): A fully automatic problem solver with human-style output. CoRR abs/1309.4501.
  12. Xiao-Shan Gao & Qiang Lin (2004): MMP/Geometer - A Software Package for Automated Geometric Reasoning. In: Proceedings of Automated Deduction in Geometry (ADG02), Lecture Notes in Computer Science 2930. Springer-Verlag, pp. 44–66, doi:10.1007/978-3-540-24616-9_4.
  13. Herbert Gelernter, J. R. Hansen & Donald Loveland (1960): Empirical explorations of the geometry theorem machine. In: Papers presented at the May 3-5, 1960, western joint IRE-AIEE-ACM computer conference, IRE-AIEE-ACM '60 (Western). ACM, San Francisco, California, pp. 143–149, doi:10.1145/1460361.1460381.
  14. Predrag Janiči\'c (2006): GCLC 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.
  15. Predrag Janiči\'c (2009): GCLC 9.0/WinGCLC 2009. Manual for the GCLC Dynamic Geometry Software.
  16. Predrag Janiči\'c (2010): Geometry Constructions Language. Journal of Automated Reasoning 44(1-2), pp. 3–24, doi:10.1007/s10817-009-9135-8.
  17. Predrag Janiči\'c & Julien Narboux (2021): Theorem Proving as Constraint Solving with Coherent Logic. Submitted.
  18. Saunders MacLane & Ieke Moerdijk (1992): Sheaves in geometry and logic: a first introduction to topos theory. Springer-Verlag.
  19. Nathaniel Miller (2001): A diagrammatic formal system for Euclidean geometry. Cornell University.
  20. Julien Narboux (2007): A Graphical User Interface for Formal Proofs in Geometry. Journal of Automated Reasoning 39(2), pp. 161–180, doi:10.1007/s10817-007-9071-4.
  21. Julien Narboux & Viviane Durand-Guerrier (2021): Combining pencil/paper proofs and formal proofs, a challenge for Artificial Intelligence and mathematics education. In: Mathematics Education in the Age of Artificial Intelligence: How Intelligence can serve mathematical human learning. Springer. In press.
  22. Hans de Nivelle & Jia Meng (2006): Geometric Resolution: A Proof Procedure Based on Finite Model Search. In: Ulrich Furbach & Natarajan Shankar: Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, Lecture Notes in Computer Science 4130. Springer, pp. 303–317, doi:10.1007/11814771_28.
  23. Tuan Minh Pham & Yves Bertot (2012): A Combination of a Dynamic Geometry Software With a Proof Assistant for Interactive Formal Proofs. Electron. Notes Theor. Comput. Sci. 285, pp. 43–55, doi:10.1016/j.entcs.2012.06.005.
  24. Andrew Polonsky (2011): Proofs, Types and Lambda Calculus. University of Bergen.
  25. G. Sutcliffe (2009): The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning 43(4), pp. 337–362, doi:10.1007/s10817-009-9143-8.
  26. Steven Vickers (1993): Geometric Logic in Computer Science. In: Theory and Formal Methods, Workshops in Computing. Springer, pp. 37–54, doi:10.1007/978-1-4471-3503-6_4.
  27. Dongming Wang (2003): Automated Generation of Diagrams with Maple and Java. In: Michael Joswig & Nobuki Takayama: Algebra, Geometry and Software Systems. Springer, Berlin, Heidelberg, pp. 277–287, doi:10.1007/978-3-662-05148-1_15.
  28. Sean Wilson & Jacques D. Fleuriot (2005): Combining Dynamic Geometry, Automated Geometry Theorem Proving and Diagrammatic Proofs. In: ETAPS Satellite Workshop on User Interfaces for Theorem Provers (UITP). Springer, Edinburgh.
  29. Daniel Winterstein (2004): Dr.Doodle: A Diagrammatic Theorem Prover. In: Proceedings of IJCAR 2004, doi:10.1007/978-3-540-25984-8_24.
  30. Zheng Ye, Shang-Ching Chou & Xiao-Shan Gao (2010): Visually Dynamic Presentation of Proofs in Plane Geometry. Journal of Automated Reasoning 45(3), pp. 243–266, doi:10.1007/s10817-009-9163-4.
  31. Zheng Ye, Shang-Ching Chou & Xiao-Shan Gao (2010): Visually Dynamic Presentation of Proofs in Plane Geometry, Part 1. J. Autom. Reason. 45(3), pp. 213–241, doi:10.1007/s10817-009-9162-5.
  32. Zheng Ye, Shang-Ching Chou & Xiao-Shan Gao (2011): An Introduction to Java Geometry Expert. In: Post-proceedings of Automated Deduction in Geometry (ADG 2008), Lecture Notes in Computer Science 6301. Springer-Verlag, 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