Meeting 13.09.2016

Wer macht was

Bereits fertige Arbeiten

Maximilian Claus: Modelchecking als Higher Order Problem darstellen

Kim Kern: Methoden zur Klausifizierung. Daraus entstand auch ein IJCAR'16 Paper.

Samuel Gfröer: TPTP Parser

Derzeit laufende Arbeiten

Marco Ziener: Proof Guidance mit Machine Learning.

Irina Makarenko: Einbettung von Freier Logik in HOL

Tobias Gleißner: Einbettung von Modallogik in HOL

Adrian Milovanovic: Beweisminimierung und Answer Variables

Alexander Steen:

• Refactoring von Unifikation und TH1 Unifikation
  • Generelles Reasoning für TH1
• Allgemeines Aufräumen:
  • Position Indexing
• Primitive Substitution
• Flexiblere Clause Selection
• Choice als Kalkülregel
• Übersetzung nach FO

Hans-Jörg Schurr: Pure Literal Erkennung ist implementiert. Derzeit Arbeit an SAT basierender Constant-Literal Erkennung. Deshalb wurden Bindings für PicoSAT geschrieben. Dann: Blocked Clause Elimination, Variable Dependency Schemas.

Max Wisniewski:

• Sequentielle Schleife in parallele Tasks zerlegen
• Agentifiziertes Kalkül
• Abhängigkeiten zwischen Agenten
• Load Balancing
• GUI zum graphischen Debuggen
• Datenstrukturen im Blackboard

Themen

In welchem Verhältnis stehen die Einbettungen zu LEO-III

Die Einbettungen stehen in keinem direkten Verhältnis zu LEO-III, sondern werden vorher generiert. Später ist ein Online Tool angedacht, welches LEO-III automatisch aufrufen wird.

Preprocessing API

Preprocessing passt gut in das vorhandene System mit Control Objekt. Deshalb wird erst mal des verwendet. Minscoping ist wahrscheinlich schlecht implementiert.

TODO

• Problemsammlung zum Benchmarken
• Normalisierung