On the Progression of Situation Calculus Universal Theories with Constants

Arenas, M, Baier, J, Navarro, J and Sardina, S 2018, 'On the Progression of Situation Calculus Universal Theories with Constants', in Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning, Tempe, United States, October 30 - November 2, pp. 484-493.


Document type: Conference Paper
Collection: Conference Papers

Title On the Progression of Situation Calculus Universal Theories with Constants
Author(s) Arenas, M
Baier, J
Navarro, J
Sardina, S
Year 2018
Conference name International Conference on Principles of Knowledge Representation and Reasoning
Conference location Tempe, United States
Conference dates October 30 - November 2
Proceedings title Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning
Publisher AAAI Press
Place of publication United States
Start page 484
End page 493
Total pages 10
Abstract The progression of action theories is an important problem in knowledge representation. Progression is second-order definable and known to be first-order definable and effectively computable for restricted classes of theories. Motivated by the fact that universal theories with constants (UTCs) are expressive and natural theories whose satisfiability is decidable, in this paper we provide a thorough study of the progression of situation calculus UTCs. First, we prove that progression of a (possibly infinite) UTC is always first-order definable and results in a UTC. Though first-order definable, we show that the progression of a UTC may be infeasible, that is, it may result in an infinite UTC that is not equivalent to any finite set of first-order sentences. We then show that deciding whether %or not there is a feasible progression of a UTC is undecidable. Moreover, we show that deciding whether %or not a sentence (in an expressive fragment of first-order logic) is in the progression of a UTC is CONEXPTIME-complete, and that there exists a family of UTCs for which the size of every feasible progression grows exponentially. Finally, we discuss resolution-based approaches to compute the progression of a UTC. This comprehensive analysis contributes to a better understanding of progression in action theories, both in terms of feasibility and difficulty.
Subjects Adaptive Agents and Intelligent Robotics
Copyright notice © 2018, Association for the Advancement of Artificial Intelligence (www.aaai.org).
Versions
Version Filter Type
Access Statistics: 9 Abstract Views  -  Detailed Statistics
Created: Tue, 26 Mar 2019, 09:36:00 EST by Catalyst Administrator
© 2014 RMIT Research Repository • Powered by Fez SoftwareContact us