User: Guest  Login
Original title:
Isabelle/Isar --- a versatile environment for human-readable formal proof documents 
Translated title:
Isabelle/Isar --- eine vielseitige Umgebung für visuell lesbare, formale Beweis-Dokumente 
Year:
2002 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof. Ph.D.) 
Referee:
Schwichtenberg, Helmut (Prof. Dr.) 
Format:
Text 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Keywords:
mechanized theorem proving; readable formal proofs; high-level languages; document preparation 
Controlled terms:
Automatisches Beweisverfahren 
TUM classification:
DAT 706d 
Abstract:
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...    »
 
Translated abstract:
[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...    »
 
Publication :
Universitätsbibliothek der TU München 
Oral examination:
01.02.2002 
File size:
1911817 bytes 
Pages:
331 
Last change:
04.07.2007