Loop-free verification of termination of derivation for a fragment of dynamic logic
Articles
Regimantas Pliuškevičius
Institute of Mathematics and Informatics
Published 2008-12-21
https://doi.org/10.15388/LMR.2008.18111
PDF

How to Cite

Pliuškevičius R. (2008) “Loop-free verification of termination of derivation for a fragment of dynamic logic”, Lietuvos matematikos rinkinys, 48(proc. LMS), pp. 283–287. doi: 10.15388/LMR.2008.18111.

Abstract

A fragment of a deterministic propositional dynamic logic (DPDL, in short) is considered The language of considered fragment contains propositional symbols, action constants, action operator (repetition) and logical symbols. For safety fragment of considered DPDL a loop-check-free sequent calculus with invertible rules is presented.

PDF
Creative Commons License

This work is licensed under a Creative Commons Attribution 4.0 International License.

Please read the Copyright Notice in Journal Policy