@(geocoq,
 author       = {Michael Beeson and Pierre Boutry and Gabriel Braun and Charly Gries and Julien Narboux},
 title        = {GeoCoq},
 url          = {https://hal.inria.fr/hal-01912024},
)
@inproceedings(coqtextbook,
 author       = {Sebastian B\"ohne and Christoph Kreitz},
 year         = {2018},
 title        = {Learning how to Prove: From the Coq Proof Assistant to Textbook Style},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {{\rm Proceedings 6th International Workshop on} Theorem proving components for Educational software, {\rm Gothenburg, Sweden, 6 Aug 2017}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {267},
 publisher    = {Open Publishing Association},
 pages        = {1--18},
 doi          = {10.4204/EPTCS.267.1},
)
@article(geocoqarticle,
 author       = {Pierre Boutry and Gabriel Braun and Julien Narboux},
 year         = {2018},
 title        = {{Formalization of the Arithmetization of Euclidean Plane Geometry and Applications}},
 journal      = {{Journal of Symbolic Computation}},
 pages        = {23},
 doi          = {10.1016/j.jsc.2018.04.007},
 url          = {https://hal.inria.fr/hal-01483457},
 note         = {To appear},
)
@article(geocoqarticle2,
 author       = {Gabriel Braun and Julien Narboux},
 year         = {2017},
 title        = {{A synthetic proof of Pappus' theorem in Tarski's geometry}},
 journal      = {{Journal of Automated Reasoning}},
 volume       = {58},
 number       = {2},
 pages        = {23},
 doi          = {10.1007/s10817-016-9374-4},
 url          = {https://hal.inria.fr/hal-01176508},
)
@article(pandora,
 author       = {Krysia Broda and Jiefei Ma and Gabrielle Sinnadurai and Alexander Summers},
 year         = {2007},
 title        = {Pandora: A Reasoning Toolbox using Natural Deduction Style},
 journal      = {Logic Journal of the IGPL},
 volume       = {15},
 number       = {4},
 pages        = {293--304},
 doi          = {10.1093/jigpal/jzm020},
)
@(xena,
 author       = {Kevin Buzzard},
 title        = {Xena},
 url          = {https://xenaproject.wordpress.com/},
)
@inproceedings(csedu,
 author       = {Maximilian Dor\'e and Krysia Broda},
 year         = {2018},
 title        = {The ELFE System - Verifying Mathematical Proofs of Undergraduate Students},
 booktitle    = {Proceedings of the 10th International Conference on Computer Supported Education (CSEDU)},
 volume       = {2},
 organization = {INSTICC},
 publisher    = {SciTePress},
 pages        = {15--26},
 doi          = {10.5220/0006681000150026},
)
@inproceedings(springer,
 author       = {Maximilian Dor\'e and Krysia Broda},
 year         = {2018},
 title        = {Intuitive reasoning in formalized mathematics with Elfe},
 booktitle    = {Communications in Computer Science},
 publisher    = {Springer},
 note         = {Forthcoming},
)
@inproceedings(sequent,
 author       = {Arno Ehle and Norbert Hundeshagen and Martin Lange},
 year         = {2018},
 title        = {The Sequent Calculus Trainer with Automated Reasoning - Helping Students to Find Proofs},
 editor       = {Pedro Quaresma and Walther Neuper},
 booktitle    = {{\rm Proceedings 6th International Workshop on} Theorem proving components for Educational software, {\rm Gothenburg, Sweden, 6 Aug 2017}},
 series       = {Electronic Proceedings in Theoretical Computer Science},
 volume       = {267},
 publisher    = {Open Publishing Association},
 pages        = {19--37},
 doi          = {10.4204/EPTCS.267.2},
)
@inproceedings(grabowski,
 author       = {Adam Grabowski},
 year         = {2016},
 title        = {Tarski's geometry modelled in Mizar computerized proof assistant},
 booktitle    = {Computer Science and Information Systems (FedCSIS), 2016 Federated Conference on},
 organization = {IEEE},
 pages        = {373--381},
 doi          = {10.15439/2016F290},
)
@article(isabelleTarski,
 author       = {T. J. M. Makarios},
 year         = {2012},
 title        = {The independence of Tarski's Euclidean axiom},
 journal      = {Archive of Formal Proofs},
 note         = {\url{http://isa-afp.org/entries/Tarskis_Geometry.html}, Formal proof development},
)
@inproceedings(lean,
 author       = {Leonardo de Moura and Soonho Kong and Jeremy Avigad and Van Doorn, Floris and Jakob von Raumer},
 year         = {2015},
 title        = {The Lean theorem prover (system description)},
 booktitle    = {International Conference on Automated Deduction},
 organization = {Springer},
 pages        = {378--388},
 doi          = {10.1007/978-3-319-21401-6\_26},
)
@inproceedings(agda,
 author       = {Ulf Norell},
 year         = {2008},
 title        = {Dependently typed programming in {A}gda},
 booktitle    = {International School on Advanced Functional Programming},
 organization = {Springer},
 pages        = {230--266},
 doi          = {10.1007/978-3-642-04652-0\_5},
)
@book(isabelle,
 author       = {Lawrence C Paulson},
 year         = {1994},
 title        = {Isabelle: A generic theorem prover},
 volume       = {828},
 publisher    = {Springer Science \& Business Media},
 doi          = {10.1007/BFb0030541},
)
@article(vampire,
 author       = {Alexandre Riazanov and Andrei Voronkov},
 year         = {2002},
 title        = {The design and implementation of \textsc{Vampire}},
 journal      = {{AI} Commun.},
 volume       = {15},
 number       = {2, 3},
 pages        = {91--110},
)
@inproceedings(eprover,
 author       = {Stephan Schulz},
 year         = {2013},
 title        = {{System Description: E~1.8}},
 editor       = {Ken McMillan and Aart Middeldorp and Andrei Voronkov},
 booktitle    = {Proc.\ of the 19th LPAR, Stellenbosch},
 series       = {LNCS},
 volume       = {8312},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-45221-5},
)
@book(schwabhauser,
 author       = {Wolfram Schwabh{\"a}user and Wanda Szmielew and Alfred Tarski},
 year         = {1983},
 title        = {Metamathematische metGoogle sagthoden in der geometrie},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-69418-9},
)
@article(tarski,
 author       = {Alfred Tarski and Steven Givant},
 year         = {1999},
 title        = {Tarski's System of Geometry},
 journal      = {Bulletin of Symbolic Logic},
 volume       = {5},
 number       = {2},
 pages        = {175–214},
 doi          = {10.2307/421089},
)
@(coq,
 author       = {{The Coq Development Team}},
 title        = {Coq},
 url          = {https://coq.inria.fr},
)
@inproceedings(mizar,
 author       = {Andrzej Trybulec and Howard A Blair},
 year         = {1985},
 title        = {Computer Assisted Reasoning with MIZAR.},
 booktitle    = {IJCAI},
 volume       = {85},
 pages        = {26--28},
)
@inproceedings(sad,
 author       = {Konstantin Verchinine and Alexander Lyaletski and Andrei Paskevich},
 year         = {2007},
 title        = {\textsc{System for Automated Deduction} (\textsc{SAD}): a tool for proof verification},
 booktitle    = {Proc. CADE-21},
 publisher    = {Springer},
 pages        = {398--403},
 doi          = {10.1007/978-3-540-73595-3_29},
)
@inproceedings(isar,
 author       = {Markus Wenzel},
 year         = {1999},
 title        = {Isar -- a Generic Interpretative Approach to Readable Formal Proof Documents},
 booktitle    = {TPHOLs '99 Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics},
 publisher    = {Springer-Verlag},
 pages        = {167--184},
 doi          = {10.1007/3-540-48256-3\_12},
)