Tableaux for Dynamic Logic of Propositional Assignments
Logic in Computer Science
2014-06-10 v1 Artificial Intelligence
Abstract
The Dynamic Logic for Propositional Assignments (DL-PA) has recently been studied as an alternative to Propositional Dynamic Logic (PDL). In DL-PA, the abstract atomic programs of PDL are replaced by assignments of propositional variables to truth values. This makes DL-PA enjoy some interesting meta-logical properties that PDL does not, such as eliminability of the Kleene star, compactness and interpolation. We define and analytic tableaux calculus for DL-PA and show that it matches the known complexity results.
Keywords
Cite
@article{arxiv.1406.2161,
title = {Tableaux for Dynamic Logic of Propositional Assignments},
author = {Tiago de Lima and Andreas Herzig},
journal= {arXiv preprint arXiv:1406.2161},
year = {2014}
}
Comments
20 pages