Loop-free verification of termination of derivation for a fragment of dynamic logic

zbMATH Open1344.03034MaRDI QIDQ2811594FDOQ2811594

Authors: R. Pliuškevičius 

Publication date: 10 June 2016

Published in: Lietuvos Matematikos Rinkinys. Lietuvos Matematiku Draugijos Darbai (Search for Journal in Brave)

Recommendations

• Termination of derivations in a fragment of transitive distributed knowledge logic
• A contraction-free and cut-free sequent calculus for propositional dynamic logic
• scientific article; zbMATH DE number 4008371
• Sequential dynamic logic
• A non-wellfounded, labelled proof system for propositional dynamic logic

zbMATH Keywords

propositional dynamic logicsequent calculusloop-checkinvertible rule

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Structure of proofs (03F07)

Cited In (3)

• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• Termination of derivations in a fragment of transitive distributed knowledge logic
• Deductive verification in decidable fragments with Ivy

This page was built for publication: Loop-free verification of termination of derivation for a fragment of dynamic logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2811594)