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