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.展开更多
By L. we denote the set of all propositional fornmlas. Let C be the set of all clauses. Define C_n=C(Lη:η∈C}.In Sec. 2 of this paper. we prove that for normal modal logics S, the notions of (S. C_)-expansions and S...By L. we denote the set of all propositional fornmlas. Let C be the set of all clauses. Define C_n=C(Lη:η∈C}.In Sec. 2 of this paper. we prove that for normal modal logics S, the notions of (S. C_)-expansions and S-expansions coincide. In Sec. 3. we prove that if I consists of default clauses then the notions of S-expansions for I and (S.C)-expansions for I coincide. To this end. we first show. in Sec 3.that the notion of S-expansions for I is the same as that of (S.L)-expansions for I.展开更多
文摘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.
文摘By L. we denote the set of all propositional fornmlas. Let C be the set of all clauses. Define C_n=C(Lη:η∈C}.In Sec. 2 of this paper. we prove that for normal modal logics S, the notions of (S. C_)-expansions and S-expansions coincide. In Sec. 3. we prove that if I consists of default clauses then the notions of S-expansions for I and (S.C)-expansions for I coincide. To this end. we first show. in Sec 3.that the notion of S-expansions for I is the same as that of (S.L)-expansions for I.
