Ill-Founded Linear Nested Sequents for LTL

Available as topic for a Master's thesis

Supervisor Tim Lyon
Computational Logic
Start
Download

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.

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.

Please click the download link to the left for a PDF document that details the goals and expectations of the project.