Abstract
In this paper we investigate tableau proof procedures for reasoning about actions and plans. Our framework is a multimodal language close to that of propositional dynamic logic, wherein we solve the frame problem by introducing the notion of dependence as a weak causal connection between actions and atoms. The tableau procedure is sound and complete for an important fragment of our language, within which all standard problems of reasoning about actions can be expressed, in particular planning tasks. Moreover, our tableaux are analytic and provide thus a decision procedure.
On leave from Universidade Federal do Paraná, Brazil
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
A.B. Baker. Nonmonotonic reasoning in the framework of situation calculus. Artificial Intelligence (AI), 49(1-3):5–23, may 1991.
T. Bylander. The computational complexity of propositional STRIPS planning. Artificial Intelligence (AI), 69(1-2):165–204, 1994.
L. Catach. Les logiques multi-modales. PhD thesis, Université Paris VI, France, 1989.
M.A. Castilho, O. Gasquet, and A. Herzig. Modal tableaux for reasoning about actions and plans. IRIT internal report, nov 1996.
G. De Giacomo and M. Lenzerini. PDL-based framework for reasoning about actions. In Proc. 4th Congresss of the Italian Association for Artificial Intelligence (IA * AI'95), number 992 in LNAI, pages 103–114. Springer-Verlag, 1995.
L. Farinas del Cerro and A. Herzig. Belief change and dependence. In Yoav Shoham, editor, Proc. 6th Conf. on Theoretical Aspects of Rationality and Knowledge (TARK'96), pages 147–162. Morgan Kaufmann Publishers, 1996.
E. Giunchiglia, G. N. Kartha, and V. Lifschitz. Actions with indirect effects (extended abstract). In Working notes of the AAAI-Spring Sysposium on Extending Theories of Actions, 1995.
M. Gelfond and V. Lifschitz. Representing action and change by logic programs. Journal of Logic Programming, pages 301–321, 1993.
R.P. Goré. Cut-free sequent and tableau systems for propositional normal modal logics. PhD thesis, University of Cambridge, England, 1992.
F. Giunchiglia and R Sebastiani. A SAT-based decision procedure for ALC. In Proc. Int. Conf. on Knowledge Representation and Reasoning (KR'96), pages 302–314, Cambridge, Massachussetts, 1996.
D. Harel. Dynamic logic. In D. Gabbay and F. Günthner, editors, Handbook of Philosophical Logic, volume II, pages 497–604. D. Reidel, Dordrecht, 1984.
A. Herzig. How to change factual beliefs using laws and independence information. In Dov M. Gabbay and Rudolf Kruse, editors, Proc. Int. Joint Conf. on Qualitative and Quantitative Practical Reasoning (ECSQARU/FAPR97), LNCS. Springer-Verlag, jun 1997.
S. Hanks and D. McDermott. Default reasoning, nonmonotonic logics, and the frame problem. In Proc. Nat. (US) Conf. on Artificial Intelligence (AAAI'86), pages 328–333, Philadelphia, PA, 1986.
A. Heuerding, M. Seyfried, and H. Zimmermann. Efficient loop-check for backward proof search in some non-classical propositional logics. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Proceedings of the 5th International Workshop TABLEAUX'96: Theorem Proving with Analytic Tableaux and Related Methods, number 1071 in LNAI, pages 210–225. Springer-Verlag, 1996.
G. N. Kartha and V. Lifschitz. Actions with indirect effects (preliminary report). In Proc. Int. Conf. on Knowledge Representation and Reasoning (KR'94), pages 341–350, 1994.
F. Lin. Embracing causality in specifying the indirect effects of actions. In Proc. of the 14th International Joint Conference on Artificial Intelligence (IJCAI'95), pages 1985–1991, Montreal, Canada, 1995.
F. Massacci. Personal communication, may 1997.
C. Mathieu. A resolution method for a non-monotonic multimodal logic. In S. Moral, editor, Proc. ECSQ UAR U'93, LNCS, pages 257–264. Springer-Verlag, 1993.
N. McCain and H. Turner. A causal theory of ramifications and qualifications. In Proc. of the 14th International Joint Conference on Artificial Intelligence (IJCAI'95), pages 1978–1984, 1995.
R. Reiter. The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression. Artificial Intelligence and Mathematical Theory of Computation, Papers in Honor of John McCarthy:359–380, 1991.
S. Rosenschein. Plan synthesis: a logical approach. In Proc. of the 8th International Joint Conference on Artificial Intelligence (IJCAI'81), pages 359–380, Academic Press, 1981.
E. Sandewall. Features and Fluents. Oxford University Press, 1995.
W. Stephan and S. Biundo. A new logical framework for deductive planning. In Proc. of the 13th International Joint Conference on Artificial Intelligence (IJCAI'93), pages 32–38, 1993.
P. Siegel. Représentation et utilisation de la connaissance en calcul propositionnel. PhD thesis, Université d'Aix-Marseille II, Aix-Marseille, France, jul 1987.
M. Thielscher. The logic of dynamic systems. In Proc, of the 14th International Joint Conference on Artificial Intelligence (IJCAI'95), pages 1956–1962, Montreal, Canada, 1995.
M. Thielscher. Ramification and causality. Artificial Intelligence (AI), 89:317–364, 1997.
G.S. Tseitin. On the complexity of derivations in propositional calculus. In Siekmann Wrightson, editor, Automated Reasoning 2: Classical papers on computational logic, pages 466–483, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Castilho, M.A., Gasquet, O., Herzig, A. (1997). Modal tableaux for reasoning about actions and plans. In: Steel, S., Alami, R. (eds) Recent Advances in AI Planning. ECP 1997. Lecture Notes in Computer Science, vol 1348. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63912-8_79
Download citation
DOI: https://doi.org/10.1007/3-540-63912-8_79
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63912-1
Online ISBN: 978-3-540-69665-0
eBook Packages: Springer Book Archive