Proof systems for planning under 0-approximation semantics  

作　　者：SHEN YuPing ZHAO XiShun 

机构地区：[1]Department of Philosophy,Institute of Logic and Cognition,Sun Yat-sen University [2]Institute of Logic and Cognition,Department of Philosophy,Sun Yat-sen University

出　　处：《Science China(Information Sciences)》2014年第7期113-124,共12页中国科学（信息科学）（英文版）

基　　金：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)

摘　　要：In this paper we propose Hoare style proof systems called PRD^0and PRKWD^0 for plan generation and plan verification under 0-approximation semantics of the action language AK.In PRD^0 （resp.PRKW0D）,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 X.The 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 stored.The 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.In this paper we propose Hoare style proof systems called PRD^0and PRKWD^0 for plan generation and plan verification under 0-approximation semantics of the action language AK.In PRD^0 （resp.PRKW0D）,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 X.The 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 stored.The 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.

关 键 词：Hoare proof systems off-line planning plan generation plan verification automated reasoning 

分 类 号：TP391.1[自动化与计算机技术—计算机应用技术]