Integration von Gleichheitsbeweisverfahren in einen typentheoretischen Beweiser

Inhalt der vorliegenden Arbeit ist die Konzeption und Implementierung von Verfahren zur Durchfüuhrung von Gleichheitsbeweisen in das Spezifikations- und Verifikationssystem Typelab, das in der Abteilung für Künstliche Intelligenz der Universitüat Ulm entwickelt wurde. Dieses System basiert auf der Typentheorie des Extended Calculus of Constructions (ECC) und beinhaltet unter anderem eine Beweiskomponente zur Durchfüurung logischer Beweise. In dieser Diplomarbeit wird in der "logischen" Beweiskomponente des Typelab-Systems eine weitere Komponente integriert, mit Hilfe deren Gleichheitsbeweise durchgefüuhrt werden können. Dabei wird zur Beweissuche nicht Typelab selbst, sondern der Theorembeweiser Discount eingesetzt. Discount ist ein verteilter Theorembeweiser für Gleichheitsprobleme, der die Knuth-Bendix Vervollstäandigungsprozedur als Basiskalkül und die Teamwork-Methode als Verteilungskonzept verwendet.

Titelseite (ca. KB) und Arbeit als komprimierte (Gzip) Postscript Datei (ca. 850 KB)
 

BibTeX Eintrag

@MastersThesis{Sorea:96,
  author = 	 {Sorea, Maria},
  title = 	 {Integration von Gleichheitsbeweisverfahren in einen
typentheoretischen Beweiser}, 
  school = 	 {Universit{\"a}t Ulm},
  year = 	 1996
}