When a course instance has been created from a template, the course instance will be in this state
Es soll ein WYSIWYG-Editor (What-you-see-is-what-you-get-Editor) für das maschinenlesbare Format TPTP THF entwickelt werden. Dieses wird zum Repräsentieren und Formalisieren von logischen Aussagen und Problemen in klassischer Prädikatenlogik höherer Stufe genutzt. Der Editor soll ein in THF formuliertes logisches Problem menschenlesbar und -editierbar machen sowie übersichtlich aufbereiten. Die Kernkomponenten sind hierbei:
Je nach Interesse und Anzahl der Teilnehmer wird zusätzlich eine Auswahl der folgenden features implementiert:
Neben der Editierkomponente soll die Software auch eine Anbindung an gängige TPTP-konforme Theorembeweiser (lokal und remote) schaffen. Theorembeweiser sind Softwaresysteme, die logische Aussagen und Probleme lösen können. Mögliche Features könnten folgende sein:
The projects goal is to develop a WYSIWYG editor (what-you-see-is-what-you-get-editor) for the machine readable format TPTP THF. This format is used to represent and formalize logical statements and problems in classical higher-order logic. The editor should be capable of creating a human-readable and editable representation of a logical problem formulated in THF. Core features:
Dependent on the number of participants and their interests a selection of the following features will be implemented:
Besides the editor part of the software should be able to (locally and remotely) interface TPTP compliant theorem provers. Theorem provers are software systems which can analyze, process or solve logical problems. The set of features may include: