Benutzer: Gast  Login
Originaltitel:
Proofs, Programs and Executable Specifications in Higher Order Logic 
Übersetzter Titel:
Beweise, Programme und ausführbare Spezifikationen in höherstufiger Logik 
Jahr:
2003 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof. Ph.D.) 
Gutachter:
Nipkow, Tobias (Prof. Ph.D.); Schwichtenberg, Helmut (Prof. Dr.) 
Format:
Text 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
proof terms; Curry-Howard isomorphism; constructive logic; program extraction; executable specifications 
Übersetzte Stichworte:
Beweisterme; Curry-Howard Isomorphismus; konstruktive Logik; Programmextraktion; ausführbare Spezifikationen 
Schlagworte (SWD):
Logische Programmierung; Softwarespezifikation; Automatisches Beweisverfahren; Konstruktive Logik 
TU-Systematik:
DAT 540d; DAT 706d 
Kurzfassung:
This thesis presents several extensions to the generic theorem prover Isabelle, a logical framework based on higher order logic. The central contribution of this thesis is the extension of Isabelle with a calculus of primitive proof terms, in which proofs are represented using lambda-terms in the spirit of the Curry-Howard isomorphism. Primitive proof terms allow for an independent verification of proofs constructed in Isabelle by a small and reliable proof checker, and are an important prerequi...    »
 
Übersetzte Kurzfassung:
Diese Arbeit präsentiert mehrere Erweiterungen des generischen Theorembeweisers Isabelle. Der zentrale Beitrag der Arbeit ist die Erweiterung von Isabelle um einen Kalkül für primitive Beweisterme, in dem Beweise als Lambda-Terme repräsentiert werden. Primitive Beweisterme erlauben eine unabhängige Verifikation von in Isabelle konstruierten Beweisen durch einen kleinen und vertrauenswürdigen Beweisprüfer und bilden eine wichtige Voraussetzung für den Austausch von Beweisen mit anderen Systemen....    »
 
Veröffentlichung:
Universitätsbibliothek der TU München 
Mündliche Prüfung:
20.10.2003 
Dateigröße:
1208305 bytes 
Seiten:
175 
Letzte Änderung:
04.07.2007