·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卷