Benutzer: Gast  Login
Originaltitel:
Isabelle/Isar --- a versatile environment for human-readable formal proof documents 
Übersetzter Titel:
Isabelle/Isar --- eine vielseitige Umgebung für visuell lesbare, formale Beweis-Dokumente 
Jahr:
2002 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof. Ph.D.) 
Gutachter:
Schwichtenberg, Helmut (Prof. Dr.) 
Format:
Text 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Stichworte:
mechanized theorem proving; readable formal proofs; high-level languages; document preparation 
Schlagworte (SWD):
Automatisches Beweisverfahren 
TU-Systematik:
DAT 706d 
Kurzfassung:
The basic motivation of this work is to make formal theory developments with machine-checked proofs accessible to a broader audience. Our particular approach is centered around the Isar formal proof language that is intended to support adequate composition of proof documents that are suitable for human consumption. Such primary proofs written in Isar may be both checked by the machine and read by human-beings; final presentation merely involves trivial pretty printing of the sources. Sound logi...    »
 
Übersetzte Kurzfassung:
[Abstract nur auf Englisch verfügbar.] The basic motivation of this work is to make formal theory developments with machine-checked proofs accessible to a broader audience. Our particular approach is centered around the Isar formal proof language that is intended to support adequate composition of proof documents that are suitable for human consumption. Such primary proofs written in Isar may be both checked by the machine and read by human-beings; final presentation merely involves trivial pre...    »
 
Veröffentlichung:
Universitätsbibliothek der TU München 
Mündliche Prüfung:
01.02.2002 
Dateigröße:
1911817 bytes 
Seiten:
331 
Letzte Änderung:
04.07.2007