Formalizing Hilbert's Grundlagen in Isabelle/Isar

Laura I. Meikle, Jacques D. Fleuriot

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication16th International Conference, TPHOLs 2003, Rome, Italy, September 8-12, 2003. Proceedings
EditorsDavid A. Basin, Burkhart Wolff
PublisherSpringer Berlin Heidelberg
Number of pages16
ISBN (Electronic)978-3-540-45130-3
ISBN (Print)978-3-540-40664-8
Publication statusPublished - 2003

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)2758

Cite this