Thema3515: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Keine Bearbeitungszusammenfassung |
Keine Bearbeitungszusammenfassung Markierung: Manuelle Zurücksetzung |
||
| Zeile 10: | Zeile 10: | ||
<br> | <br> | ||
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. | 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. | ||
|Beschreibung EN=Linear temporal logic (LTL) is a modal logic used for reasoning about temporal properties in computing, particularly in program verification and model checking. Existing sequent-style proof systems for LTL, such as infinitary labeled calculi and cyclic Gentzen systems, have certain limitations, including complex sequents and non-invertible rules. | |Beschreibung EN=Linear temporal logic (LTL) is a modal logic used for reasoning about temporal properties in computing, particularly in program verification and model checking. Existing sequent-style proof systems for LTL, such as infinitary labeled calculi and cyclic Gentzen systems, have certain limitations, including complex sequents and non-invertible rules. | ||
<br> | <br> | ||
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. | ||
}} | }} | ||
Version vom 28. März 2025, 14:08 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.
