Reynald Affeldt & Cyril Cohen (2017):
Formal foundations of 3D geometry to model robot manipulators.
In: Yves Bertot & Viktor Vafeiadis: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017.
ACM,
pp. 30–42,
doi:10.1145/3018610.3018629.
P. O. Bell (1955):
Generalized Theorems of Desargues for n-Dimensional Projective Space.
Proceedings of the American Mathematical Society 6(5),
pp. 675–681,
doi:10.2307/2032913.
Available at http://www.jstor.org/stable/2032913.
Francisco Botana, Markus Hohenwarter, Predrag Janicic, Zoltán Kovács, Ivan Petrovi\'c, Tomas Recio & Simon Weitzhofer (2015):
Automated Theorem Proving in GeoGebra: Current Achievements.
Journal of Automated Reasoning 55,
pp. 39–59,
doi:10.1007/s10817-015-9326-4.
D. Braun, N. Magaud & P. Schreck (2021):
Two New Ways to Formally Prove Dandelin-Gallucci's Theorem.
In: ISSAC 2021 : International Symposium on Symbolic and Algebraic Computation.
ACM,
doi:10.1145/3452143.3465550.
David Braun (2019):
Approche combinatoire pour l'automatisation en Coq des preuves formelles en géométrie d'incidence projective.
Université de Strasbourg.
David Braun, Nicolas Magaud & Pascal Schreck (2019):
Two cryptomorphic formalizations of projective incidence geometry.
Ann. Math. Artif. Intell. 85(2-4),
pp. 193–212,
doi:10.1007/s10472-018-9604-z.
Shang-Ching Chou, Xiao-Shan Gao & Jing-Zhong Zhang (1994):
Machine Proofs in Geometry.
Series on Applied Mathematics.
World Scientific,
doi:10.1142/2196.
Jack Edmonds (1971):
Matroids and the greedy algorithm.
Mathematical Programming 1(1),
pp. 127–136,
doi:10.1007/BF01584082.
Laurent Fuchs & Laurent Théry (2010):
A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry.
In: Pascal Schreck, Julien Narboux & Jürgen Richter-Gebert: Automated Deduction in Geometry - 8th International Workshop, 2010, Munich, Germany, July 22-24, 2010, Revised Selected Papers,
Lecture Notes in Computer Science 6877.
Springer,
pp. 51–67,
doi:10.1007/978-3-642-25070-5_3.
H. Gelernter (1959):
Realization of a Geometry Theorem-Proving Machine.
In: Proc. of the International Conference on Information Processing.
UNESCO,
pp. 273–281,
doi:10.5555/216408.216418.
Ákos G Horváth (2017):
Gallucci's axiom revisited.
In: arXiv preprint arXiv:1712.04800.
Predrag Janicic, Julien Narboux & Pedro Quaresma (2010):
The Area Method.
Journal of Automated Reasoning - JAR 48,
doi:10.1007/s10817-010-9209-7.
Magaud, Nicolas and Narboux, Julien and Schreck, Pascal (2012):
A Case Study in Formalizing Projective Geometry in Coq: Desargues Theorem.
Computational Geometry : Theory and Applications 45(8),
pp. 406–424,
doi:10.1016/j.comgeo.2010.06.004.
Dominique Michelucci & Pascal Schreck (2006):
Incidence Constraints: a Combinatorial Approach.
Int. Journal of Computational Geometry and Applications 16(5-6),
pp. 443–460,
doi:10.1142/S0218195906002130.
Forest Ray Moulton (1902):
A Simple Non-Desarguesian Plane Geometry.
Transactions of the American Mathematical Society 3(2),
pp. 192–195,
doi:10.1090/S0002-9947-1902-1500595-3.
James G Oxley (2006):
Matroid Theory 3.
Oxford University Press, USA.
Eugenio Roanes-Macías & Eugenio Roanes-Lozano (2006):
A Maple Package for Automatic Theorem Proving and Discovery in 3D-Geometry.
In: Francisco Botana & Tomás Recio: Automated Deduction in Geometry, 6th International Workshop, ADG 2006, Pontevedra, Spain, Aug. 31-Sept. 2, 2006. Revised Papers,
Lecture Notes in Computer Science 4869.
Springer,
pp. 171–188,
doi:10.1007/978-3-540-77356-6_11.
William Thomas Tutte (1959):
Matroids and graphs.
Transactions of the American Mathematical Society 90(3),
pp. 527–552,
doi:10.2307/1993185.
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,
doi:10.1007/s10817-009-9163-4.
eptcs@eptcs.org