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.展开更多
Hoare logic is a logic used as a way of specifying semantics of programming languages, which has been extended to be a separation logic to reason about mutable heap structure. In a model M of Hoare logic, each program...Hoare logic is a logic used as a way of specifying semantics of programming languages, which has been extended to be a separation logic to reason about mutable heap structure. In a model M of Hoare logic, each program α induces an M-computable function fα M on the universe of M; and the M-recursive functions are defined on M. It will be proved that the class of all the M-computable functions fα M induced by programs is equal to the class of all the M- recursive functions. Moreover, each M-recursive function is ∑ 1 NM -definable in M, where the universal quantifier is a num- ber quantifier ranging over the standard part of a nonstandard model M.展开更多
In this paper we generalize the while-rule in Hoare calculus to an infinite one and then present a sufficient condition much weaker than the expressiveness for Cook's relative completeness theorem with respect to ...In this paper we generalize the while-rule in Hoare calculus to an infinite one and then present a sufficient condition much weaker than the expressiveness for Cook's relative completeness theorem with respect to our new axiomatic system. Using the extended Hoare calculus we can derive true Hoare formulas which contain while- statements free of loop invariants. It is also pointed out that the weak condition is a first order property and therefore provides a possible approach to the characterization of relative completeness which is also a first-order property.展开更多
文摘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.
文摘Hoare logic is a logic used as a way of specifying semantics of programming languages, which has been extended to be a separation logic to reason about mutable heap structure. In a model M of Hoare logic, each program α induces an M-computable function fα M on the universe of M; and the M-recursive functions are defined on M. It will be proved that the class of all the M-computable functions fα M induced by programs is equal to the class of all the M- recursive functions. Moreover, each M-recursive function is ∑ 1 NM -definable in M, where the universal quantifier is a num- ber quantifier ranging over the standard part of a nonstandard model M.
文摘In this paper we generalize the while-rule in Hoare calculus to an infinite one and then present a sufficient condition much weaker than the expressiveness for Cook's relative completeness theorem with respect to our new axiomatic system. Using the extended Hoare calculus we can derive true Hoare formulas which contain while- statements free of loop invariants. It is also pointed out that the weak condition is a first order property and therefore provides a possible approach to the characterization of relative completeness which is also a first-order property.
基金国家教育部博士点基金(the Fund for the Doctoral Program of the Ministry of Education of China under Grant No.20050359004)国家教育部新世纪优秀人才计划项目(the New Century Excellent Talent Foundation from MOE of China under Grant No.NCET-04-050562)安徽省科技公关计划项目(the Key Technologies R&D Program of Anhui Province, China under Grant No.06012069B)
