Thema3515: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Keine Bearbeitungszusammenfassung |
Keine Bearbeitungszusammenfassung |
||
| Zeile 18: | Zeile 18: | ||
This project aims to introduce an alternative LTL proof system based on linear nested sequents (LNS), a structured sequent framework that maintains desirable properties like rule invertibility and syntactic cut-elimination. Specifically, it seeks to develop an ill-founded (and potentially cyclic) LNS system, where proofs are finitely branching, ill-founded trees. This would be the first proof system combining LNS with ill-founded proofs, making it of significant theoretical interest to proof theorists and logicians. | This project aims to introduce an alternative LTL proof system based on linear nested sequents (LNS), a structured sequent framework that maintains desirable properties like rule invertibility and syntactic cut-elimination. Specifically, it seeks to develop an ill-founded (and potentially cyclic) LNS system, where proofs are finitely branching, ill-founded trees. This would be the first proof system combining LNS with ill-founded proofs, making it of significant theoretical interest to proof theorists and logicians. | ||
<br> | <br> | ||
Please click the download link to the left for a PDF document that details the goals and expectations of the project. | Please click the download link to the left for a PDF document that details the goals and expectations of the project. | ||
}} | }} | ||
Version vom 28. März 2025, 14:10 Uhr
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.
Bitte klicken Sie auf den Download-Link auf der linken Seite, um ein PDF-Dokument zu erhalten, in dem die Ziele und Erwartungen des Projekts beschrieben sind.
