References

  1. Michael Beeson, Pierre Boutry, Gabriel Braun, Charly Gries & Julien Narboux: GeoCoq. Available at https://hal.inria.fr/hal-01912024.
  2. 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.
  3. 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.
  4. Gabriel Braun & Julien Narboux (2017): A synthetic proof of Pappus' theorem in Tarski's geometry. Journal of Automated Reasoning 58(2), pp. 23, doi:10.1007/s10817-016-9374-4. Available at https://hal.inria.fr/hal-01176508.
  5. 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.
  6. Kevin Buzzard: Xena. Available at https://xenaproject.wordpress.com/.
  7. 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.
  8. Maximilian Doré & Krysia Broda (2018): Intuitive reasoning in formalized mathematics with Elfe. In: Communications in Computer Science. Springer. Forthcoming.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. Lawrence C Paulson (1994): Isabelle: A generic theorem prover 828. Springer Science & Business Media, doi:10.1007/BFb0030541.
  15. Alexandre Riazanov & Andrei Voronkov (2002): The design and implementation of Vampire. AI Commun. 15(2, 3), pp. 91–110.
  16. 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.
  17. Wolfram Schwabhäuser, Wanda Szmielew & Alfred Tarski (1983): Metamathematische metGoogle sagthoden in der geometrie. Springer, doi:10.1007/978-3-642-69418-9.
  18. Alfred Tarski & Steven Givant (1999): Tarski's System of Geometry. Bulletin of Symbolic Logic 5(2), pp. 175–214, doi:10.2307/421089.
  19. The Coq Development Team: Coq. Available at https://coq.inria.fr.
  20. Andrzej Trybulec & Howard A Blair (1985): Computer Assisted Reasoning with MIZAR.. In: IJCAI 85, pp. 26–28.
  21. 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.
  22. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org