@inproceedings(amerkad_mathematics_2001,
 author       = {Ahmed Amerkad and Yves Bertot and Lo\IeC{\"\i}c Pottier and Laurence Rideau},
 year         = {2001},
 title        = {Mathematics and {Proof} {Presentation} in {Pcoq}},
 booktitle    = {Workshop {Proof} {Transformation} and {Presentation} and {Proof} {Complexities} in connection with {IJCAR} 2001},
 address      = {Siena},
)
@article(avigad_formal_2009,
 author       = {Jeremy Avigad and Edward Dean and John Mumma},
 year         = {2009},
 title        = {A {Formal} {System} for {Euclid}'s {Elements}},
 journal      = {The Review of Symbolic Logic},
 volume       = {2},
 pages        = {700--768},
 doi          = {10.1017/S1755020309990098},
)
@article(beeson_proof-checking_2019,
 author       = {Michael Beeson and Julien Narboux and Freek Wiedijk},
 year         = {2019},
 title        = {Proof-checking {Euclid}},
 journal      = {Annals of Mathematics and Artificial Intelligence},
 volume       = {85},
 number       = {2-4},
 pages        = {213--257},
 doi          = {10.1007/s10472-018-9606-x},
 note         = {Publisher: Springer},
)
@article(bertot_visualizing_2004,
 author       = {Yves Bertot and Fr\IeC{\'e}d\IeC{\'e}rique Guilhot and Lo\IeC{\"\i}c Pottier},
 year         = {2004},
 title        = {Visualizing {Geometrical} {Statements} with {GeoView}},
 journal      = {Proceedings of the Workshop User Interfaces for Theorem Provers 2003},
 volume       = {103},
 pages        = {49--65},
 doi          = {10.1016/j.entcs.2004.09.013},
)
@article(bertot_generic_1998,
 author       = {Yves Bertot and Laurent Thery},
 year         = {1998},
 title        = {A {Generic} {Approach} to {Building} {User} {Interfaces} for {Theorem} {Provers}},
 journal      = {The Journal of Symbolic Computation},
 volume       = {25},
 pages        = {161--194},
 doi          = {10.1006/jsco.1997.0171},
)
@inproceedings(bezem_automating_2005,
 author       = {Marc Bezem and Thierry Coquand},
 year         = {2005},
 title        = {Automating {Coherent} {Logic}},
 editor       = {Geoff Sutcliffe and Andrei Voronkov},
 booktitle    = {12th {International} {Conference} on {Logic} for {Programming}, {Artificial} {Intelligence}, and {Reasoning} \IeC{\textemdash} {LPAR} 2005},
 series       = {Lecture {Notes} in {Computer} {Science}},
 volume       = {3835},
 publisher    = {Springer-Verlag},
 pages        = {246--260},
 doi          = {10.1007/11591191\_18},
)
@article(botana_automated_2015,
 author       = {Francisco Botana and Markus Hohenwarter and Jani\IeC{\v c}i\IeC{\'c}, Predrag and Kov\IeC{\'a}cs, Zolt\IeC{\'a}n and Petrovi\IeC{\'c}, Ivan and Tom\IeC{\'a}s Recio and Simon Weitzhofer},
 year         = {2015},
 title        = {Automated {Theorem} {Proving} in {GeoGebra}: {Current} {Achievements}},
 journal      = {Journal of Automated Reasoning},
 volume       = {55},
 number       = {1},
 pages        = {39--59},
 doi          = {10.1007/s10817-015-9326-4},
)
@article(chou_automated_1996-1,
 author       = {Shang-Ching Chou and Xiao-Shan Gao and Ji Zhang},
 year         = {1996},
 title        = {Automated {Generation} of {Readable} {Proofs} with {Geometric} {Invariants}, {II}. {Theorem} {Proving} {With} {Full}-{Angles}},
 journal      = {Journal of Automated Reasoning},
 volume       = {17},
 number       = {13},
 pages        = {349--370},
 doi          = {10.1007/BF00283134},
)
@book(coq_development_team_the_coq_2010,
 author       = {{Coq development team, The}},
 year         = {2010},
 title        = {The {Coq} proof assistant reference manual, {Version} 8.3},
 publisher    = {LogiCal Project},
 url          = {http://coq.inria.fr},
)
@article(dyckhoff_geometrization_2015,
 author       = {Roy Dyckhoff and Sara Negri},
 year         = {2015},
 title        = {Geometrization of first-order logic},
 journal      = {The Bulletin of Symbolic Logic},
 volume       = {21},
 pages        = {123--163},
 doi          = {10.1017/bsl.2015.7},
)
@article(ganesalingam_fully_2013,
 author       = {M. Ganesalingam and W. T. Gowers},
 year         = {2013},
 title        = {A fully automatic problem solver with human-style output},
 journal      = {CoRR},
 volume       = {abs/1309.4501},
)
@inproceedings(gao_mmp/geometer_2004,
 author       = {Xiao-Shan Gao and Qiang Lin},
 year         = {2004},
 title        = {{MMP}/{Geometer} - {A} {Software} {Package} for {Automated} {Geometric} {Reasoning}},
 booktitle    = {Proceedings of {Automated} {Deduction} in {Geometry} ({ADG02})},
 series       = {Lecture {Notes} in {Computer} {Science}},
 volume       = {2930},
 publisher    = {Springer-Verlag},
 pages        = {44--66},
 doi          = {10.1007/978-3-540-24616-9\_4},
)
@inproceedings(gelernter_empirical_1960,
 author       = {Herbert Gelernter and J. R. Hansen and Donald Loveland},
 year         = {1960},
 title        = {Empirical explorations of the geometry theorem machine},
 booktitle    = {Papers presented at the {May} 3-5, 1960, western joint {IRE}-{AIEE}-{ACM} computer conference},
 series       = {{IRE}-{AIEE}-{ACM} '60 ({Western})},
 publisher    = {ACM},
 address      = {San Francisco, California},
 pages        = {143--149},
 doi          = {10.1145/1460361.1460381},
)
@incollection(janicic_gclc_2006,
 author       = {Jani\IeC{\v c}i\IeC{\'c}, Predrag},
 year         = {2006},
 title        = {{GCLC} \IeC{\textemdash} {A} {Tool} for {Constructive} {Euclidean} {Geometry} and {More} {Than} {That}},
 editor       = {Andr\IeC{\'e}s Iglesias and Nobuki Takayama},
 booktitle    = {Mathematical {Software} - {ICMS} 2006},
 series       = {Lecture {Notes} in {Computer} {Science}},
 volume       = {4151},
 publisher    = {Springer},
 pages        = {58--73},
 doi          = {10.1007/11832225\_6},
)
@unpublished(janicic_gclc_2009,
 author       = {Jani\IeC{\v c}i\IeC{\'c}, Predrag},
 year         = {2009},
 title        = {{GCLC} 9.0/{WinGCLC} 2009},
 note         = {Manual for the GCLC Dynamic Geometry Software},
)
@article(janicic_geometry_2010,
 author       = {Jani\IeC{\v c}i\IeC{\'c}, Predrag},
 year         = {2010},
 title        = {Geometry {Constructions} {Language}},
 journal      = {Journal of Automated Reasoning},
 volume       = {44},
 number       = {1-2},
 pages        = {3--24},
 doi          = {10.1007/s10817-009-9135-8},
)
@misc(janicic_theorem_2021,
 author       = {Jani\IeC{\v c}i\IeC{\'c}, Predrag and Julien Narboux},
 year         = {2021},
 title        = {Theorem {Proving} as {Constraint} {Solving} with {Coherent} {Logic}},
 note         = {Submitted},
)
@book(maclane_sheaves_1992,
 author       = {Saunders MacLane and Ieke Moerdijk},
 year         = {1992},
 title        = {Sheaves in geometry and logic: a first introduction to topos theory},
 publisher    = {Springer-Verlag},
)
@phdthesis(miller_diagrammatic_2001,
 author       = {Nathaniel Miller},
 year         = {2001},
 title        = {A diagrammatic formal system for {Euclidean} geometry},
 school       = {Cornell University},
)
@article(narboux_graphical_2007,
 author       = {Julien Narboux},
 year         = {2007},
 title        = {A {Graphical} {User} {Interface} for {Formal} {Proofs} in {Geometry}},
 journal      = {Journal of Automated Reasoning},
 volume       = {39},
 number       = {2},
 pages        = {161--180},
 doi          = {10.1007/s10817-007-9071-4},
)
@incollection(narboux_combining_2021,
 author       = {Julien Narboux and Durand-Guerrier, Viviane},
 year         = {2021},
 title        = {Combining pencil/paper proofs and formal proofs, a challenge for {Artificial} {Intelligence} and mathematics education},
 booktitle    = {Mathematics {Education} in the {Age} of {Artificial} {Intelligence}: {How} {Intelligence} can serve mathematical human learning},
 publisher    = {Springer},
 note         = {In press},
)
@inproceedings(nivelle_geometric_2006,
 author       = {Hans de Nivelle and Jia Meng},
 year         = {2006},
 title        = {Geometric {Resolution}: {A} {Proof} {Procedure} {Based} on {Finite} {Model} {Search}},
 editor       = {Ulrich Furbach and Natarajan Shankar},
 booktitle    = {Automated {Reasoning}, {Third} {International} {Joint} {Conference}, {IJCAR} 2006, {Seattle}, {WA}, {USA}, {August} 17-20, 2006, {Proceedings}},
 series       = {Lecture {Notes} in {Computer} {Science}},
 volume       = {4130},
 publisher    = {Springer},
 pages        = {303--317},
 doi          = {10.1007/11814771\_28},
)
@article(pham_combination_2012,
 author       = {Tuan Minh Pham and Yves Bertot},
 year         = {2012},
 title        = {A {Combination} of a {Dynamic} {Geometry} {Software} {With} a {Proof} {Assistant} for {Interactive} {Formal} {Proofs}},
 journal      = {Electron. Notes Theor. Comput. Sci.},
 volume       = {285},
 pages        = {43--55},
 doi          = {10.1016/j.entcs.2012.06.005},
)
@phdthesis(polonsky_proofs_2011,
 author       = {Andrew Polonsky},
 year         = {2011},
 title        = {Proofs, {Types} and {Lambda} {Calculus}},
 school       = {University of Bergen},
)
@article(sutcliffe_tptp_2009,
 author       = {G. Sutcliffe},
 year         = {2009},
 title        = {The {TPTP} {Problem} {Library} and {Associated} {Infrastructure}: {The} {FOF} and {CNF} {Parts}, v3.5.0},
 journal      = {Journal of Automated Reasoning},
 volume       = {43},
 number       = {4},
 pages        = {337--362},
 doi          = {10.1007/s10817-009-9143-8},
)
@inproceedings(vickers_geometric_1993,
 author       = {Steven Vickers},
 year         = {1993},
 title        = {Geometric {Logic} in {Computer} {Science}},
 booktitle    = {Theory and {Formal} {Methods}},
 series       = {Workshops in {Computing}},
 publisher    = {Springer},
 pages        = {37--54},
 doi          = {10.1007/978-1-4471-3503-6\_4},
)
@inproceedings(wang_automated_2003,
 author       = {Dongming Wang},
 year         = {2003},
 title        = {Automated {Generation} of {Diagrams} with {Maple} and {Java}},
 editor       = {Michael Joswig and Nobuki Takayama},
 booktitle    = {Algebra, {Geometry} and {Software} {Systems}},
 publisher    = {Springer},
 address      = {Berlin, Heidelberg},
 pages        = {277--287},
 doi          = {10.1007/978-3-662-05148-1\_15},
)
@inproceedings(wilson_combining_2005,
 author       = {Sean Wilson and Jacques D. Fleuriot},
 year         = {2005},
 title        = {Combining {Dynamic} {Geometry}, {Automated} {Geometry} {Theorem} {Proving} and {Diagrammatic} {Proofs}},
 booktitle    = {{ETAPS} {Satellite} {Workshop} on {User} {Interfaces} for {Theorem} {Provers} ({UITP})},
 publisher    = {Springer},
 address      = {Edinburgh},
)
@inproceedings(winterstein_dr.doodle:_2004,
 author       = {Daniel Winterstein},
 year         = {2004},
 title        = {Dr.{Doodle}: {A} {Diagrammatic} {Theorem} {Prover}},
 booktitle    = {Proceedings of {IJCAR} 2004},
 doi          = {10.1007/978-3-540-25984-8\_24},
)
@article(ye_visually_2009,
 author       = {Zheng Ye and Shang-Ching Chou and Xiao-Shan Gao},
 year         = {2010},
 title        = {Visually {Dynamic} {Presentation} of {Proofs} in {Plane} {Geometry}},
 journal      = {Journal of Automated Reasoning},
 volume       = {45},
 number       = {3},
 pages        = {243--266},
 doi          = {10.1007/s10817-009-9163-4},
)
@article(ye_visually_2010,
 author       = {Zheng Ye and Shang-Ching Chou and Xiao-Shan Gao},
 year         = {2010},
 title        = {Visually {Dynamic} {Presentation} of {Proofs} in {Plane} {Geometry}, {Part} 1},
 journal      = {J. Autom. Reason.},
 volume       = {45},
 number       = {3},
 pages        = {213--241},
 doi          = {10.1007/s10817-009-9162-5},
)
@inproceedings(ye_introduction_2011,
 author       = {Zheng Ye and Shang-Ching Chou and Xiao-Shan Gao},
 year         = {2011},
 title        = {An {Introduction} to {Java} {Geometry} {Expert}},
 booktitle    = {Post-proceedings of {Automated} {Deduction} in {Geometry} ({ADG} 2008)},
 series       = {Lecture {Notes} in {Computer} {Science}},
 volume       = {6301},
 publisher    = {Springer-Verlag},
 pages        = {189--195},
 doi          = {10.1007/978-3-642-21046-4\_10},
)