第3卷第4期 智能系统学报 Vol 3 Ng 4 2008年8月 CAA I Transactions on Intelligent Systems Aug 2008 一种逻辑强化学习的tableau推理方法 刘全2，崔志明，高阳2，陈道蓄2，姚望舒 (1苏州大学计算机科学与技术学院，江苏苏州215006：2南京大学软件新技术国家重点实验室，江苏南京210093) 摘要：tableau方法是一种具有较强的通用性和适用性的推理方法，但由于函数符号、等词等的限制，使得自动推理 具有不确定性.针对tableau推理中封闭集合构造过程具有盲目性的问题，提出将强化学习用于ableau自动推理的 方法.该方法将tableau推理过程中的逻辑公式与强化学习相结合，产生抽象的状态和活动.这样一方面可以通过学 习方法控制自动推理的推理顺序，形成合理的封闭分枝，减少推理的盲目性：另一方面复杂的推理可以利用简单的 推理结果，提高推理的效率。 关键词：逻辑强化学习；tableau推理 中图分类号：TP301文献标识码：A文章编号：1673-4785(2008)04-0355-06 Tableau rea son ng method ba sed on log ical re inforcement learn ng LIU Quan"2,CUIZhim ing,GAO Yang,CHEN Dao-xu',YAO W ang-shu (1.School ofCumputer Science of Technobgy,Soochow University,Suzhou 215006,China,2 State Key Laboratory for Novel Sofware Technobgy,Nanjing University,Nanjing 210093,China) Abstract:The tableau method is a reasoning method with high universality and applicability However,given the restrictions of function symbols and equations,there remains a great deal of uncertainty in automated reasoning In order to remove blind reasoning in the construction of a clsed set for tableau reasoning,a method was developed to introduce reinforcement leaming into tableau reasoning Reinforcement leaming was combined with the logical or mulae in tableau reasoning to produce abstract states and actions On the one hand,reasoning sequences in auto reasoning can be controlled by the leaming method to fom reasonable clsed branches and reduce the blindness of reasoning On the other hand,smple reasoning results can be reused in the complex reasoning system to mprove reasoning effic iency. Keywords:bgical reinforcement leaming tableau reasoning Tableau方法是1955年由Beh提出的一种推理 机科学家的兴趣，同归结一样，被认为是重要的自动 方法，其实质是将语义结构中的关系表现出来，使证 推理方法之一.近年来，tableau方法引起了更为广泛 明理论与语义联系起来.对于不同的逻辑系统，所使 的关注，成为语义WB山、自然语言理解)、数据库 用的tableaui规则是相同的，只是对公式构造集进行 修正)模型检测等推理系统的核心推理方法. 扩展，使之更接近相应的逻辑系统.由于tableau方法 对于自动推理来说，考核推理效率的2个重要 具有较强的通用性和直观性，从20世纪60年代开 指标就是推理所需要的时间和空间.在tableau推理 始，这种方法引起以Smullyan、Fitting为代表的计算 中也同样存在着效率问题.如对Y公式实例化的次 数的限定，以及δ公式中函数符号和自变量的限制， 收稿日期：2007-10-22 限制控制处理不得当，可以使一个简单的证明变得 基金项目：国家自然科学基金资助项目(60673092,60775046)：教有 部重点资助项目(207040)：中国博士后科研基金资助项目 非常复杂，延迟了tableau的封闭时间，甚至得不到 (20060390919):江苏省高校自然科学基金资助项目 (06KJB520104):江苏省博士后科研基金资助项目 证明.另外，由于等词的对称性，对于含等词的ab (060211C);江苏省现代企业信息化应用支撑软件工程技 leau会出现搜索空间膨胀，甚至死循环的现象.从经 术研究中心开发项目(SX200804). 通信作者：刘全.Emait quanliu@suda edu cn 典逻辑向非经典逻辑扩展方面看，虽然经典逻辑的 1994-2009 China Academie Journal Electronic Publishing House.All rights reserved.http://www.cnki.net第 3卷第 4期 智 能 系 统 学 报 Vol. 3 №. 4 2008年 8月 CAA I Transactions on Intelligent System s Aug. 2008 一种逻辑强化学习的 tableau推理方法 刘 全 1, 2 ,崔志明 1 ,高 阳 2 ,陈道蓄 2 ,姚望舒 1 (1. 苏州大学 计算机科学与技术学院 ,江苏 苏州 215006; 2. 南京大学 软件新技术国家重点实验室 ,江苏 南京 210093) 摘 要 : tableau方法是一种具有较强的通用性和适用性的推理方法 ,但由于函数符号、等词等的限制 ,使得自动推理 具有不确定性. 针对 tableau推理中封闭集合构造过程具有盲目性的问题 ,提出将强化学习用于 tableau自动推理的 方法. 该方法将 tableau推理过程中的逻辑公式与强化学习相结合 ,产生抽象的状态和活动. 这样一方面可以通过学 习方法控制自动推理的推理顺序 ,形成合理的封闭分枝 ,减少推理的盲目性 ;另一方面复杂的推理可以利用简单的 推理结果 ,提高推理的效率. 关键词 :逻辑强化学习 ; tableau推理 中图分类号 : TP301 文献标识码 : A 文章编号 : 167324785 (2008) 0420355206 Tableau reason ing method based on logical re inforcement learn ing L IU Quan 1, 2 , CU I Zhi2m ing 2 , GAO Yang 1 , CHEN Dao2xu 1 , YAO W ang2shu 2 (1. School of Cumputer Science of Technology, Soochow University, Suzhou 215006, China; 2. State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China) Abstract: The tableau method is a reasoning method with high universality and app licability. However, given the restrictions of function symbols and equations, there remains a great deal of uncertainty in automated reasoning. In order to remove blind reasoning in the construction of a closed set for tableau reasoning, a method was developed to introduce reinforcement learning into tableau reasoning. Reinforcement learning was combined with the logical for2 mulae in tableau reasoning to p roduce abstract states and actions. On the one hand, reasoning sequences in auto reasoning can be controlled by the learning method to form reasonable closed branches and reduce the blindness of reasoning. On the other hand, simp le reasoning results can be reused in the comp lex reasoning system to imp rove reasoning efficiency. Keywords: logical reinforcement learning; tableau reasoning 收稿日期 : 2007210222. 基金项目 :国家自然科学基金资助项目 ( 60673092, 60775046) ;教育 部重点资助项目 (207040) ;中国博士后科研基金资助项目 (20060390919) ;江苏 省 高 校 自 然 科 学 基 金 资 助 项 目 (06KJB520104) ; 江 苏 省 博 士 后 科 研 基 金 资 助 项 目 (060211C) ;江苏省现代企业信息化应用支撑软件工程技 术研究中心开发项目 ( SX200804). 通信作者 :刘 全. E2mail: quanliu@ suda. edu. cn. Tableau方法是 1955年由 Beth提出的一种推理 方法 ,其实质是将语义结构中的关系表现出来 ,使证 明理论与语义联系起来. 对于不同的逻辑系统 ,所使 用的 tableau规则是相同的 ,只是对公式构造集进行 扩展 ,使之更接近相应的逻辑系统. 由于 tableau方法 具有较强的通用性和直观性 ,从 20世纪 60年代开 始 ,这种方法引起以 Smullyan、Fitting为代表的计算 机科学家的兴趣 ,同归结一样 ,被认为是重要的自动 推理方法之一. 近年来 , tableau方法引起了更为广泛 的关注 ,成为语义 WEB [ 1 ]、自然语言理解 [ 2 ]、数据库 修正 [ 3 ]、模型检测 [ 4 ]等推理系统的核心推理方法. 对于自动推理来说 ,考核推理效率的 2个重要 指标就是推理所需要的时间和空间. 在 tableau推理 中也同样存在着效率问题. 如对 γ2公式实例化的次 数的限定 ,以及δ2公式中函数符号和自变量的限制 , 限制控制处理不得当 ,可以使一个简单的证明变得 非常复杂 ,延迟了 tableau的封闭时间 ,甚至得不到 证明. 另外 ,由于等词的对称性 ,对于含等词的 tab2 leau会出现搜索空间膨胀 ,甚至死循环的现象. 从经 典逻辑向非经典逻辑扩展方面看 ,虽然经典逻辑的