Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25680
Titel: Equality and extensionality in automated higher-order theorem proving
Verfasser: Benzmueller, Christoph
Sprache: Englisch
Erscheinungsjahr: 1999
SWD-Schlagwörter: Logik ; Stufe n ; Automatisches Beweisverfahren ; Typentheorie ; Lambda-Kalkül
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: 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 zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-1657
hdl:20.500.11880/25736
http://dx.doi.org/10.22028/D291-25680
Erstgutachter: Jörg H. Siekmann
Tag der mündlichen Prüfung: 1-Jan-1999
SciDok-Publikation: 12-Feb-2004
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
ChristophBenzmueller_ProfDrJoergHSiekmann.pdf2,53 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.