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