Meeting 26.06.14

Meeting 26.06.14

StarExec

Ab demnächst werden die Theorembeweiser Wettbewerbe auf StarExec laufen. Wir müssen uns also langsam auf StarExec einrichten, dass LeoIII darauf läuft.

Problem: Die Intallation von Systemen (Beweisern) auf StarExec ist recht umständlich, da die Syntax recht schlimm ist. Also rechtzeit drauf einrichten.

Website

Bis zum Vortrag (in 3 Wochen) eine kleine LeoIII Website einrichten.

1. Zusamenfassung (Antrag oder aus dem Abstract)
2. Verantwortliche
3. Paper Section
4. Stand(??)

Logo

Drei Köpfiger Löwe??? (Parallelismus (3 Köpfe), Leo (Löwe))

Parser

Wir nehmen Produkt und Summentypen mit auf. Später können wir es durch Typkonstruktoren verallgemeinern.

Externe Beweiser

• Anschließen von TPTP Beweisern (über TPTP Website)
• Geoff fragen, wie wir es benutzen dürften