This paper describes part of the formalization of Hilbert's Grundlagen der Geometrie in the higher order logic of Isabelle/Isar, an extension of the interactive theorem prover Isabelle. Many mechanized proofs and formalization issues are discussed and the work is compared against Hilbert's prose and also other research in the field. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Meikle, L. I., & Fleuriot, J. D. (2003). Formalizing Hilbert’s Grundlagen in Isabelle/Isar. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2758, 319–334. https://doi.org/10.1007/10930755_21
Mendeley helps you to discover research relevant for your work.