Entwicklung und Implementierung eines Beweisers für konstruktive Logik

Inhalt der vorliegenden Arbeit ist die Entwicklung und Implementierung der Beweiskomponente des Systems Typelab, das auf der Typtheorie des Extended Calculus of Constructions (ECC) basiert und in der Abteilung für Künstliche Intelligenz der Universität Ulm entwickelt wurde. Hierzu ist als Inferenzmechanismus der in ECC eingebetteten intuitionistischen Logik höherer Ordnung ein Regelsystem im Stile von herkömmlichen Sequenzenkalkülen vorgeschlagen worden. Durch die so gewonnene Einbettung eines intuitionistischen Sequenzenkalküls in die Typtheorie ECC ist mit Hilfe der Beweiskomponente des Typelab-Systems eine gerichtete, suggestive Beweissuche möglich, die im Vergleich zu bestehenden Systemen einen hohen Automatisierungsgrad erlaubt. Der Anwendungsschwerpunkt des Beweisers liegt in der interaktiven, expliziten Konstruktion von Beweisen durch einen Benutzer. Innerhalb der Beweissuche steht die Benutzerführung, sowie die Entlastung des Benutzers um triviale Beweisentscheidungen im Vordergrund. Zudem bietet die im Rahmen dieser Arbeit realisierte Beweiskomponente die Möglichkeit der Definition von komplexen Beweiskommandos und Suchprozeduren unter der Verwendung von Taktiken.

Die als theoretische Grundlage des Systems Typelab gewählte Typtheorie ECC bietet einen adäquaten Ansatz des formalen Software Engineerings: Durch die Integration einer formalen funktionalen Programmiersprache, dem Lambda-Kalkül, und einer intuitionistischen Logik höherer Ordnung bietet der Kalkül ECC die Voraussetzungen für den Einsatz als Spezifikationssprache innerhalb des formalen Softwareentwurfs. Eine formale Spezifikation ermöglicht die exakte Formulierung der Anforderungen an die Funktionalität eines Programmes und die Festlegung seiner wünschenswerten Eigenschaften. In diesem Sinn ist ein Programm korrekt, wenn es den Anforderungen seiner Spezifikation genügt. Die Lösung von Beweisverpflichtungen im Zuge des Programmentwurf mit Typelab ist die Aufgabe der realisierten Beweiskomponente.
 

Online Kopie

Postscipt-Datei (ca 660 KB)
 

BibTeX Eintrag

@MastersThesis{Wagner:95a,
  author = 	 "Matthias Wagner",
  title = 	 "{Entwicklung und Implementierung eines Beweisers f{\"u}r
		  konstruktive Logik}", 
  school = 	 "Universit{\"a}t Ulm",
  year = 	 1995
}