·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.nete: = 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卷