6 papers
Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents
Tim S. Lyon, Lukas Zenger
We introduce the formalism of non-wellfounded and cyclic linear nested sequent calculi, developing concrete systems for linear temporal logic (LTL). The paper addresses two central…
Proof Theory for Non-Contingency Logic
Yunsong Wang, Lukas Zenger
{Non-contingency logic $(\KWL)$ replaces the usual necessity operator of modal logic with an operator expressing that a proposition is necessarily true or necessarily false. Beside…
Intuitionistic Dynamic Logic
Lukas Zenger
This thesis develops the mathematical theory of intuitionistic dynamic logics - extensions of intuitionistic propositional logic with modalities and fixed point operators. Such sys…
Non-Wellfounded and Cyclic Proofs for LTL: A Syntactic Correspondence with Linear Nested Sequents
Tim S. Lyon, Lukas Zenger
We introduce the formalism of non-wellfounded and cyclic linear nested sequent calculi, developing concrete systems for linear temporal logic (LTL). The paper addresses two central…
Intuitionistic Common Knowledge
Lukas Zenger
We study an intuitionistic version of common knowledge logic (CK), called ICK, which was introduced by Jäger and Marti. ICK extends intuitionistic propositional logic (IPL) by mult…
Coalgebraic proof translations for non-wellfounded proofs
Borja Sierra Miranda, Thomas Studer, Lukas Zenger
Non-wellfounded proof theory results from allowing proofs of infinite height in proof theory. To guarantee that there is no vicious infinite reasoning, it is usual to add a constra…