Loop-free verification of termination of derivation for a fragment of dynamic logic
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 w...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Vilnius University Press
2008-12-01
|
| Series: | Lietuvos Matematikos Rinkinys |
| Online Access: | https://www.journals.vu.lt/LMR/article/view/18111 |
| _version_ | 1819023447979720704 |
|---|---|
| author | Regimantas Pliuškevičius |
| author_facet | Regimantas Pliuškevičius |
| author_sort | Regimantas Pliuškevičius |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-21T04:39:03Z |
| format | Article |
| id | doaj.art-3e7209181c8f4cb0ae47b43292658f72 |
| institution | Directory Open Access Journal |
| issn | 0132-2818 2335-898X |
| language | English |
| last_indexed | 2024-12-21T04:39:03Z |
| publishDate | 2008-12-01 |
| publisher | Vilnius University Press |
| record_format | Article |
| series | Lietuvos Matematikos Rinkinys |
| spelling | doaj.art-3e7209181c8f4cb0ae47b43292658f722022-12-21T19:15:46ZengVilnius University PressLietuvos Matematikos Rinkinys0132-28182335-898X2008-12-0148proc. LMS10.15388/LMR.2008.18111Loop-free verification of termination of derivation for a fragment of dynamic logicRegimantas Pliuškevičius 0Institute of Mathematics and InformaticsA 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.https://www.journals.vu.lt/LMR/article/view/18111 |
| spellingShingle | Regimantas Pliuškevičius Loop-free verification of termination of derivation for a fragment of dynamic logic Lietuvos Matematikos Rinkinys |
| title | Loop-free verification of termination of derivation for a fragment of dynamic logic |
| title_full | Loop-free verification of termination of derivation for a fragment of dynamic logic |
| title_fullStr | Loop-free verification of termination of derivation for a fragment of dynamic logic |
| title_full_unstemmed | Loop-free verification of termination of derivation for a fragment of dynamic logic |
| title_short | Loop-free verification of termination of derivation for a fragment of dynamic logic |
| title_sort | loop free verification of termination of derivation for a fragment of dynamic logic |
| url | https://www.journals.vu.lt/LMR/article/view/18111 |
| work_keys_str_mv | AT regimantaspliuskevicius loopfreeverificationofterminationofderivationforafragmentofdynamiclogic |