19317212

WiSe 17/18: Projektseminar: KI-gestützte Pflege einer internationalen Schuldatenbank

Christoph Benzmüller

Comments

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:

opening/closing of THF files and representation of the contents in conventional logic notation similar to the interactive theorem prover Isabelle;
preparation of a problem: Table of contents of the axioms/theorems, folding/expanding axioms;
file browser.

Dependent on the number of participants and their interests a selection of the following features will be implemented:

syntax highlighting;
syntax error notifications;
semantical error notifications e.g. type errors;
auto completion (e.g. for types and identifiers);
code generation (e.g. for used but undefined constants);
identifier following on shift click
auto linebreaking and line spacing for large formulas;
simultaneous editing of the WYSIWYG representation and THF;
graphical interface for editing semantics of non-classical logics;
graph representation of formulas;
full-text search.

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:

preparing the provers return values;
switching on/off of logical statements;
automatic redundancy test on axiom sets;
automatic check for superfluous axioms;
automatic check for contradictory axioms;
integration of additional tools for formatting, format conversion, semantic embedding of non-classical logics,...toolchain creation;
testing framework.