Ill-Founded Linear Nested Sequents for LTL

Studienarbeiten

• Themenvorschläge für Studien- und Abschlussarbeiten
• Abgeschlossene Arbeiten
  • Algebra und Diskrete Strukturen
  • Algebraische und logische Grundlagen der Informatik
  • Automatentheorie
  • Computational Logic
  • Knowledge-aware Artificial Intelligence
  • Logische Programmierung und Argumentation
  • Wissensbasierte Systeme
• Laufende Studienarbeiten

Toggle side column

Ill-Founded Linear Nested Sequents for LTL

Verfügbar als Thema einer Masterarbeit

•   Betreuer Tim Lyon
•   Computational Logic
•   Beginn
•   Download

Die lineare temporale Logik (LTL) ist eine modale Logik zur Untersuchung temporaler Eigenschaften in der Informatik, insbesondere in der Programmanalyse und Modellprüfung. Bestehende beweistheoretische Systeme für LTL, wie infinitär markierte Kalküle und zyklische Gentzen-Systeme, haben bestimmte Einschränkungen. Dazu gehören komplexe Sequenzen und nicht-invertierbare Regeln.

Dieses Projekt soll ein alternatives Beweissystem für LTL auf Basis linearer verschachtelter Sequenzen (LNS) einführen. LNS ist ein strukturiertes Sequenzsystem mit vorteilhaften Eigenschaften wie regelbasierter Invertierbarkeit und syntaktischer Schnittelimination. Ziel ist die Entwicklung eines grundlagenlosen (und möglicherweise zyklischen) LNS-Systems, bei dem Beweise endlich verzweigte, grundlagenlose Bäume sind. Dies wäre das erste Beweissystem, das LNS mit grundlagenlosen Beweisen kombiniert und ist daher von großem theoretischem Interesse für Beweistheoretiker und Logiker.