基于模态逻辑D公理系统的Conformant规划方法

作     者：吕帅 刘磊 李莹 石莲 Lü Shuai;Liu Lei;Li Ying;Shi Lian

作者机构：吉林大学计算机科学与技术学院长春130012 吉林大学符号计算与知识工程教育部重点实验室长春130012 

出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)

年 卷 期：2009年第46卷第7期

页      面：1160-1168页

核心收录：

学科分类：0810[工学-信息与通信工程] 0808[工学-电气工程] 08[工学] 081104[工学-模式识别与智能系统] 0839[工学-网络空间安全] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 

基　　金：国家自然科学基金项目(60603031 60773097 60873044) 高等学校博士学科点基金项目(20050183065 20060183044 20070183057)~~ 

主　　题：conformant规划 模态逻辑 自动推理 可满足性 公理系统 D公理 

摘      要：2006年,conformant规划问题成为国际规划竞赛不确定性问题域中的标准测试问题,得到研究人员的广泛关注.目前,conformant规划系统都是将其看成信念状态空间上的启发式搜索问题予以求解.通过分析conformant规划问题的语法和语义,提出新的基于模态逻辑的规划框架,将其转换为模态逻辑D公理系统的一系列定理证明问题.提出2种基于模态逻辑的编码方式,构造相应的公理与推理规则形成模态公式集,保证对于D系统的定理证明过程等同于原问题的规划过程,并通过问题实例验证该方法的有效性.继基于SAT、CSP、线性规划、模型检测等求解技术的规划方法后,该规划框架是基于转换的规划方法的一种新的尝试.