User: Guest  Login
Original title:
Automating Recursive Definitions and Termination Proofs in Higher-Order Logic 
Translated title:
Automatisierung von Funktionsdefinitionen und Terminierungsbeweisen in höherstufiger Logik 
Year:
2009 
Document type:
Dissertation 
Institution:
Fakultät für Informatik 
Advisor:
Nipkow, Tobias (Prof., Ph.D.) 
Referee:
Nipkow, Tobias (Prof., Ph.D.); Paulson, Lawrence C. (Prof., Ph.D.) 
Language:
en 
Subject group:
DAT Datenverarbeitung, Informatik 
Abstract:
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...    »
 
Translated abstract:
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...    »
 
Oral examination:
22.07.2009 
Pages:
141 
Last change:
25.08.2009