Studium

193
Teilnahmepflicht

Wenn eine Veranstaltungsinstanz aus einer Schablone erstellt wird, befindet sie sich in diesem Zustand.

  • Die Daten sind in der Regel noch nicht vollständig und es kann noch alles bearbeitet werden.
  • Dozenten und Sekretariate können den Zuständ auf Bearbeitet setzen.

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:

  • Öffnen und Speichern von THF-Dateien sowie die Darstellung und Editiermöglichkeit in konventioneller Logikschreibweise ähnlich der des interaktiven Theorembeweisers Isabelle;
  • übersichtliche Darstellung eines Problems durch ein Inhaltsverzeichnis der Axiome/Theoreme, eventuell "Ein-" und "Ausklappen" von Axiomen im Problem,
  • Filebrowser.

Je nach Interesse und Anzahl der Teilnehmer wird zusätzlich eine Auswahl der folgenden features implementiert:

  • Syntax highlighting;
  • syntax error notification;
  • semantical error notifications z.B. type errors;
  • auto completion von Bezeichnern/Typen;
  • code generation z.B. für bereits benutzte aber undefinierte Konstantensymbole;
  • Bezeichner-Following bei Shift-Klick;
  • Auto linebreaking/-spacing für große Formeln
  • gleichzeitiges Editieren der WYSIWYG-Darstellung  und THF;
  • Interface zum Bearbeiten/Einstellen der Semantik von nicht-klassischen Logiken in THF;
  • Darstellung von Formeln als Graph;
  • Volltextsuche.

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:

  • Aufbereitung der Rückgabewerte der Beweiser;
  • Ein- und Ausblenden einzelner Axiome/Theoreme für den Beweiser;
  • automatisches Testen auf Redundanzen von Axiomen;
  • automatisches Testen auf unbenötigte Axiome;
  • automatisches Testen auf widersprüchliche Axiome;
  • Anbindung an zusätzliche tools z.B. zur Formatierung, Umwandlung in andere Formate, semantischen Einbettung eines Problems usw., evtl. Möglichkeit zur Erstellung einer Toolchain;
  • Testframework.

 

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.

Sprachübergreifend

Werdende Mütter

Keine Gefährdungen vorliegend
Teilweise Gefährdungen vorliegend
Alternative Lehrveranstaltung
Gefährdungen vorliegend
Mutterschutzbogen anzeigen

Stillende Mütter

Keine Gefährdungen vorliegend
Teilweise Gefährdungen vorliegend
Alternative Lehrveranstaltung
Gefährdungen vorliegend
Mutterschutzbogen anzeigen