Das Beweisassistenzsystem OMEGA

Software-Entwickler in der Theoriebildung und insbesondere bei der
Beweisführung zu unterstützen. Eine formale Logik (sie legt die Syntax
und Semantik der Formelsprache fest) und ein Beweiskalkül (er
definiert syntaktische Konstruktionsvorschriften für Beweise) bilden
den Kern eines jeden Beweisassistenzsystems. Darüber hinaus
beinhaltet ein Beweisassistenzsystem eine Vielzahl weiterer
Komponenten, beispielsweise zur Automatisierung der Beweissuche oder
zur Verwaltung strukturierter Theorien. Wichtig sind auch geeignete
Schnittstellen zum Benutzer zur Formalisierung von Theorien, zur
interaktiven bzw. automatisch unterstützten Beweisführung, oder auch
zur Präsentation eines Beweises in einer benutzerfreundlichen
Darstellung, zum Beispiel als natürlichsprachlichen Text. Vor
Verwendung eines Beweisassistenzsystems ist ein Benutzer in der Regel
gezwungen, sich zunächst die formallogische Syntax für Formeln und das
Jargon zur Steuerung der interaktiven und automatischen Beweissuche
des Beweisassistenzsystems anzueignen.

Dieser Vortrag gibt einen Überblick des Beweisassistenzsystems OMEGA
und insbesondere die darin enthaltenen Techniken und Werkzeuge zur
Theorieverwaltung und Beweiskonstruktion. Aufbauend darauf beschreiben
wir die Integration von OMEGA in den Texteditor Texmacs. Ziel dieser
Forschung ist es Autoren von mathematischen Texten die Unterstützung
des Beweisassistenzsystems in einer gewohnten Umgebung anzubieten und
den zu erlernenden Anteil an formallogischen Formalismen und Jargons
zu reduzieren. Der Vortrag schließt mit Vorführung des integrierten
Systems.