Formale Methoden und Deduktion
Prof. Dr. J. Avenhaus

Praktikum Reduktionssysteme WS 2003/04

Aufgabenstellung

Aufbauend auf einer sehr komfortablen Plattform soll ein Gleichheitsbeweiser entwickelt werden. Hauptziel ist es, die Komponente zu verbessern, die im praktischen Einsatz den größten Anteil an der Rechenzeit hat: In einem vervollständigungsbasierten Beweiser - wie etwa WALDMEISTER - wird erfahrungsgemäß 80-99% der gesamten Rechenzeit für die Simplifizierung der neuen kritischen Paare benötigt. Ein Grund dafür ist, dass manche Terme mehrfach simplifiziert werden. Dies soll durch geeignete Datenstrukturen und darauf arbeitende Algorithmen vermieden werden.

Implementierung

Die Implementierung erfolgt in Java.

Voraussetzungen

Vorlesung Reduktionssysteme

Ansprechpartner

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

Impressum

AG Formale Methoden und Deduktion

Fachbereich Informatik

Technische Universität Kaiserslautern