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 |