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

MaRDI QIDQ2811594zbMATH OpenFDO

Authors R. Pliuškevičius

Publication date 10 June 2016

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

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)

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

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)