Proof systems for planning under 0-approximation semantics

作     者：SHEN YuPing ZHAO XiShun 

作者机构：Department of PhilosophyInstitute of Logic and CognitionSun Yat-sen University Institute of Logic and CognitionDepartment of PhilosophySun Yat-sen University 

出 版 物：《Science China(Information Sciences)》 (中国科学:信息科学(英文版))

年 卷 期：2014年第57卷第7期

页      面：117-128页

核心收录：

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

基　　金：supported by National Natural Science Foundation of China (Grant Nos.60970040,61272059) Ministry of Eduction (Grant Nos.11JJD720020,10JZD0006) Guangdong Young Scientists Programme (Grant Nos.GD10YZX03,WYM10114) 

主　　题：Hoare proof systems off-line planning plan generation plan verification automated reasoning 

摘      要：In this paper we propose Hoare style proof systems called PR0Dand PRKW0Dfor plan generation and plan verification under 0-approximation semantics of the action language *** PR0D(***0D),a Hoare triple of the form{X}c{Y}(resp.{X}c{KWp})means that all literals in Y become true(resp.p becomes known)after executing plan c in a state satisfying all literals in *** proof systems are shown to be sound and complete,and more importantly,they give a way to efficiently generate and verify longer plans from existing verified shorter plans by applying so-called composition rule,provided that an enough number of shorter plans have been properly *** idea behind is a tradeoff between space and time,we refer it to off-line planning and point out that it could be applied to general planning problems.