PDL with data constants
From MaRDI portal
This paper considers an extension of classical propositional dynamic logic with new operators for programs such as \(\alpha\) \(\cap \beta\) (the intersection of the programs \(\alpha\) and \(\beta)\) and \({\bar \alpha}\) (the complement of the program \(\alpha)\) and new formulas such as \(\alpha\) \(\subset \beta\) and \(\alpha =\beta\), which is given an (infinitary) complete axiomatization and shown to be highly undecidable.
Recommendations
Cites work
- An elementary proof of the completeness of PDL
- First-order dynamic logic
- scientific article; zbMATH DE number 3843130 (Why is no real title available?)
- scientific article; zbMATH DE number 3853056 (Why is no real title available?)
- scientific article; zbMATH DE number 3731325 (Why is no real title available?)
- scientific article; zbMATH DE number 3735127 (Why is no real title available?)
- scientific article; zbMATH DE number 3266609 (Why is no real title available?)
- scientific article; zbMATH DE number 3315203 (Why is no real title available?)
- scientific article; zbMATH DE number 3198011 (Why is no real title available?)
- Propositional dynamic logic of regular programs
Cited in
(39)- Propositional dynamic logic with local assignments
- Infinitary propositional normal modal logic
- \(\Pi_ 1^ 1\)-universality of some propositional logics of concurrent programs
- A modal perspective on the computational complexity of attribute value grammar
- The complexity of PDL with interleaving
- Hybrid languages
- Towards reasoning about Hoare relations
- Propositional dynamic logic with quantification over regular computation sequences
- A propositional logic of Boolean recursive programs in which predicate variables appear in conditions
- Clausal tableaux for hybrid PDL
- Well-structured program equivalence is highly undecidable
- scientific article; zbMATH DE number 2084328 (Why is no real title available?)
- scientific article; zbMATH DE number 3845549 (Why is no real title available?)
- scientific article; zbMATH DE number 3858391 (Why is no real title available?)
- PDL with intersection of programs: a complete axiomatization
- PDL with negation of atomic programs
- scientific article; zbMATH DE number 3912350 (Why is no real title available?)
- scientific article; zbMATH DE number 3924749 (Why is no real title available?)
- scientific article; zbMATH DE number 3968565 (Why is no real title available?)
- scientific article; zbMATH DE number 3979045 (Why is no real title available?)
- scientific article; zbMATH DE number 3983144 (Why is no real title available?)
- scientific article; zbMATH DE number 4010497 (Why is no real title available?)
- scientific article; zbMATH DE number 4033711 (Why is no real title available?)
- scientific article; zbMATH DE number 4045721 (Why is no real title available?)
- scientific article; zbMATH DE number 139632 (Why is no real title available?)
- Derivation rules as anti-axioms in modal logic
- scientific article; zbMATH DE number 1114354 (Why is no real title available?)
- PDL is the bisimulation-invariant fragment of weak chain logic
- Deterministic SQEMA and application for pre-contact logic
- From positive PDL to its non-classical extensions
- Automated Reasoning
- Computer Science Logic
- Propositional dynamic logic with program quantifiers
- PDL with Intersection and Converse Is 2EXP-Complete
- Undecidability of PDL with \(L=\{a^{2^ i}| i\geq 0\}\)
- An essay in combinatory dynamic logic
- On the undecidability of logics with converse, nominals, recursion and counting
- Determinism and looping in combinatory PDL
- The many faces of counts-as: A formal analysis of constitutive rules
This page was built for publication: PDL with data constants
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1065545)
