Tableaux for Dynamic Logic of Propositional Assignments
This work provides a proof system for DL-PA, which is incremental as it adapts existing tableaux methods to a logic with specific meta-logical properties.
The paper tackles the problem of reasoning in Dynamic Logic for Propositional Assignments (DL-PA) by defining an analytic tableaux calculus, and shows that it matches known complexity results.
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.