Plans with loops are more general and compact than classical sequential plans, and gaining increasing atten- tions in artificial intelligence （AI）. While many existing ap- proaches mainly focus on algorithmic issues...Plans with loops are more general and compact than classical sequential plans, and gaining increasing atten- tions in artificial intelligence （AI）. While many existing ap- proaches mainly focus on algorithmic issues, few work has been devoted to the semantic foundations on planning with loops. In this paper, we first develop a tailored action lan- guage , together with two semantics for handling do- mains 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 O- approximation semantics, which uses the so-called idea off- line planning and on-line querying strategy in knowledge compilation, i.e., the agent could generate and store short proofs as many as possible in the spare time, and then per- form quick query by constructing a long proof from the stored shorter proofs using compositional rule. We argue that both our semantics and proof system could serve as logical foun- dations for reasoning about actions with loops.展开更多
文摘Plans with loops are more general and compact than classical sequential plans, and gaining increasing atten- tions in artificial intelligence （AI）. While many existing ap- proaches mainly focus on algorithmic issues, few work has been devoted to the semantic foundations on planning with loops. In this paper, we first develop a tailored action lan- guage , together with two semantics for handling do- mains 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 O- approximation semantics, which uses the so-called idea off- line planning and on-line querying strategy in knowledge compilation, i.e., the agent could generate and store short proofs as many as possible in the spare time, and then per- form quick query by constructing a long proof from the stored shorter proofs using compositional rule. We argue that both our semantics and proof system could serve as logical foun- dations for reasoning about actions with loops.
