第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卷
第4期 刘全，等：一种逻辑强化学习的tab leau推理方法 ·359· 赋值，那么必然有分枝B'∈S,o,且M.)卡B! 作为推理机的实际应用系统中 根据Y公式的定义，有B卡r°((x)… 4结束语 (付，)中，1≤≤p使得Bo卡r°{（付x)…(付品） 中，0}，即M,以卡中o,这里Φ={(x)…(x,) 本文提出了将逻辑强化学习用于tableau推理 中，1≤≤p时，因为o,P,P})为中的反驳，使 的方法，对处理tab leau推理的盲目性具有一定的价 值.但该研究只是相关研究的开端，正在研究和将要 得中o卡Γp,V…VP,对于某一j∈1，k,必 有M,以卡P,即M满足S,+1中的分枝BoUP, 研究的内容主要包括以下几方面：I)拟采用tableau 推理模型对逻辑状态和逻辑活动进行建模，研究一 证毕 种新的函数估计模型，使其一方面能够以任何精度 定理2如果对于公式中存在一个tableau抽 逼近理论的强化学习值函数，另一方面在增量环境 象状态证明序列{{门中}}=S,S,S.1,Sn=0 中保证收敛性.2)拟将布尔剪枝、P-tableau等方法 (n≥0)，那么Φ是一个重言式. 证明中是『不可满足的，那么根据引理1，T 与逻辑强化学习相结合，对逻辑状态空间模型进行 相应的等价转换，采用解线性方程组的方式来简化 也是「不可满足的，依次类推，Sn1,S,S。是「- 状态空间，降低状态空间维数，解决大规模、连续的 不可满足的.这样，第1个tableau{门中}也是T- MDP问题.在tetris问题中，试验所设计的强化学习 不可满足的，即门中是「不可满足的，这等价于中 框架和算法，并对比收敛速度.3)结合所研究的模 是「不可满足的.证毕 型和算法，研究一种面向Deep Web搜索引擎的自 3实验结果 适应爬虫搜索算法.在模型不确定的情况下，寻找满 足搜索算法的优化目标的最优策略，达到爬虫总搜 将基于逻辑强化学习的tableau方法应用于 索路径最短、搜索无关页面最低等，并在性能上对比 TableauTAP系统I]中，在W indows环境下，应用 目前常用的几种爬虫调度算法， SW HPROLOG语言对该系统进行了实现，主要是将 基于强化学习的tableau过程自动生成Prolog程序， 参考文献： 并与原系统中的推理规则相结合，形成一个可运行 [1]史忠植，董明楷，蒋运承，张海俊.语义Wcb的逻辑基础 的推理程序.应用改进后的系统对TPTP自动推理 [J].中国科学(E辑)，2004,34(10)：1123-1138 测试库中的400个问题进行了证明，并与原系统进 SHI Zhongzhi,DONGM ingkai J ANG Yuncheng,ZHANG 行了对比，结果见表2 Haijun A logic foundation for the semantic web [J].Sci ence in China(Series E),2004,34(10):1123-1138 表2TPTP中定理的证明结果对比表 [2 ]BLACKBURN P,BOS J.Representation and inference for Table 2 The theorem provng results contrast n TPTP natural language [C]//CSLI Publications,Crysmann, VaLm 测试封闭分CU时 占内存空 Berthold,2005. 算法 限定次数封闭分枝数枝数间/s间bye [3 ]BERTOSS L.SCHW ND C Analytic tableaux and database 改进TableauTAP 982 1354 457 123243 9512 repairs[C]//Foundations of Infomation and Knowledge Systems Springer LNCS 2284,2003 原TableauTAP1S60 102305020845891 205422 [4苏开乐，骆翔宇，吕关锋.符号化模型检测CL[J]计算 机学报，2005,28(11)：1798-1806 从表2中可以看出，改进后的TableauTA P的几 SU Kaile,LUO Xiangyu,LU'Guanfeng Symbolic model 项指标均优于原系统，尤其是在CU时间方面，由 checking for CIL [J ]Chinese Joumal of Computer,2005, 于TableauTAP具有学习功能，后继的证明可以学习 28(11):1798-1806 到前面的证明结论，因此运行速度要比原系统高得 [5 PASKEV CCH A.Connection tableaux with lazy paramodula- 多.同时由于该方法的普遍性，使得编程时不需要针 tion[C]//DCAR 2006 Seattle,USA,2005. 对不同的逻辑系统考虑太多的情况，使得程序代码 [6 ]HORV IIZ E Machine leaming,reasoning,and intelligence 比其他的系统要小得多，也更容易应用到自动推理 in daily life:directions and challenges[C]//Proceedings of 1994-2009 China Academic Journal Electronic Publishing House.All rights reserved.http://www.cnki.net
赋值 ,那么必然有分枝 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卷