Formale Methoden und Deduktion
Prof. Dr. J. Avenhaus

FB Inf

Praktikum Reduktionssysteme WS 2002/03


Aufgabenstellung

Es soll eine Familie von vervollständiungsbasierten Beweisern für die Gleichungslogik entworfen und implementiert werden.

Besonderes Gewicht wird auf die Implementierung effizienter Match- und Unifikationsroutinen gelegt. Dies wird durch die Verwendung sog. Indizierungsstrukturen erreicht, die Leistungssteigerungen um mehrere Größenordnungen gegenüber naiven Ansätzen erlauben.


Implementierung

Die Implementierung erfolgt in Java; eine Kollektion von Basisklassen, wie z.B. Termen, wird zur Verfügung gestellt.


Voraussetzungen

Vorlesung Reduktionssysteme

Kenntnisse der verwendeten Werkzeuge (z.B. zur Quelltextverwaltung) werden zu Anfang des Praktikums erworben.


Ansprechpartner

Bernd Löchner, 34-408
Tobias Schmidt-Samoa, 34-407


Vorbesprechung:     Donnerstag, 18.07.02, 10:00, 34-420


Impressum AG Formale Methoden und Deduktion Fachbereich Informatik Technische Universität Kaiserslautern Valid HTML 4.01!

Letzte Änderung: Wednesday, 26-Oct-05 08:59:17 GMT
www-aven@informatik.uni-kl.de