Formalizing Hilbert’s Grundlagen in Isabelle/Isar

DOI10.1007/10930755_21zbMath1279.68291OpenAlexW1606604604WikidataQ56432564 ScholiaQ56432564MaRDI QIDQ3559773

Laura I. Meikle, Jacques D. Fleuriot

Publication date: 7 May 2010

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/10930755_21

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

From informal to formal proofs in Euclidean geometry, Implementing Euclid's straightedge and compass constructions in type theory, Two cryptomorphic formalizations of projective incidence geometry, Formalization of the arithmetization of Euclidean plane geometry and applications, What is a proof?, A proof-centric approach to mathematical assistants, Bridging the Gap Between Argumentation Theory and the Philosophy of Mathematics, The area method. A recapitulation, A review and prospect of readable machine proofs for geometry theorems, A case study in formalizing projective geometry in Coq: Desargues theorem, A graphical user interface for formal proofs in geometry, Bridging the gap between argumentation theory and the philosophy of mathematics, Formalization of the Poincaré disc model of hyperbolic geometry, Mechanical Theorem Proving in Tarski’s Geometry, Diagrams in mathematics, An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time, A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs, Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL, Formalizing complex plane geometry, Automated generation of machine verifiable and readable proofs: a case study of Tarski's geometry

Uses Software

• Isabelle