Automated Reasoning over Deontic Action Logics with Finite Vocabularies

Pablo F. Castro
(Universidad Nacional de Rio Cuarto - CONICET)
Thomas S. E. Maibaum
(McMaster University)

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.

In Nazareno Aguirre and Leila Ribeiro: Proceedings First Latin American Workshop on Formal Methods (LAFM 2013), Buenos Aires, Argentina, August 26th 2013, Electronic Proceedings in Theoretical Computer Science 139, pp. 16–30.
Published: 2nd January 2014.

ArXived at: https://dx.doi.org/10.4204/EPTCS.139.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org