Reasoning about actions with loops via Hoare logic

作     者：Jiankun HE Xishun ZHAO 无

作者机构：Institute of Logic and Cognition Sun Yat-sen University Guangzhou 512075 China 

出 版 物：《Frontiers of Computer Science》 (中国计算机科学前沿（英文版）)

年 卷 期：2016年第10卷第5期

页      面：870-888页

核心收录：

学科分类：07[理学] 08[工学] 070104[理学-应用数学] 0835[工学-软件工程] 0701[理学-数学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金 国家社会科学基金 Science Foundation of Ministry of Education of China the Fundamental Research Funds for the Central Universities 

主　　题：action language plan generation plan verification loop-plan Hoare logic 

摘      要：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.