Anzeige
Erschienen in:
2013 | OriginalPaper | Buchkapitel
From Tarski to Hilbert
verfasst von : Gabriel Braun, Julien Narboux
Erschienen in: Automated Deduction in Geometry
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In this paper, we report on the formal proof that Hilbert’s axiom system can be derived from Tarski’s system. For this purpose we mechanized the proofs of the first twelve chapters of Schwabäuser, Szmielew and Tarski’s book:
Metamathematische Methoden in der Geometrie
. The proofs are checked formally within classical logic using the Coq proof assistant. The goal of this development is to provide clear foundations for other formalizations of geometry and implementations of decision procedures.