机器学习：一种逻辑强化学习的tableau推理方法.pdf_大学文库

第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会出现搜索空间膨胀 ,甚至死循环的现象. 从经典逻辑向非经典逻辑扩展方面看 ,虽然经典逻辑的

·356· 智能系统学报第3卷相应规则和方法可以直接应用到非经典逻辑中，但 A 是有时会出现大量的冗余分枝，降低计算机的处理 A2 效率.近年来，针对tableau?推理效率问题，在tableau … 推理技术、策略及方法上有大量的研究，并且取得了 An 非常可喜的成果1在文献[6]中，针对制约自动推如果T为{A1,A2,,An}的一个tableau,且T为T 理发展的瓶颈推理的不确定性问题，提出了推应用tableau扩展规则后的结果，那么T也是{A1, 理器与机器学习相结合的未来发展方向.文献[7]、 A2,An的一个tableau [8等提出了将归纳学习、决策树学习等方法与模利用tableau方法进行定理证明，将被证明的公型生成推理方法相结合，用来模拟生物化学反应的式分为4类，即aBY8-公式，各类公式对应的过程.文献[9等提出了将机器学习与推理方法相 a规则为o1 结合，实现Web上智能化搜索.但这些方法大多是针对具体的某类逻辑公式而提出的，缺乏普遍性，仍 a 然不能解决推理中的不确定性问题，不利于计算机 … 实现 a 本文在强化学习的基础上，提出针对tableau自动 B-规则、Y-规则与6-规则分别为推理的逻辑强化学习方法.这种方法，可以从强化学习 B Y 6 B1…|B。Y1(以`8f(,n)) 的层面上找到tableau扩展的最佳方法，适用于多种类式中：y是一个自由变量，f是一个新skolen函数符型的tableau推理.该方法对于更大程度地减少tableau 号，，x是分枝中出现的自由变量扩展的盲目性不确定性，具有重要的意义 12强化学习 1预备知识强化学习是一种从环境状态到动作映射的学 L.1逻辑与tableau推理习山其主要解决的问题是：一个能够感知环境的自一阶符号为元数m≥0的关系符号P的集合治Aent如何通过学习选择达到其目标的最优动作及常量C的集合组成.如果关系符号p∈P的元数类似问题普遍存在于自动控制、工序优化、棋类对弈 m(m≥0)为0，则p称为命题.项是变量X或常量等领域.Agent在其环境中作出每个动作时，会从环境 Cp为n元谓词符号，，为项，则p(,) 中得到奖励或惩罚信息，以表示结果状态的正确与为原子，记为A左.一个替换是形如{/，…/} 否.A gent的任务是从这个非直接的有延迟的回报中的一个有限集合，其中%是变量符号，4是不同于学习，以便后续的动作产生最大的累积回报].标准的项，并且在此集合中不存在斜线符号后面相同变的Agenti强化学习框架结构如图1所示量符号的2个元素，称为替换的分子，为替换的回报分母，当，…，为基项时，称此替换为基替换.合状态取A为原子集合.合取A称为合取B的包含，如果存在一个替换日，使得B0CA,记为A≤B.当项、原子或子句E不包含变量时称为基例.表达式集合活动 {E,E的合一o称为最一般合一，当且仅当对图1标准的A gent强化学习框架结构此集合的每一个合一日，都存在替换入，使得0=0· Fig 1 The framework of standard Agent reinforcement 入，对于原子a和b的最一般合一记为mgu(a,b). leaming ∑的Herbrand基表示为HBz,是由所有∑中谓词和 Agent学习可以表述为马尔可夫决策过程函数符号构成的基原子集合 (Markov decison process,MDP),MDP是一个元组令A1,A2,…An}为公式的有限集合.下列分 M=(S,A,T,R),这里S是系统状态集；A是活动枝树为公式A1,A2,An}的一个tableau: 集，对于每个状态s∈S,A gent都可以得到一个有穷 1994-2009 China Academic Journal Electronic Publishing House.All rights reserved.http://www.cnki.net

相应规则和方法可以直接应用到非经典逻辑中 ,但是有时会出现大量的冗余分枝 ,降低计算机的处理效率. 近年来 ,针对 tableau推理效率问题 ,在 tableau 推理技术、策略及方法上有大量的研究 ,并且取得了非常可喜的成果 [ 5 ] . 在文献 [ 6 ]中 ,针对制约自动推理发展的瓶颈 ———推理的不确定性问题 ,提出了推理器与机器学习相结合的未来发展方向. 文献 [ 7 ]、 [ 8 ]等提出了将归纳学习、决策树学习等方法与模型生成推理方法相结合 ,用来模拟生物化学反应的过程. 文献 [ 9 ]等提出了将机器学习与推理方法相结合 ,实现 W eb上智能化搜索. 但这些方法大多是针对具体的某类逻辑公式而提出的 ,缺乏普遍性 ,仍然不能解决推理中的不确定性问题 ,不利于计算机实现. 本文在强化学习的基础上 ,提出针对 tableau自动推理的逻辑强化学习方法. 这种方法 ,可以从强化学习的层面上找到 tableau扩展的最佳方法 ,适用于多种类型的 tableau推理.该方法对于更大程度地减少 tableau 扩展的盲目性、不确定性 ,具有重要的意义. 1预备知识 1. 1 逻辑与 tableau推理一阶符号 ∑为元数 m ≥0的关系符号 P的集合及常量 C的集合组成. 如果关系符号 p∈P的元数 m (m ≥0)为 0,则 p称为命题. 项是变量 X 或常量 C. p为 n元谓词符号 , t1 , …, tn 为项 ,则 p ( t1 , …, tn ) 为原子 ,记为 A t∑. 一个替换是形如 { t1 / v1 , …, tn / vn } 的一个有限集合 ,其中 vi 是变量符号 , ti 是不同于 vi 的项 ,并且在此集合中不存在斜线符号后面相同变量符号的 2个元素 ,称 ti 为替换的分子 , vi 为替换的分母 ,当 t1 , …, tn 为基项时 ,称此替换为基替换. 合取 A为原子集合. 合取 A 称为合取 B 的 θ2包含 ,如果存在一个替换 θ,使得 Bθ< A,记为 A≤θB. 当项、原子或子句 E不包含变量时称为基例. 表达式集合 { E1 , …, Ek }的合一 σ称为最一般合一 ,当且仅当对此集合的每一个合一 θ,都存在替换 λ,使得 θ=σ· λ,对于原子 a和 b的最一般合一记为 mgu ( a, b). ∑的 Herbrand基表示为 HB∑ ,是由所有 ∑中谓词和函数符号构成的基原子集合. 令 { A1 , A2 , …, An }为公式的有限集合. 下列分枝树为公式 {A1 , A2 , …, An }的一个 tableau: A1 A2 … An 如果 T为 {A1 , A2 , …, An }的一个 tableau,且 T 3 为 T 应用 tableau扩展规则后的结果 ,那么 T 3 也是 { A1 , A2 , …, An }的一个 tableau. 利用 tableau方法进行定理证明 ,将被证明的公式分为 4类 ,即 α2、β2、γ2、δ2公式 ,各类公式对应的 α2规则为 [ 10 ] α α1 … αn β2规则、γ2规则与 δ- 规则分别为 β β1 | … | βn 、 γ γ1 ( y) 、 δ δ1 ( f ( x1 , …, xn ) ) . 式中 : y是一个自由变量 , f是一个新 skolen函数符号 , x1 , …, xn 是分枝中出现的自由变量. 1. 2 强化学习强化学习是一种从环境状态到动作映射的学习 [ 11 ] .其主要解决的问题是 :一个能够感知环境的自治 Agent,如何通过学习选择达到其目标的最优动作. 类似问题普遍存在于自动控制、工序优化、棋类对弈等领域. Agent在其环境中作出每个动作时 ,会从环境中得到奖励或惩罚信息 ,以表示结果状态的正确与否. Agent的任务是从这个非直接的有延迟的回报中学习 ,以便后续的动作产生最大的累积回报 [ 12 ] . 标准的 Agent强化学习框架结构如图 1所示. 图 1 标准的 Agent强化学习框架结构 Fig. 1 The framework of standard Agent reinforcement learning Agent学习可以表述为马尔可夫决策过程 (Markov decision p rocess, MDP) , MDP是一个元组 M = (S, A, T, R ) ,这里 S 是系统状态集; A 是活动集 ,对于每个状态 s∈S, Agent都可以得到一个有穷 ·356· 智能系统学报第 3卷

第4期刘全，等：一种逻辑强化学习的tableau推理方法 ·357 的活动集A(s)∈A:T为迁移，对于每个ss'∈S和态0是{g(f(x))≈，g()≈f(五， a∈A(,都存在一个迁移T使得状态从s转移到 P(g(f(a),b).如果一个可能状态中存在互补 s,即表示为，严s!这里p表示由活动a引起的对，那么该状态称为封闭状态.抽象状态{门P(a, 从状态s迁移到s的概率，且对于每个s∈S,a∈A都 c以，gf))≈，g&≈f(,P(g(fa,b, 满足(y:∑esp(3a,s)=L对于每个迁移，Agent P(a,b),P(,c以在替换a/:后，是封闭状态. 都可以获得一个立时回报R(sa,s)=r在这种情定义3一个抽象迁移To的形式为B。D0 况下，回报函数R只依赖于目前的状态和活动，如 Ho,这里P(To):=p∈0,11，R(To):=r∈0,1，果R是概率的，那么称它为非确定性的，否则称为 a是一个抽象活动，且body(To):=Bo且head 确定性的.一个策略π：S→A,它基于当前观察到的 (o:=Ho是抽象状态，这里，body/1和head/1为2 状态s选择下一步动作a,即Ⅱ(s)=a,因此A- 个一阶谓词。 ent的任务是找到一个策略π'，使得对于所有的状假设Io的范围是受限的，即vars(Ho)vars 态s∈S,值函数(s,最大.(s主要有以下3 (Bo)且vars(a)∈vars(Bo),vars/1为一个受限一种形式阶谓词.则抽象转换只依赖于目前状态的信息编码折算累积回报：V(s)=Y+, 抽象转换的主要思想是：如果Aent处于状态Z,使得B≤Z,那么活动有限水平回报：产(s)三) a在概率p下，将转移到状态Z':=[ZB01UH0 得到的直接回报为r 平均回报：(s)=m hh 在tableau推理中，引起状态迁移的惟一原因是这里使用的未解释的记号和概念，请参见文献扩展规则的使用，即α规则在抽象状态内部，使得 [7和[121 合取元素得到扩展，B规则可以使一个抽象状态分解为多个状态，Y规则和δ规则分别引入了自变量 2逻辑强化学习和函数符号 MDP的逻辑组成对应于一个有穷的状态机，由为了说明问题，考虑下面的抽象迁移，上述含等于状态和活动是非结构的，因此这个自动机必须是词公式由一种状态迁移到另一种状态：以命题表示.通过逻辑马尔可夫决策程序(logical {(x)((g(x)≈f(x))V门(x≈a), Markov decison process,LOMDP])可以通过逻辑符 (x)(g(fx划≈x),b≈cp(g(g(a)),b), 号来替代同类状态和活动，最大程度地减少状态和 7p(ac以}Q9:-1:la脸 f(g(x2)≈f(为)) 活动的数量 V门（≈a),gfx)≈，ecp(g（g(a) 定义1令A为逻辑，「为A中的定理，P为A 中的谓词集合，C为A中的常量集合，A为A中的特 b),7p(a,c} 定的活动谓词集合.逻辑马尔可夫决策程序(LOM- 应用到状态Ep: DP)定义为Mo=(So,Ao,Io,R),其中So= fx)(gx)≈f(x)V门（≈a),(x) fs∈HB"vC IsE『,Ao≡{a∈HBuc|a非「，To (gfx))≈x),b≈cp(g(g(a)),b),p(a S04oSo→0,11 c以定义2抽象状态是一个逻辑原子的合取式，当执行抽象迁移rl alfa后，后继状态为即逻辑查询.这里空合取记为0 {(g()≈f&))V门(&≈a,gfm))≈ 抽象状态表示状态集，状态So是在∑上的一个 ,b≈cp(g(g(al),bl,门p(a.c 基例的有穷合取，即Herbrand子集上的逻辑解释. 转换概率为09，获得直接回报为·1 在一个含等词的逻辑公式{(Hx)((g(x)≈ 下面是基于逻辑强化学习的tableau算法. f(x))V门（≈a)),(x)g(f(x))≈x),≈c 算法1： P(g(g(ad),b,7P(a,c中，一个可能的抽象状初始化Q。,对所有的(sa)赋初值0 1994-2009 China Academic Journal Electronic Publishing House.All rights reserved.http://www.cnki.net

的活动集 A ( s) ∈A; T为迁移 ,对于每个 s, s′∈S 和 a∈A (s) ,都存在一个迁移 T,使得状态从 s转移到 s′,即表示为 s p: r: a s′. 这里 p表示由活动 a引起的从状态 s迁移到 s′的概率 ,且对于每个 s∈S, a∈A都满足 (s) : ∑s′∈S p ( s, a, s′) = 1. 对于每个迁移 , Agent 都可以获得一个立时回报 R ( s, a, s′) = r. 在这种情况下 ,回报函数 R 只依赖于目前的状态和活动 ,如果 R是概率的 ,那么称它为非确定性的 ,否则称为确定性的. 一个策略 π: S →A,它基于当前观察到的状态 st 选择下一步动作 at ,即 π ( st ) = at . 因此 A2 gent的任务是找到一个策略 π3 ,使得对于所有的状态 st ∈S,值函数 V π ( st )最大. V π ( st )主要有以下 3 种形式 : 折算累积回报 :V π (st ) ≡ ∑ ∞ i =0 γi rt+i , 有限水平回报 :V π (st ) ≡ ∑ ∞ i =0 rt+i , 平均回报 : V π (st ) ≡ limh→∞ 1 h ∑ h i =0 γt+i . 这里使用的未解释的记号和概念 ,请参见文献 [7 ]和 [ 12 ]. 2 逻辑强化学习 MDP的逻辑组成对应于一个有穷的状态机 ,由于状态和活动是非结构的 ,因此这个自动机必须是以命题表示. 通过逻辑马尔可夫决策程序 ( logical Markov decision p rocess, LOMDP])可以通过逻辑符号来替代同类状态和活动 ,最大程度地减少状态和活动的数量. 定义 1 令 Λ为逻辑 ,Γ为 Λ中的定理 , P为 Λ 中的谓词集合 , C为Λ中的常量集合 , &为Λ中的特定的活动谓词集合. 逻辑马尔可夫决策程序 (LOM2 DP)定义为 MLO = ( SLO , ALO , TLO , R ) , 其中 SLO ≡ { s∈HB P∪C | s5 Γ}, ALO ≡{ a∈HB &∪C | a 5 Γ}, TLO : SLO ×ALO ×SLO →[0, 1 ]. 定义 2 抽象状态是一个逻辑原子的合取式 , 即逻辑查询. 这里空合取记为 ª. 抽象状态表示状态集 ,状态 SLO是在 ∑上的一个基例的有穷合取 ,即 Herbrand子集上的逻辑解释. 在一个含等词的逻辑公式 { ( Π x ) ( ( g ( x ) ≈ f ( x) ) ∨┐ ( x≈ a) ) , ( Π x) ( g ( f ( x) )≈ x) , b≈ c, P ( g ( g ( a) ) , b) , ┐P ( a, c) }中 ,一个可能的抽象状态 sLO 是 { g ( f ( x1 ) ) ≈ x1 , g ( x2 ) ≈ f ( x2 ) , P ( g ( f ( a) ) , b) }. 如果一个可能状态中存在互补对 ,那么该状态称为封闭状态. 抽象状态 { ┐P ( a, c) , g ( f ( x1 ) )≈ x1 , g ( x2 )≈ f ( x2 ) , P ( g ( f ( a) ) , b) , P ( a, b) , P ( x2 , c) }在替换 a / x2 后 ,是封闭状态. 定义 3 一个抽象迁移 TLO的形式为 BLO p∶r∶α HLO ,这里 P (TLO ) ∶ = p∈[0, 1 ], R (TLO ) ∶ = r∈[0, 1 ], a是一个抽象活动, 且 body ( TLO ) ∶ = BLO且 head (TLO ) : =HLO是抽象状态,这里, body/1和 head /1为 2 个一阶谓词. 假设 TLO的范围是受限的 ,即 vars(HLO ) Α vars (BLO )且 vars( a) Α vars(BLO ) , vars/1为一个受限一阶谓词. 则抽象转换只依赖于目前状态的信息编码. 抽象转换的主要思想是 : 如果 Agent处于状态 Z,使得 B ≤θZ,那么活动 a在概率 p下 ,将转移到状态 Z′∶= [ Z \Bθ] ∪Hθ, 得到的直接回报为 r. 在 tableau推理中 ,引起状态迁移的惟一原因是扩展规则的使用 ,即 α2规则在抽象状态内部 ,使得合取元素得到扩展 ,β2规则可以使一个抽象状态分解为多个状态 ,γ2规则和 δ2规则分别引入了自变量和函数符号. 为了说明问题 ,考虑下面的抽象迁移 ,上述含等词公式由一种状态迁移到另一种状态 : { ( Π x ) ( ( g ( x ) ≈ f ( x ) ) ∨┐ ( x≈ a ) ) , ( Π x) ( g ( f ( x) )≈ x ) , b≈ c, p ( g ( g ( a ) ) , b ) , ┐p ( a, c) } 0. 9∶ - 1∶rl_alfa { ( g ( x2 ) ≈ f ( x2 ) ) ∨┐( x2≈ a) , g ( f ( x1 ) )≈ x1 , b≈ c, p ( g ( g ( a ) ) , b) , ┐p ( a, c) }. 应用到状态 Exp: { ( Π x) ( ( g ( x)≈ f ( x) ) ∨┐ ( x≈ a) ) , ( Π x) ( g ( f ( x ) )≈ x ) , b≈ c, p ( g ( g ( a ) ) , b) , ┐p ( a, c) }. 当执行抽象迁移 rl_alfa后 ,后继状态为 { ( g ( x2 ) ≈ f ( x2 ) ) ∨┐ ( x2 ≈ a) , g ( f ( x1 ) ) ≈ x1 , b≈ c, p ( g ( g ( a) ) , b) , ┐p ( a, c) }. 转换概率为 0. 9,获得直接回报为 - 1. 下面是基于逻辑强化学习的 tableau算法. 算法 1: 初始化 Q0 ,对所有的 (s, a)赋初值 0 第 4期刘全 ,等 :一种逻辑强化学习的 tableau推理方法 ·357·

·358· 智能系统学报第3卷 e:=0 元组的元素有对应关系，每一个LOMDP MLo= do forever (So,Ao,Io,R)对应于一个离散的M=(S,A,T e:=e+1 R),证毕元=0 引理1给定一个tableau抽象状态序列产生一个随机状态 (S,)osm,如果tableau S,(0≤j≤n)是「可满足的， while not cbse(s)do/*判断是否为封闭状态那么tableau S,+1也是「可满足的 */ 证明令B是通过应用经典扩展规则或定理选择tableau规则a 扩展规则形成的抽象活动，从抽象状态S,到S+的执行规则a, 分枝，应用定理封闭规则可以删除封闭分枝.令M= 接收到立即回报=r(s,a) D,)为可满足S,的「结构观察新状态马1 令v为任意变量，应用B规则，在S,中必然存 r=i+1 在分枝B使得M,以卡B,如果B不同于B,那么 endwhile B'∈S+l for j=i-1 to0 do 另外，如果B'=B,那么M,以卡B.令B为在B 产生实例x=(s,g,g小，4：=方+ma此Q.(5* 中应用B规则得到的公式，根据B公式的性质，M, a y卡B必然有M,y卡B,或M,yFB,因此有M, 如果实例中存在(s,a,u,那么用x来替以卡B1B)UB或M,以卡(B1B})U 换它，否则加入x 存在，因此(B\B})UB,和M,)卡(B1B;)U 对于一个简单的例子(p(x)Vq(x))八 B2在S+中 p(alFq(a,可以使用算法l产生一个tableau过 ā和Y规则证明与B规则证明相类似程，如表1所示令δ为应用δ规则从S,到S1得到的δ公式表1公式(p(x)Vq(x))∧p(a)卜q(a)的基于逻辑强化 8,fx,x))为加到分枝中的公式f是新的学习的tablea ui过程 skolem函数符号，且，，x是在8中的自由变 Table I Tableau process based on logical renforcement leam- 量).定义一个不同于M的结构M'=(D,),除了 ing of fommuh (p(x)Vq(x))A p(a)(a) 新的函数符号油1解释外，其他按如下方法定义： Example 1 Example 2 Example 3 Example 4 Qvalue(0.81) Qvalue(0.9) Qvalue(1.0)Qvalue (1.0) 对于在区间D中的每个元素集d,…d,如果存在 rl alfa rl alfa rl beta rl beta 一个元素d使得M,)卡6(x),这里5(x)=d plt)A plal p(x)Vg(x) p(x) q(a) (1≤≤m且5(x)=d那么f(d,,d)=d如果 g(a) p(a) p(a) p(a) 存在如此元素d,可选其中之一，如果不存在此类元 g(a) g(a) q(a) 素，可以在区域中选择任意元素.对于所有的变量赋在替换x下，为封闭状态封园默态> 值r如果M,以卡8那么M:以卡6，(f(, x)人.由于不出现在「中，故M为「结构定理1每一个LOMDP中Mo=(So,Ao, 令v为任意变量赋值，在S,中必然存在分枝 Io,R)对应于一个离散的M=(S,A,T,R) B,使得(M,v)FB!如果B不同于B,那么证明令HB HBs为抽象状态谓词的所有 M:WFB'(f不出现在B中)且B'∈S+ 基原子的集合，HB三HBz为抽象活动谓词的所有当8∈B'=B,必然有M,)F6(M'以E 基原子的集合.状态集合S。都包含在有穷的集合 8(f,m,这样(B1(δ})U6,(f(x, HB中，活动集合a都包含在有穷的集合HB中， x))在S+的一个分枝上，并且由M满足一个抽象迁移o是一个形式为BE巴H。,其中定理扩展规则：令反驳(o,P,P})用于扩 Bo和H都为抽象状态，a为抽象活动，Mo中的R 展tableau,由于S,为T可满足的，那么S,o也是T- 与M中的R相同.因此可以看出，Mo和M中的四可满足的.令M为「结构满足S,o,且v为任意变量 1994-2009 China Academic Journal Electronic Publishing House.All rights reserved.http://www.cnki.net

e: = 0 do forever e: = e + 1 i: = 0 产生一个随机状态 s0 while not close (si ) do /3 判断是否为封闭状态 3 / 选择 tableau规则 ai 执行规则 ai 接收到立即回报 ri = r(si , ai ) 观察新状态 si + 1 i: = i + 1 endwhile for j = i - 1 to 0 do 产生实例 x = (sj , aj , qj ) , qj: = rj +maxa′Qe (sj +1 , a′) 如果实例中存在 ( sj , aj , qold ) , 那么用 x来替换它 ,否则加入 x. 对于一个简单的例子 ( p ( x ) ∨ q ( x ) ) ∧ p ( a) ├q ( a) ,可以使用算法 1产生一个 tableau过程 ,如表 1所示. 表 1 公式 ( p ( x) ∨q ( x) ) ∧┐ p ( a ) ├q ( a )的基于逻辑强化学习的 tableau过程 Table 1 Tableau process based on logical re inforcement learn2 ing of formula (p (x) ∨q (x) ) ∧┐ p (a) ├q (a) Example 1 Example 2 Example 3 Examp le 4 Qvalue (0. 81) rl_alfa (p(x)∨q(x))∧ ┐ p(a) ┐ q ( a) Qvalue (0. 9) rl_alfa p ( x) ∨q ( x) ┐ p ( a) ┐ q ( a) Qvalue (1. 0) rl_beta p ( x) ┐ p ( a) ┐ q ( a) 在替换 x / a下 ,为封闭状态 Qvalue (1. 0) rl_beta q ( a) ┐ p ( a) ┐ q ( a) 封闭状态定理 1 每一个 LOMDP 中 MLO = ( SLO , ALO , TLO , R )对应于一个离散的 M = (S, A, T, R ). 证明令 HB S Σ Α HBΣ 为抽象状态谓词的所有基原子的集合 , HB a Σ Α HBΣ 为抽象活动谓词的所有基原子的集合. 状态集合 SLO都包含在有穷的集合 HB S Σ 中 ,活动集合 a都包含在有穷的集合 HB a Σ 中 , 一个抽象迁移 TLO是一个形式为 BLO p: r:α HLO ,其中 BLO和 HLO都为抽象状态 , a为抽象活动 , MLO中的 R 与 M 中的 R 相同. 因此可以看出 , MLO和 M 中的四元组的元素有对应关系 , 每一个 LOMDP MLO = (SLO , ALO , TLO , R )对应于一个离散的 M = (S, A, T, R ) ,证毕. 引理 1 给定一个 tableau 抽象状态序列 (Sj ) 0≤j≤n ,如果 tableau Sj (0≤j≤n)是 Γ2可满足的 , 那么 tableau Sj + 1也是 Γ2可满足的. 证明令 B 是通过应用经典扩展规则或定理扩展规则形成的抽象活动 ,从抽象状态 Si 到 Si + 1的分枝 ,应用定理封闭规则可以删除封闭分枝. 令M = 〈D, I〉为可满足 Si 的 Γ2结构. 令 v为任意变量 ,应用 β2规则 ,在 Si 中必然存在分枝 B ′使得 (M , v) 5 B ′,如果 B ′不同于 B ,那么 B ′∈Si + 1 . 另外 ,如果 B ′=B ,那么 (M , v) 5 B. 令 β为在 B 中应用β2规则得到的公式 ,根据β2公式的性质 , (M , v) 5 β必然有 (M , v) 5 β1 或 (M , v) 5 β2 ,因此有 (M , v) 5 (B \{β} ) ∪{β1 }或 (M , v) 5 (B \{β} ) ∪{β2 } 存在 ,因此 (B \{β} ) ∪{β1 }和 (M , v) 5 (B \{β} ) ∪ {β2 }在 Si + 1中. α2和 γ2规则证明与 β2规则证明相类似. 令 δ为应用 δ2规则从 Si 到 Si + 1得到的 δ2公式 , δ1 ( f ( x1 , …, xm ) )为加到分枝中的公式 ( f是新的 skolem函数符号 ,且 x1 , …, xm 是在 δ中的自由变量 ). 定义一个不同于 M 的结构 M ′=〈D, I′〉,除了新的函数符号 f由 I′解释外 ,其他按如下方法定义 : 对于在区间 D中的每个元素集 d1 , …, dm ,如果存在一个元素 d使得 (M ,ξ) 5 δ1 ( x ) , 这里 ξ( xj ) = dj (1≤j≤m )且 ξ( x) = d,那么 f I ( d1 , …, dm ) = d. 如果存在如此元素 d,可选其中之一 ,如果不存在此类元素 ,可以在区域中选择任意元素. 对于所有的变量赋值 v:如果 (M , v) 5 δ, 那么 (M ′, v) 5 δ1 ( f ( x1 , …, xm ) ). 由于 f不出现在 Γ中 ,故 M ′为 Γ2结构. 令 v为任意变量赋值 , 在 Si 中必然存在分枝 B ′,使得 (M , v ) 5 B ′, 如果 B ′不同于 B , 那么 (M ′, v) 5 B ′( f不出现在 B ′中 )且 B ′∈Si + 1 . 当 δ∈B ′= B , 必然有 (M , v) 5 δ, (M ′, v) 5 δ1 ( f ( x1 , …, xm ) ) ,这样 (B \ { δ} ) ∪{δ1 ( f ( x1 , …, xm ) ) }在 Si + 1的一个分枝上 ,并且由 M ′满足. 定理扩展规则 :令反驳〈σ, {ρ1 , …,ρk } 〉用于扩展 tableau,由于 Si 为 Γ2可满足的 ,那么 Siσ也是 Γ2 可满足的. 令 M 为Γ2结构满足 Siσ,且 v为任意变量 ·358· 智能系统学报第 3卷

赋值 ,那么必然有分枝 B ′∈Siσ,且 (M , v) 5 B ′. 根据 γ2公式的定义 , 有 B 5 Γ °{ ( Π x i 1 ) … (Π x i m i )φj | 1≤j≤p}使得 Bσ5 Γ °{ ( Π x i 1 ) …( Π x i m i ) φσj },即 (M , v) 5 Φσ,这里 Φ = { ( Π x i 1 ) … ( Π x i m i ) φj | 1≤j≤p},因为〈σ, {ρ1 , …,ρk } 〉为 Φ的反驳 ,使得 Φσ5 Γ°ρ1 ∨…∨ρk ,对于某一 j∈{ 1, …, k },必有 (M , v) 5 ρj ,即 M 满足 Si + 1中的分枝 Bσ∪{ρj}. 证毕. 定理 2 如果对于公式 φ存在一个 tableau抽象状态证明序列 { { ┐φ} } = S0 , S1 , …, Sn - 1 , Sn = ª ( n≥0) ,那么 φ是一个 Γ2重言式. 证明 φ是 Γ2不可满足的 ,那么根据引理 1, Tn 也是 Γ2不可满足的 ,依次类推 , Sn - 1 , …, S1 , S0 是 Γ2 不可满足的. 这样 ,第 1个 tableau{ { ┐φ} }也是 Γ2 不可满足的 ,即 ┐φ是 Γ2不可满足的 ,这等价于 φ 是 Γ2不可满足的. 证毕. 3 实验结果将基于逻辑强化学习的 tableau 方法应用于 TableauTAP系统 [ 13 ] 中 ,在 W indows环境下 , 应用 SW I2PROLOG语言对该系统进行了实现 ,主要是将基于强化学习的 tableau过程自动生成 Prolog程序 , 并与原系统中的推理规则相结合 ,形成一个可运行的推理程序. 应用改进后的系统对 TPTP自动推理测试库中的 400个问题进行了证明 ,并与原系统进行了对比 ,结果见表 2. 表 2 TPTP中定理的证明结果对比表 Table 2 The theorem prov ing results con tra st in TPTP 算法 VarLim 限定次数测试封闭分枝数封闭分枝数 CPU时间 /s 占内存空间 /byte 改进 TableauTAP 982 1 354 457 123. 243 9 512 原 TableauTAP 1 560 10 230 5 020 845. 891 205 422 从表 2中可以看出 ,改进后的 TableauTAP的几项指标均优于原系统 ,尤其是在 CPU时间方面 ,由于 TableauTAP具有学习功能 ,后继的证明可以学习到前面的证明结论 ,因此运行速度要比原系统高得多. 同时由于该方法的普遍性 ,使得编程时不需要针对不同的逻辑系统考虑太多的情况 ,使得程序代码比其他的系统要小得多 ,也更容易应用到自动推理作为推理机的实际应用系统中. 4 结束语本文提出了将逻辑强化学习用于 tableau推理的方法 ,对处理 tableau推理的盲目性具有一定的价值. 但该研究只是相关研究的开端 ,正在研究和将要研究的内容主要包括以下几方面 : 1)拟采用 tableau 推理模型对逻辑状态和逻辑活动进行建模 ,研究一种新的函数估计模型 ,使其一方面能够以任何精度逼近理论的强化学习值函数 ,另一方面在增量环境中保证收敛性. 2)拟将布尔剪枝、IP2tableau等方法与逻辑强化学习相结合 ,对逻辑状态空间模型进行相应的等价转换 ,采用解线性方程组的方式来简化状态空间 ,降低状态空间维数 ,解决大规模、连续的 MDP问题. 在 tetris问题中 ,试验所设计的强化学习框架和算法 ,并对比收敛速度. 3)结合所研究的模型和算法 ,研究一种面向 Deep W eb搜索引擎的自适应爬虫搜索算法. 在模型不确定的情况下 ,寻找满足搜索算法的优化目标的最优策略 ,达到爬虫总搜索路径最短、搜索无关页面最低等 ,并在性能上对比目前常用的几种爬虫调度算法. 参考文献 : [ 1 ]史忠植 ,董明楷 ,蒋运承 ,张海俊. 语义 W eb的逻辑基础 [J ]. 中国科学 (E辑 ) , 2004, 34 (10) : 112321138. SH I Zhongzhi, DONGM ingkai, J IANG Yuncheng, ZHANG Haijun. A logic foundation for the semantic web [ J ]. Sci2 ence in China ( Series E) , 2004, 34 (10) : 1123 - 1138. [ 2 ]BLACKBURN P, BOS J. Rep resentation and inference for natural language [ C ] / / CSL I Publications, Crysmann, Berthold, 2005. [ 3 ]BERTOSS L, SCHW IND C. Analytic tableaux and database repairs [ C ] / /Foundations of Information and Knowledge Systems. Sp ringer LNCS 2284, 2003. [ 4 ]苏开乐 ,骆翔宇 ,吕关锋. 符号化模型检测 CTL [J ]. 计算机学报 , 2005, 28 (11) : 179821806. SU Kaile, LUO Xiangyu, LU¨Guanfeng. Symbolic model checking for CTL [J ]. Chinese Journal of Computer, 2005, 28 (11) : 179821806. [ 5 ] PASKEV ICH A. Connection tableaux with lazy paramodula2 tion[C ] / / IJCAR 2006. Seattle, USA, 2005. [ 6 ]HORV ITZ E. Machine learning, reasoning, and intelligence in daily life: directions and challenges[C ] / /Proceedings of 第 4期刘全 ,等 :一种逻辑强化学习的 tableau推理方法 ·359·

·360· 智能系统学报第3卷 [ML.Bled,Slvenia,1999 作者简介： [7]BRYANT C,MUGGETON S,OL NER S Combining in- 刘全，男，1969年生教授博士后，中 ductive bgic programm ing,active leaming and robotics to 国计算机学会高级会员，主要研究方向为 discover the function of genes[J].Electronic Transactions 智能信息处理、自动推理机器学习.主持和 in A rtificial Intelligence,2001,6(12):1-36 参与国家级科研项目4项，主持省部级和 [8 ]CALZONEL,CHABR IER N,FAGES E Machine leaming 市局级科研项目10多项，获省部级科技 bimolecular interactions from temporal logic properties 进步奖2项，市侷)级科技进步奖8项发 [C ]//Proceedings of CMSB 2005.Edinburgh,Scotland, 表学术论文40余篇，其中S℃收录4篇 2005 E收录20篇. [9]TEEVAN J,HORV IIZ E Personalizing search via autma- 崔志明，男，1961年生，教授，博士 ted analysis of interests and activities[C]//Proceedings of 生导师，中国计算机学会高级会员，主 SIGR Salvador,B razil,2005:449-456 要研究方向为模式识别、Deep Weh主 [10 ]F IITNGM.First-order bgic and automated theorem pro- 持国家级及省部级科研项目18项.作 ving[M ]New York:Springer-Verlag,1996 为项目负责人完成并通过省（部）级以 [11高阳，陈世福，陆鑫.强化学习综述[J]自动化学上鉴定的项目有28项，并获国防科工报，2004,30(1)：86-100 委科技进步一等奖1项、省部级科技进 GAO Yang,CHEN Shifu,LU Xin Research on reinforce- 步二等奖2项、三等奖4项、省优秀软件奖三等奖2项：发表 ment leaming technobgy:a review [J].Acta Automatica 学术论文100余篇，其中被SCkE收录28篇，出版著（译） Sinica,2004.30(1):86-100 作13部，申请发明专利4项，获软件著作权6项. [12 ]OTTERLO M.Reinforcement leaming for relational MDPs 高阳，男，1972年生，副教授，博 [C]//Machine Leaming Conference of Belgium and the 士，中国人工智能学会理事，中国机器 Netherlands(BeNeLeam'04).[S I ]2004:138-145. 学习专业委员会常务委员，主要研究方 [13刘全，孙吉贵.基于Tableau的定理机器证明系统Tab 向为强化学习、多Agenti系统.发表学术 leau TA P[J]计算机工程，2006,32(7)：38-45 论文50余篇. LU Quan,SUN Jigui Theorem proving system based on Tab- eau TAP[J]Computer Engineering.2006,32(7):38-45 The Sno-European W orkshop on I telligent Robots and Systems (SEIROS'08) 第一届中欧智能系统及机器人国际学术研讨会第一届中欧智能系统及机器人国际学术研讨会将于2008年12月11~13日在重庆邮电大学举行.此次学术论坛是由英国Ox6d大学、英国Essex.大学、德国Hamberg大学瑞士苏黎世联邦高等工业大学等国际著名大学的智能系统及机器人技术专家发起，响应科技部关于“中欧科技年”2008年活动的建议，旨在为全球智能系统及机器人的专家、学者和工程技术人员提供一个学术交流、研讨平台和应用成果的展示平台，促进国际科技合作和学术交流征文范围：智能机器人技术、机器人感知技术、仿生机器人、受生物启发的控制技术、基于人工神经网络、模糊、遗传算法的仿生机器人技术、服务机器人、医疗手术机器人、类人机器人、多机器人协作、智能人机交互、智能信息处理、图像处理与模式识别、机电一体化、智能控制与自动化、智能复杂系统截稿日期：2008-10-10 论文录用通知日期：2008-11-10 联系人：徐晓东李敏联系电话：023-62471421 Email:seirs08@cqupt edu cn 1994-2009 China Academic Journal Electronic Publishing House.All rights reserved.http://www.cnki.net

ICML. Bled, Slovenia, 1999. [ 7 ]BRYANT C, MUGGLETON S, OL IVER S. Combining in2 ductive logic p rogramm ing, active learning and robotics to discover the function of genes[ J ]. Electronic Transactions in A rtificial Intelligence, 2001, 6 (12) : 1236. [ 8 ]CALZONE L, CHABR IER N, FAGES F. Machine learning biomolecular interactions from temporal logic p roperties [C ] / /Proceedings of CMSB 2005. Edinburgh, Scotland, 2005. [ 9 ] TEEVAN J, HORV ITZ E. Personalizing search via automa2 ted analysis of interests and activities[ C ] / /Proceedings of SIGIR. Salvador, Brazil, 2005: 4492456. [ 10 ] F ITTINGM. First2order logic and automated theorem p ro2 ving[M ]. New York: Sp ringer2Verlag, 1996. [ 11 ]高阳 ,陈世福 ,陆鑫. 强化学习综述 [J ]. 自动化学报 , 2004, 30 (1) : 862100. GAO Yang, CHEN Shifu, LU Xin. Research on reinforce2 ment learning technology: a review [ J ]. Acta Automatica Sinica, 2004, 30 (1) : 862100. [ 12 ]OTTERLO M. Reinforcement learning for relational MDPs [C ] / / Machine Learning Conference of Belgium and the Netherlands(BeNeLearn’04). [ S. l. ], 2004: 1382145. [13 ]刘全 ,孙吉贵. 基于 Tableau的定理机器证明系统 Tab2 leauTAP[J ].计算机工程 , 2006, 32 (7): 38245. L IU Quan, SUN Jigui. Theorem proving system based on Tab2 leauTAP[J ]. Computer Engineering, 2006, 32 (7) : 38 - 45. 作者简介 : 刘全 ,男 ,1969年生 ,教授 ,博士后 ,中国计算机学会高级会员 ,主要研究方向为智能信息处理、自动推理、机器学习.主持和参与国家级科研项目 4项,主持省部级和市 (局 )级科研项目 10多项 ,获省部级科技进步奖 2项,市 (局 )级科技进步奖 8项.发表学术论文 40余篇 ,其中 SCI收录 4篇 , EI收录 20篇. 崔志明 ,男 , 1961年生 ,教授 ,博士生导师 ,中国计算机学会高级会员 ,主要研究方向为模式识别、Deep W eb. 主持国家级及省部级科研项目 18项. 作为项目负责人完成并通过省 (部 )级以上鉴定的项目有 28项 ,并获国防科工委科技进步一等奖 1项、省部级科技进步二等奖 2项、三等奖 4项、省优秀软件奖三等奖 2项 ;发表学术论文 100余篇 ,其中被 SCI、EI收录 28篇 ,出版著 (译 ) 作 13部 ,申请发明专利 4项 ,获软件著作权 6项. 高阳 ,男 , 1972年生 ,副教授 ,博士 ,中国人工智能学会理事 ,中国机器学习专业委员会常务委员 ,主要研究方向为强化学习、多 Agent系统. 发表学术论文 50余篇. The Sino2European W orkshop on Intelligent Robots and System s ( SEIROS ’08) 第一届中欧智能系统及机器人国际学术研讨会第一届中欧智能系统及机器人国际学术研讨会将于 2008年 12月 11～13日在重庆邮电大学举行. 此次学术论坛是由英国 Oxford大学、英国 Essex大学、德国 Hamberg大学、瑞士苏黎世联邦高等工业大学等国际著名大学的智能系统及机器人技术专家发起 ,响应科技部关于“中欧科技年 ”2008年活动的建议 ,旨在为全球智能系统及机器人的专家、学者和工程技术人员提供一个学术交流、研讨平台和应用成果的展示平台 ,促进国际科技合作和学术交流. 征文范围 :智能机器人技术、机器人感知技术、仿生机器人、受生物启发的控制技术、基于人工神经网络、模糊、遗传算法的仿生机器人技术、服务机器人、医疗手术机器人、类人机器人、多机器人协作、智能人机交互、智能信息处理、图像处理与模式识别、机电一体化、智能控制与自动化、智能复杂系统. 截稿日期 : 2008210210 论文录用通知日期 : 2008211210 联系人 :徐晓东李敏联系电话 : 023 - 62471421 E2mail: seiros08@cqup t. edu. cn ·360· 智能系统学报第 3卷