| Artificial Intelligence Planning is an important field in AI, which studies in generating a plan that will achieve a desired goal, given a description of some actions’ effects.In order to find a feasible plan, one need to study how an action affects the world state and agent’s knowledge state. This leads us to the field of “reasoning about actions and changes”, which allows us to predict whether a plan would achieve some goals that we want, and thus may help us come up with a feasible plan. Compared to traditional sequential planing(where a plan is a sequence of actions), planning with loops under incomplete information is more general and compact, and gaining increasing attentions in AI. While many existing approaches mainly focus on algorithmic issues, few work has been devoted to the semantic foundations on planning with loops. After considering and comparing several main logical representations of reasoning about actions, we choose action language, which has a natural concise syntax, to study the property of actions and related problems. In this paper, motivated by two examples, we first develop a tailored action language AL K, together with two semantics for handling domains with non-deterministic actions and loops. Then we propose a sound and(relative) complete Hoare-style proof system for efficient plan generation and verification under 0-approximation semantics, which uses the so-called idea off-line planning and on-line reasoning strategy from Knowledge Compilation,i.e., the agent could generate and store short proofs as many as possible in the spare time, and then perform quick query by constructing a long proof from the stored shorter proofs using compositional rule. Our system could generate and verify new plans by using the existing ones, which could improve the efficiency of real-world planning. We argue that both our semantics and proof system could serve as logical foundations for reasoning about actions with loops under non-deterministic domain. |
PDF Full Text Request