Benutzer: Gast  Login
Originaltitel:
Automating Recursive Definitions and Termination Proofs in Higher-Order Logic 
Übersetzter Titel:
Automatisierung von Funktionsdefinitionen und Terminierungsbeweisen in höherstufiger Logik 
Jahr:
2009 
Dokumenttyp:
Dissertation 
Institution:
Fakultät für Informatik 
Betreuer:
Nipkow, Tobias (Prof., Ph.D.) 
Gutachter:
Nipkow, Tobias (Prof., Ph.D.); Paulson, Lawrence C. (Prof., Ph.D.) 
Sprache:
en 
Fachgebiet:
DAT Datenverarbeitung, Informatik 
Kurzfassung:
The aim of this thesis is to provide an infrastructure for general recursive function definitions in a proof assistant based on higher-order logic (HOL) that has no native support for recursion or pattern matching. In the first part we develop a tool that automates recursive function definitions and provides appropriate proof rules for them. Compared to previous work, our package supports the definition of partial functions, modeling the domain of the function by an inductive domain pred...    »
 
Übersetzte Kurzfassung:
Ziel dieser Arbeit ist die Entwicklung einer Infrastruktur für rekursive Funktionsdefinitionen in einem interaktiven Theorembeweiser, in dem Rekursion und Pattern-Matching nicht von Haus aus unterstützt werden. Wir arbeiten im Kontext höherstufiger Logik (higher-order logic, HOL). Im ersten Teil entwickeln wir ein Werkzeug, welches Funktionsdefinitionen automatisiert und geeignete Beweisregeln dafür bereitstellt. Im Gegensatz zu existierenden Ansätzen unterstützt unser Verfahren auch partiel...    »
 
Mündliche Prüfung:
22.07.2009 
Seiten:
141 
Letzte Änderung:
25.08.2009