Formale Methoden und Deduktion Prof. Dr. J. Avenhaus

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