Integration von Gleichheitsverfahren in einen typentheoretischen Beweiser

Inhalt der vorliegenden Arbeit ist die Konzeption und Implementierung von Verfahren zur Durchführung von Gleichheitsbeweisen in das Spezifikations- und Verifikationssystem Typelab, das in der Abteilung für Künstliche Intelligenz der Universität Ulm entwickelt wurde. Dieses System basiert auf der Typentheorie des Extended Calculus of Constructions (ECC) und beinhaltet unter anderem eine Beweiskomponente zur Durchfürung logischer Beweise. In dieser Diplomarbeit wird in der "logischen" Beweiskomponente des Typelab-Systems eine weitere Komponente integriert, mit Hilfe deren Gleichheitsbeweise durchgeführt 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ändigungsprozedur als Basiskalkül und die Teamwork-Methode als Verteilungskonzept verwendet.

Diplomarbeit. Universität Ulm 1996.

Titelseite (gzipped postscript) und Arbeit (gzipped postscript)

BibTeX Entry

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