direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

Habilitationen 2006

Lehrprobe

Theoriebildung und Beweisautomatisierung in der Stufenlogik
Dr.-Ing. Thomas Santen, Berlin
Freitag, den 1. Dezember, um 13.00 Uhr, Raum FR 5516

Die Stufenlogik, die auch als Logik höherer Ordnung (HOL) bezeichnet wird, basiert auf dem typisierten Lambda-Kalkül. Nur wenige Axiome sind notwendig, um eine Logik zu erhalten, in der sich sehr viele mathematische Theorien repräsentieren lassen. Da der typisierte Lamda-Kalkül auch die semantische Basis funktionaler Programmiersprachen ist, ist es nicht verwunderlich, dass sich die Stufenlogik gut mit Beweiswerkzeugen unterstützen lässt.

Die Vorlesung führt zunächst die Syntax und Semantik der Stufenlogik ein, um dann darauf einzugehen, wie sich mittels definitorischer Erweiterungen komplexe Theorien in der Logik repräsentieren lassen. Verschiedene Ansätze zur Einbettung von Formalismen in die Logik werden diskutiert. Schließlich werden die Grundmechanismen zum Führen maschinengestützter Beweise in der Logik vorgestellt.

Zusatzinformationen / Extras

Direktzugang

Schnellnavigation zur Seite über Nummerneingabe

Diese Seite verwendet Matomo für anonymisierte Webanalysen. Mehr Informationen und Opt-Out-Möglichkeiten unter Datenschutz.