Automated Reasoning over Deontic Action Logics with Finite Vocabularies

In this paper we investigate further the tableaux system for a deontic action logic we presented in previous work. This tableaux system uses atoms (of a given boolean algebra of action terms) as labels of formulae, this allows us to embrace parallel execution of actions and action complement, two action operators that may present difficulties in their treatment. One of the restrictions of this logic is that it uses vocabularies with a finite number of actions. In this article we prove that this restriction does not affect the coherence of the deduction system; in other words, we prove that the system is complete with respect to language extension. We also study the computational complexity of this extended deductive framework and we prove that the complexity of this system is in PSPACE, which is an improvement with respect to related systems.