Wissensbasierte Methoden zur Beweisunterstützung in Typentheorie

Inhalt der Arbeit ist die Entwicklung und Integration einer wissensbasierten Komponente zur Beweisunterstützung in das Spezifikations- und Verifikationssystem Typelab. Es wird eine Methode entwickelt, die es in einem typentheoretischen Umfeld erlaubt, das manuelle sowie das automatische Führen von Beweisen durch den Einsatz von Methoden aus dem Bereich der terminologischen Wissensrepräsentation zu unterstützen. Dazu wird gezeigt, wie Objekte als Konzepte identifiziert und durch einen Klassifikationsprozeß in Taxonomien bezüglich ihrer Subsumtionsbeziehungen angeordnet werden können. Die so entstandenen terminologischen Komponenten der zu konstruierenden Wissensbasen werden dazu verwendet, Elemente, welche in einer assertionalen Komponente aufgesammelt werden, über Subsumtionskanten von Unterkonzepten zu Elementen ihrer jeweiligen Oberkonzepte zu transportieren, um das aktuelle Beweisziel zu lösen. Zum einen wird mit diesem Ansatz das Abstraktionsniveau von Beweisen durch systematische Wiederverwendung von Beweisen angehoben. Zum anderen kann die Rückwärtssuche des Beweisers durch eine am aktuellen Beweisziel orientierte Vorwärtssuche innerhalb der wissensbasierten Komponente unterstützt werden. Der tatsächliche Nutzen dieses Verfahrens hängt dabei stark von dem Umfang und der Qualität der zur Verfügung stehenden Wissensbasen ab. Deshalb werden Methoden entwickelt, die den Benutzer beim Aufbau von Wissensbasen geeignet unterstützen, sowie den automatischen Aufbau einfacher Wissensbasen erlauben.
 

Online Kopie

Acrobat-Datei (ca 850 KB, benötigt zum Lesen Acrobat von Adobe)
 

BibTeX Eintrag

@MastersThesis{Luther:95a,
  author = 	 "Marko Luther",
  title = 	 "{Wissensbasierte Methoden zur Beweisunterst{\"u}tzung in Typentheorie}", 
  school = 	 "Universit{\"a}t Ulm",
  year = 	 1995
}