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: | Dissertation |
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 hdl:20.500.11880/25736 http://dx.doi.org/10.22028/D291-25680 |
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 | Size | Format | |
---|---|---|---|---|
ChristophBenzmueller_ProfDrJoergHSiekmann.pdf | 2,53 MB | Adobe PDF | View/Open |
Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.