Please use this identifier to cite or link to this item: doi:10.22028/D291-25680
Title: Equality and extensionality in automated higher-order theorem proving
Author(s): Benzmueller, Christoph
Language: English
Year of Publication: 1999
SWD key words: Logik ; Stufe n ; Automatisches Beweisverfahren ; Typentheorie ; Lambda-Kalkül
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
Abstract: This thesis focuses on equality and extensionality in automated higher-order theorem proving based on Church's simply typed lambda - calculus (classical type theory). First, a landscape of various semantical notions is preented that is motivated by the different roles equality adopts in them. Each of the semantical notions in this landscape - including Henkin semantics - is then linked with an abstract consistency principle that can be employed for analysing the connection between syntax and semantics of higer-order calculi. Apart from this proof theoretic tools, the main contributions of this are the three new calculi ER (extensional higher-order resolution), EP (extensoinal higher-order paramodulation) and ERUE (extensonal higher-order RUE-resolution) which improve the mechanisation of defined and primitvie equality in classical type theory. In contrast to the refutation approaches for classical type theory developed so far, these calculi reach Henkin completeness without requiring additional extensionality axioms. The key idea is to allow for recursive calls from higer-order unification to the overall refutation search. Calculus ER, which in contrast to EP and ERUE, considers equality only as a defined notion, has been implemented in the theorem prover LEO and the suitability of this approach for proving simple theorems about sets has been demonstrated in a case study.
Diese Arbeit untersucht Gleichheit und Extensionalitaet im automatischen Beweisen in Logik hoeherer Stufe. Die betrachtete Sprache ist die klassische Typtheorie, d.h. eine Logik hoeherer Stufe basierend auf Churchs einfach getypten Lambda-Kalkül. Zunächst werden unterschiedlich starke Semantikbegriffe für die klassische Typtheorie erarbeitet, die durch die jeweils unterschiedlichen Rollen, die die Gleichheit in ihnen einnimmt, motiviert sind. Jedem der eingeführten Semantikbegriffe wird dann eine Menge abstrakter Konsistenzeigenschaften zugeordnet mit dem Ziel, die Analyse der Verbindung zwischen Syntax und Semantik von Beweiskalkülen für die klassische Typtheorie zu erleichtern.
Link to this record: urn:nbn:de:bsz:291-scidok-1657
Advisor: Jörg H. Siekmann
Date of oral examination: 1-Jan-1999
Date of registration: 12-Feb-2004
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
ChristophBenzmueller_ProfDrJoergHSiekmann.pdf2,53 MBAdobe PDFView/Open

Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.