Jede Gruppe soll schlieaus den bisher entstandenen Teilen ein
komplettes Beweissystem bauen. Dieses soll ein Programm werden, danach Start, den Benutzer nach dem Textfile fragt, in dem eine
aussagenlogische Formel steht, diesen dann einlädt und schliefragt mit welchem Beweiser diese Formel bewiesen werden soll und unter
welchem File das Ergebnis abzuspeichern ist. Da Gofer ungleich
Haskell kein Modulkonzept zur Verfügung stellt, wird das Zusammenfassen
der einzelnen Programmteile ein wenig Handarbeit bedeuten. Es kann
passieren (auch wenn die Wahrscheinlichkeit eher gering ist), daFunktionen mit gleichen Namen global in verschiedenen Programmteilen
definiert wurden. Noch etwas gefährlicher ist es, wenn verschiedene
Gruppe gleiche Datentypen in unterschiedlicher Weise zu Instanzen
bestimmter Typklassen definiert haben.
Die eigentliche Programmierarbeit in dieser Aufgabe besteht aus
I/O-Operationen, einmal im Lesen und Schreiben von Dateien, zum anderen
im Dialog mit dem Benutzer. I/O ist in rein funktionalen Sprachen ein
sehr heikles Thema. Kaum eine Woche vergeht, wo auf dem Newsboard
comp.lang.functional nicht ein Hilferuf diesbezüglich zu finden ist. Da
wir dieses Thema in unserer Vorlesung ausgespart haben, sei hier eine
kurze Übersicht darüber angegeben: