Tableaux for Dynamic Logic of Propositional Assignments

TL;DR

This paper introduces an analytic tableaux calculus for the Dynamic Logic of Propositional Assignments (DL-PA), highlighting its meta-logical advantages over PDL and confirming its computational complexity.

Contribution

It presents a new tableaux calculus for DL-PA, demonstrating its effectiveness and aligning with known complexity results.

Findings

Tableaux calculus for DL-PA is sound and complete.

DL-PA enjoys properties like eliminability of Kleene star, compactness, and interpolation.

Complexity results for DL-PA are confirmed through the calculus.

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.