模糊命题模态逻辑的Tableau方法

刘磊,王强,吕帅,2

(1.吉林大学 计算机科学与技术学院，吉林 长春 130012； 2.吉林大学 数学学院, 吉林 长春 130012)



模糊命题模态逻辑的Tableau方法

刘磊1,王强1,吕帅1,2

(1.吉林大学 计算机科学与技术学院，吉林 长春 130012； 2.吉林大学 数学学院, 吉林 长春 130012)

为提高模糊命题模态逻辑(fuzzy propositional modal logic, FPML)的推理能力,本文将经典模态逻辑中的Tableau方法推广到FPML中,提出了基于FPML的Tableau规则并证明了其正确性,给出了模糊断言集合的约简策略;在此基础上给出了FPML中的不一致性和不一致估值的定义。最后给出基于Tableau方法的FPML的一致性检测方法TFPML和模糊断言集合的不一致估值计算方法CID,并证明了其正确性。实例分析表明,本文提出的方法是正确有效的。

Tableau方法；模态逻辑；模糊命题模态逻辑；不确定推理；一致性检测；模糊断言集合

自动推理隶属人工智能领域,也是理论计算机科学的一个重要组成部分,主要用来进行自动定理证明,通常用来判定某个公式的有效性或可满足性,在模态逻辑、描述逻辑、时态逻辑等非经典逻辑中也有广泛应用[1-3]。模态逻辑自提出以来,研究人员针对不同的模态系统提出了很多有效的推理方法,包括模态Tableau方法、模态归结方法[4]、基于关系转换的方法[5-6]等。可能性逻辑是经典命题逻辑的扩充,是用于解决不确定知识表示和推理的逻辑,类比地在模态逻辑中,为了解决含有不确定知识的表示与推理。Hájek提出了模糊模态逻辑(fuzzy modal logic， FML),并提出了一种在模糊S5系统中的公理化方法,将模态逻辑中的等价关系对应到了FML中的不一致关系[7-8]。

命题模态逻辑(propositional modal logic， PML)是模态逻辑的一种最经典形式,模糊命题模态逻辑(fuzzy propositional modal logic， FPML)是PML的推广。FPML是在PML的基础上加入了隶属度因子n,对于后者而言，n∈{0,1}；对于前者，n∈[0,1]。目前,基于FPML的推理方法大多使用演绎方法。Tableau方法是一种完备的推理方法[9-11],且在经典逻辑与非经典逻辑的知识表示与推理过程中应用广泛。在国内,刘全等提出了一种基于布尔剪枝的多值广义量词Tableau推理规则简化方法,对含广义量词(交和并)规则的简化方法进行研究,建立了一套含广义量词的一阶多值逻辑公式的简化Tableau推理方法,该方法将传统的Tableau方法基础上,简化了一阶多值逻辑公式中的规则,提高了推理效率[12]。刘大有等结合冲突技术和矛盾学习技术实现了针对模态系统S4的推理机S4P,且效率优于著名的描述逻辑求解器RACER和FACT++[13],S4P中包含两种Tableau算法优化技术，即冲突技术和矛盾学习技术,冲突技术利用否定范式的冲突来确定公式集的不一致性,而矛盾学习技术利用增加的矛盾原因集来减少节点的扩展,这是Tableau方法在经典模态系统S4中的成功运用。在国外也有很多基于Tableau方法的改进和推广,Tao等提出一种PSPACE Tableau算法,对描述逻辑进行了扩展,在其中增加了多模态逻辑K(m)和S4(m)中的模态算子[14],极大地提高了描述逻辑的表达能力。Hidalgo-Doblado等提出了一种基于描述逻辑的形式校验的Tableau算法[15],详细说明了基于Tableau算法的规则应用与分支选择策略,提高了描述逻辑ALC的推理效率。因此将Tableau方法加以推广应用在FPML推理中有益于Tableau方法的更进一步深入研究与应用。

非经典逻辑的描述和表示较为复杂,多用Tableau方法来进行求解或证明,如经典模态逻辑和经典描述逻辑中Tableau方法的使用尤为广泛。但是有关FPML的Tableau方法及其对应的推理规则在国内外未见报到,因此本文将经典模态逻辑中的Tableau方法推广到FPML中,可以用来对不同模态逻辑的不确定知识进行表示和预测,以及不确定性知识库的一致性判定等。本文提出基于FPML的Tableau规则,给出模糊断言集合的约简策略;在此基础上给出FPML中的不一致性和不一致估值的定义;最后给出基于Tableau方法的FPML一致性检测方法和模糊断言集合的不一致估值计算方法,并证明其正确性。

1 模糊关系

对于一个模糊断言,它的模糊度量值表示该PML公式成立的程度,是对PML公式进行模糊化处理的结果。对模糊Kripke模型中的等价关系R进行模糊化处理得到模糊关系,用以描述当前可能世界ω和其相邻可及世界υ的等价关系成立的程度。

定义1 FPML中的模糊关系表示为一个有序对[(ω,υ):R,η],其中(ω,υ):R表示可能世界ω和可能世界υ具有等价关系,η为模糊关系的模糊度量值,表示可能世界ω及可能世界υ具有等价关系的程度。

引理1 设ω是当前可能世界,υ是ω的相邻可及世界,τ是υ的相邻可及世界,且满足ω和υ的模糊关系为[(ω,υ):R,η1],υ和τ的模糊关系为[(υ,τ):R,η2],则有:[(ω,υ):R,η1],[(υ,τ):R,η2] iff [(ω,τ):R,η3]且η3=η1×η2。

证明:

充分性。根据已知条件,可知ω、υ、τ在同一条可达世界路径上,因为[(ω,τ):R,η3]成立且R为等价关系(自反,传递,对称),所以对于可达路径上的ω和υ、υ和τ也有等价关系;由于ω和τ的模糊关系大小η3是由ω和υ的模糊关系与υ和τ的模糊关系共同决定的,所以η3=η1×η2。

必要性。已知有[(ω,υ):R,η1],[(υ,τ):R,η2]成立,且R为等价关系(自反、传递、对称),因此ω和τ也存在R关系,容易知道ω,υ,τ在同一条可达世界路径上,ω和υ具有等价关系的程度、υ和τ具有等价关系的程度二者共同决定了ω和τ具有等价关系的程度,因此有[(ω,τ):R,η3]成立,且η3=η1×η2。

证毕。

定理1 若一条可能世界的路径序列为ω1,ω2,… ,ωn,且相邻的两个可能世界均存在等价关系,则:

[(ω1,ω2):R,η1],[(ω2,ω3):R,η2],…,[(ωn-1,ωn):R,ηn-1] iff [(ωi,ωj):R,ηi×…×ηj-1](i

由引理1容易得证,在此不赘述。

例1 假设图1中的条件成立,ω是当前可能世界,υ1、υ2、υ3是ω的三个相邻可及世界,τ1、τ2是υ1的两个相邻可及世界,τ3、τ4、τ5是υ2的三个相邻可及世界。它们之间的模糊关系表示如下

[(ω,υ1):R,0.2],[(ω,υ2):R,0.4],[(ω,υ3):R,0.6],[(υ1,τ1):R,0.1],[(υ1,τ2):R,0.3],[(υ2,τ3):R,0.5],[(υ2,τ4):R,0.7],[(υ2,τ5):R, 0.9]

根据定理1可知,图1中所有的可达路径序列为(ω,υ1,τ1),(ω,υ1,τ2),(ω,υ2,τ3),(ω,υ3,τ4),(ω,υ2,τ5),(ω,υ3),除已知的模糊关系外,可以计算出如下可达世界的模糊关系:

[(ω,τ1):R,0.02],[(ω,τ2):R,0.06],[(ω,τ3):R,0.2],[(ω,τ4):R,0.28],[(ω,τ5):R,0.36]

图1 可能世界及其模糊关系Fig.1 The possible worlds and their fuzzy relations

事实上,由于等价关系的性质,只要给定了相邻的可能世界的模糊度量值,可以求得该路径序列上任意2个可能世界的模糊关系的模糊度量值。模糊断言集合事实上可以通过约简策略来进行约简。模糊关系的定义与模糊断言的定义相似,只是模糊关系的有序对的前半部分用来描述可能之间的等价关系,而模糊断言的有序对的前半部分用来描述命题模态公式,因此模糊关系中也可以使用约简策略,如例1中,因为所描述是在模态S5系统下的FPML,因此R一定为等价关系,而由[(υ1,τ1):R,0.1]可以得到[(τ1,υ1):R,0.1],由[(ω,τ1):R,0.02]和[(τ1,υ1):R,0.1]可以得到[(ω,υ1):R,0.002]。需要强调的一点是:[(ω,υ1):R,0.002]与[(ω,υ1):R,0.2]并不矛盾,通过约简规则可以由[(ω,υ1):R,0.2]将[(ω,υ1):R,0.002]删除。在可能性逻辑中,若两个命题公式成立的程度不一致时,可能性高的断言可以约简掉可能性低的断言。在计算过程中,若出现从后继世界来逆推模糊度量值时,会导致模糊度量值趋近于0,因此只考虑从前一个世界向其后继世界的计算。

定理2 在一个模糊关系集合中,若存在模糊关系[(ω,υ):R,α]与[(ω,υ):R,β],α和β是关于ω和υ的模糊关系的模糊度量值,且α≠β,则可以将模糊度量值较小的模糊断言删除,即用<φ,max(α,β)>替换<φ,α>和<φ,β>。

证明: 在可能性逻辑中,当α≥β时,有(φ,α)├(φ,β)[16]。在此,可以将ω和υ具有等价关系当作一个命题p,且该命题是二值的,当α≥β时,等同于可能性逻辑中,可得(p,α)├(p,β),定理得证。

2 扩展Tableau规则

本节结合传统的模态逻辑中使用的Tableau规则给出了在FPML中的基本推理规则以及在推理过程所使用到的约简策略,利用Tableau规则可以对给定的模糊断言集合中的模糊断言进行处理。

2.1 推理规则

∧-规则:即模态逻辑中的α规则的推广,公式φ∧ψ成立的程度决定公式φ和公式ψ分别成立的程度,形式地:

∨-规则:即模态逻辑中的β规则的推广,若公式φ∨ψ成立的程度为α,则公式φ成立的程度为α或公式ψ成立的程度为α,形式地:

□-规则:对于含必然算子的命题模态公式而言,它的模糊断言和所在世界与后继可能世界的模糊关系共同决定它在后继可能世界的模糊断言的形式,且后继可能世界中的模糊度量值为当前世界的模糊度量值与模糊关系的最小值,形式地:

◇-规则:对于含有可能算子的模态公式而言,若在后继可能世界中,不存在模糊断言和模糊关系使得它们的模糊度量值都大于当前世界的可能性估值,则可以用当前世界的模糊度量值代替它们的模糊度量值,形式地:

ζ表示存在一个υ使得有<υ:φ,β>,[(ω,υ):R,γ],且min(β,γ)≥α。

在使用◇-规则时,必须保证在可能世界υ中,模糊断言<υ:φ,β>和模糊关系[(ω,υ):R,γ]的可能性度量至少有一个比α小,这样在可能世界υ中推导出来的模糊断言α大于β或者γ。

()

⊥-规则:若两个模糊断言有冲突,可以用一个模糊断言来替换,其公式部分为⊥,模糊度量值为约简前的两个模糊断言的模糊度量值的最小值,形式地:

相比较于其他规则,◇-规则比较难以理解,在此给出证明过程。

定理3 ◇-规则是正确的。

证明: 使用反证法来进行证明,假设ζ成立,那么在可能世界υ中,有模糊断言<υ:φ,β>和模糊关系[(ω,υ):R,γ],且min(β,γ)≥α,根据引理2,可以用<υ:φ,β>替换掉<υ:φ,α>,即所推导出的<υ:φ,α>是无效的。所以假设不成立,◇-规则是正确的。

证毕。

2.2 约简策略

在FPML中使用Tableau方法时,终止条件为推导出冲突或不能再使用表规则进行推演。下面给出FPML中的冲突定义。

定义2Σ是模糊断言集合,φ为任意的PML公式,若∑中同时包含如下两个模糊断言:

<φ,α>,<φ,β>

称Σ包含一个冲突⊥,若Σ中存在冲突,那么Σ是不一致的,利用冲突规则可以将两个冲突的模糊断言约简为一个模糊断言,即<⊥,min(α,β)>。

根据文献[16]可以得到如下定义:

定义3Σ是模糊断言集合,Σ的不一致性估值为

Inc(Σ)=max{α|Σ╞<⊥,α>}

定义4 设Σ1=<φ∨ψ,α>∪Σ,Σ2=<φ,α>∪Σ,Σ3=<ψ,α>∪Σ,则有

Inc(Σ1)=min(Inc(Σ2),Inc(Σ3))

通过FPML的不一致性定义,可以在对FPML使用Tableau方法推理时,计算产生冲突的不一致估值,因为使用Tableau方法进行推理时,一定是通过使用表规则推导出冲突或者不能再使用表规则而终止,因此当推导出冲突的时候,一定可以计算出Σ的不一致估值,由此可以对所要处理的模糊断言集合进行一致性检测。

模态逻辑使用Tableau方法进行推理时,因为所要构造的Tableau有限树过于复杂,经常会增加一些剪枝策略来加快求解,快速判断有限树的某个分支是否含有冲突,从而得到模态公式的可满足性。FPML是PML的推广,它在PML的基础上增加了模糊度量值表示某个PML公式在可能世界中有效的程度,模糊度量值的加入使得模糊断言集合的规模急剧增长,因为在模糊断言集合中,同一个公式可能会有不同的度量值,也就是说存在两个模糊断言,它们的PML公式部分相同,而模糊度量值部分不同。在推理过程中,可以使用一些相应的约简策略来对模糊断言集合进行约简,从而减少模糊断言集合的规模。

引理2 若在模糊断言集合中同时存在模糊断言<φ,α>和<φ,β>,φ是任意的模态公式,α和β是公式φ的模糊度量值,且α≠β,则可以将模糊度量值较小的模糊断言删除,即用<φ,max(α,β)>替换<φ,α>和<φ,β>。

证明: 在可能性逻辑中,当α≥β时,有(φ,α)├(φ,β)[16]。FPML中将可能性逻辑中的命题公式换成了PML公式,下面证明对于PML公式来说,也有这样的性质存在:

1)若PML公式为φ,当φ不含模态算子时,φ是命题公式,上述性质显然成立。

2)若PML公式为□φ,根据T公理可知,在当前世界ω上述性质成立;φ在后继可能世界υ中模糊度量值是由φ在当前世界ω的度量值以及ω与υ的模糊关系共同决定的,而针对于<□φ,α>和<□φ,β>而言,当前世界ω与后继可能世界υ的模糊关系一定是相同的,因此α和β的偏序关系在所有的后继世界中都不会改变,因此对于模态公式□φ来说,上述性质是成立的。

3)若PML公式为◇φ,其在模态逻辑下的定义是存在某个与当前世界相邻的后继可能世界使得φ成立,因此只考虑在可能世界υ中的情况,根据◇-规则,当满足其使用条件时,有如下替换成立:

对于<◇φ,α>和<◇φ,β>,在可能世界υ中,α和β的偏序关系也不会发生改变,因此上述性质成立。

证毕。

例2 已知Σ={<ω:□φ,0.8>,<ω:□φ,0.6>},在当前世界ω中,<φ,0.8>,<φ,0.6>一定成立,可以进行约简,满足性质;当ω与υ的模糊关系为[(ω,υ):R,0.3]时,在可能世界υ中有<υ:φ,0.3>,两者在可能世界υ中的映射是相同的;而当ω与υ的模糊关系为[(ω,υ):R,0.9]时,则在可能世界υ中有<υ:φ,0.8>,<υ:φ,0.6>,两者在可能世界υ中的映射偏序关系保持不变;而当ω与υ的模糊关系为[(ω,υ):R,0.7]时,则在可能世界υ中有<υ:φ,0.7>,<υ:φ,0.6>,两者在可能世界υ中的映射偏序关系仍保持不变,所以通过引理2可以将∑约简成∑′={<ω:□φ,0.8>}。

推论1 若在∑中同时存在模糊断言<φ→ψ,α>和<φ,β>,可以用<ψ,min(α,β)>替换<φ→ψ,α>。

此推论又可看作是MP规则在FPML中的推广,也类似于可能性逻辑中提到的归结方法[16],因为φ→ψ与φ∨ψ是等价的,其证明过程与归结方法的证明过程类似,在此不赘述。

应用以上引理和推论可以对要处理的模糊断言集合进行预处理,删除掉一些不必要的模糊断言,从而降低模糊断言集合的规模,对剩余模糊断言使用Tableau方法求解,尽快找到冲突,计算模糊断言集合的不一致性。

3 模糊断言集合的一致性检测

文中提到针对模态逻辑的理论研究一般是在模态系统中进行的,不同的模态系统的性质又各不相同[16],在S5公理系统中,可以使用S5规约定理。

定理4[17](S5规约定理)在S5系统中,对于任意的模态公式,若其模态词的嵌套层数大于1,则可以对其进行规约,使得公式的模态词的个数不大于1,从而大大降低了公式复杂度和规模。

本文的所有推理过程都是在模糊S5系统中进行的,对模糊断言集合中的任一模糊断言,都可以使用规约定理对其PML公式部分进行归约,使公式的模态度小于或等于1。设模糊断言集合为Σ={Δ1,Δ2，… ,Δn},Δn表示n个模糊断言。约简策略的集合为RED={R1,R2},R1和R2分别为

表规则集合为RT={R∧,R∨,R□,R◇,R,R⊥}。下面给出关于模糊断言集合∑一致性检测的过程的形式化描述:

Procedure TFPML(Tableau in fuzzy proposition modal logic)

1)输入:模糊断言集合Σ={Δ1,… ,Δn}

2)IfΣ=Ø Then return consistent

3)While ∑不含有冲突 do

While 可以用规则集RED依次化简Σdo 用RED化简Σ

EndWhile

If 不 能用表规则集合RT对Σ进行推演

Then return consistent

Else 用表规则集合RT对Σ进行推演

将被约简的模糊断言放入集合Σ1

Σ=Σ-Σ1

将新推导出的模糊断言放入集合Σ2

Σ=Σ∪Σ2

EndIf

EndWhile

4) return inconsistent

定理5 过程TFPML是正确完备的。

证明:若Σ=Ø,Σ是一致的,在第二行返回consistent,否则判断Σ是否含有冲突。若Σ含有冲突,则Σ是不一致的,退出循环,返回inconsistent,否则使用规则集RED对Σ进行化简,引理2和推论1保证了RED化简的正确性。若对Σ使用表规则的过程中产生了冲突,那么Σ一定是不一致的,退出循环,返回inconsistent,否则对Σ循环使用表规则集RT,直到不能使用RT为止,若此时仍没有产生冲突,那么Σ是一致的,返回consistent。Tableau方法在使用Tableau规则时,每一步都可以给出对应的树结构,在推理树中,叶节点都是原子的,即在此处不能再使用Tableau规则。因此算法一定会终止。

证毕。

对于任意给定的模糊断言集合Σ,都可以使用TFPML方法对Σ进行一致性检测,若Σ是不一致的,往往需要给出不一致性估值来表示其不一致程度。下面给出一致性检测的一致性估值的计算方法过程的形式化描述:

Procedure CID(computing the Inconsistent degree)

1)输入:模糊断言集合Σ={Δ1,Δ… ,Δn}

2)While 可以用规则集RED依次化简Σdo

用RED化简Σ

EndWhile

3)While 可以用表规则集合RT对Σ进行推演 do

用表规则集合RT对Σ进行推演

将被约简的模糊断言放入集合Σ1

Σ=Σ-Σ1

将新推导出的模糊断言放入集合Σ2

Σ=Σ∪v2

While 可以用规则集RED依次化简Σdo

用RED化简Σ

Endwhile

EndWhile

4)IfΣ含有冲突

Then return 冲突模糊断言的模糊度量值

Else return 0

CID与TFPML的思想基本相同,TFPML只要归约出冲突,立即退出循环,并返回inconsistent;而CID为了要计算不一致估值,需要对Σ不断地使用表规则集RT,直到不能使用表规则集RT为止,并在使用表规则集RT的同时使用规则集RED对Σ进行归约,若包含多个冲突模糊断言,则归约过后只会留下模糊度量值最大的冲突断言。最后进行判断,若有冲突,则返回冲突模糊断言的模糊度量值,即不一致估值,否则返回0。因此,计算不一致估值的方法CID也是正确完备的。

4 实例分析

本文将可能性逻辑中的不一致定义和不一致估值计算方法扩展到了FPML中,给出了模糊断言集合的不一致性定义及其不一致估值的计算方法,提出了基于Tableau方法的FPML一致性检测方法TFPML和不一致估值计算方法CID,并在两种方法的过程中加入了约简策略,验证了约简策略和所提出方法的正确完备性,约简策略有利于及时地对模糊断言集合进行约简,能够提高推理效率。

FPML是PML的并不像模态逻辑和命题逻辑那样有标准的Benchmark问题[18],尚未出现关于FPML的模糊断言测试集,因此本文基于模糊描述逻辑中的实例[19],构造了FPML的实例,通过实例来演示推理过程,同时也进一步验证了该计算方法的正确性。由于CID与TFPML的思想基本相同,TFPML只要归约出冲突,立即退出循环,并返回inconsistent;而CID为了要计算不一致估值需要返回的是确定的模糊度量值,因此本文仅给出CID方法的过程。首先给出一个简单的例子。

例3Σ={<φ,0.3>,<φ,0.1>,<ψ,0.5>,<φ→ψ,0.2>},计算该模糊断言集合的不一致估值。

1)使用RED规则集的R1对Σ进行约简,根据引理2,可以删除<φ,0.1>,约简后的模糊断言集合Σ={<φ,0.3>,<ψ,0.5>,<φ→ψ,0.2>}。

2)使用RED规则集的R2对Σ进行约简,根据推论1,可以用<ψ,0.2>代替<φ→ψ,0.2>,约简后的模糊断言集合Σ={<φ,0.3>,<ψ,0.5>,<ψ,0.2>}。

3)新增加的<ψ,0.2>与<ψ,0.5>产生冲突,使用R⊥规则得到<⊥,0.2>,约简后的模糊断言集合Σ={<φ,0.3>,<⊥,0.2>}。

4)此时不可以再使用表规则集RT对模糊断言集合Σ进行约简,也不能使用RED规则集对Σ进行约简,Σ中有冲突,所以Σ是不一致的,且Σ的不一致估值为0.2,即Inc(Σ)=0.2。

下面考虑一个更为复杂的例子。

例4 设Σ={<ω:φ,0.3>,<ω:φ,0.1>,<ω:ψ,0.5>,<ω:□φ,0.6>,<ω:φ→ψ,0.2>,<ω:□□φ,0.3>,<υ:□◇(φ∧χ),0.4>,<υ:◇(φ∧ψ),0.2>,<ω:◇◇(φ∧ψ),0.8>,<ω:◇(φ∧ψ),0.8>},υ为ω的相邻可及世界,计算Σ的不一致估值。

1)使用RED规则集的R1对Σ进行约简,由于本文所处理的模态公式都是默认在S5系统中的,因此<ω:□□φ,0.3>与<ω:□φ,0.3>等价、<υ:□◇(φ∧χ),0.4>与<υ:◇(φ∧χ),0.4>等价、<ω:◇◇(φ∧ψ),0.8>与<ω:◇(φ∧ψ),0.8>等价,因此根据引理2,可以删除<ω:φ,0.1>,<ω:□□φ,0.3>,<υ:◇(φ∧ψ),0.2>,<ω:◇◇(φ∧ψ),0.8>,约简后的模糊断言集合为:Σ={<ω:φ,0.3>,<ω:ψ,0.5>,<ω:□φ,0.6>,<ω:φ→ψ,0.2>,<υ:◇(φ∧ψ),0.4>,<ω:◇(φ∧ψ),0.8>}。

2)使用RED规则集的R2对Σ进行约简,根据推论1,可以用<ψ,0.2>代替<φ→ψ,0.2>,约简后的模糊断言集合为Σ={<ω:φ,0.3>,<ω:ψ,0.5>,<ω:□φ,0.6>,<ω:ψ,0.2>,<υ:◇(φ∧χ),0.4>,<ω:◇(φ∧ψ),0.8>}。

3)新增加的<ω:ψ,0.2>与<ω:ψ,0.5>产生了冲突,使用R⊥规则得到<ω:⊥,0.2>,约简后的模糊断言集合为Σ={<ω:φ,0.3>,<ω:□φ,0.6>,<ω:⊥,0.2>,<υ:◇(φ∧χ),0.4>,<ω:◇(φ∧ψ),0.8>}。

4)对于模糊断言<ω:◇(φ∧ψ),0.8>,由于在可能世界υ中,并不存在<υ:φ,β>,[(ω,υ):R,γ],且min(β,γ)≥0.8,因此ζ条件不成立,可以使用R◇规则,得到<υ:(φ∧ψ),0.8>,[(ω,υ):R,0.8]。假设υ的下一可能世界为τ,在可能世界τ中ζ条件也不成立,同理<υ:◇(φ∧χ),0.4>使用R◇规则得到<τ:(φ∧χ),0.4>,[(υ,τ):R,0.4],约简后的模糊断言集合为Σ={<ω:φ,0.3>,<ω:□φ,0.6>,<ω:⊥,0.2>,<τ:(φ∧χ),0.4>,<υ:(φ∧ψ),0.8>}。模糊关系集为

Г={[(ω,υ):R,0.8], [(υ,τ):R,0.4]}。

5)继续使用表规则集合RT对模糊断言集合Σ进行推演,<υ:(φ∧ψ),0.8>使用R∧规则得到<υ:φ,0.8>,<υ:ψ,0.8>,<τ:(φ∧χ),0.4>使用R∧规则得到<τ:φ,0.4>,<τ:χ,0.4>,此时模糊断言集合为Σ={<ω:φ,0.3>,<ω:□φ,0.6>,<ω:⊥,0.2>,<τ:φ,0.4>,<τ:χ,0.4>,<υ:φ,0.8>,<υ:ψ,0.8>}。模糊关系集为Г={[(ω,υ):R, 0.8],[(υ,τ):R,0.4]}。

6)对于模糊断言<ω:□φ,0.6>,使用R□规则得到<υ:φ,0.6>,而<υ:φ,0.6>与<υ:φ,0.8>使用R⊥规则得到<υ:⊥,0.6>,此时模糊断言集合为:Σ={<ω:φ,0.3>,<ω:⊥,0.2>,<τ:φ,0.4>,<τ:χ,0.4>,<υ:⊥,0.6>,<υ:ψ,0.8>}。模糊关系集为

Г={[(ω,υ):R,0.8],[(υ,τ):R,0.4]}。

7)此时,对于模糊断言集合Σ不可以再使用表规则集RT对模糊断言集合Σ进行约简,也不能使用RED规则集对Σ进行约简,Σ中有冲突,所以Σ是不一致的,且Σ的不一致估值为所有冲突断言中最大的模糊度量值,即Inc(Σ)=0.6。

例3、4表明,对任意给定的有限的模糊断言集合,都可以通过扩展Tableau规则对其进行推演,且可以判断模糊断言集合的一致性。若给定的模糊断言集合是不一致的,还可以通过CID方法计算出模糊断言集合的不一致估值,即该集合的一致性程度,它描述了该集合有效的程度。

5 结论

1)扩展的Tableau规则可以应用于FPML,且在推理过程加入约简策略可以较为高效地处理模糊断言集中的不一致问题。

2)TFPML和CID是正确有效的,同时为Tableau方法在其他非经典逻辑或混合逻辑中的应用奠定了基础。

[1]GOLISKA-PILAREK J, MUOZ-VELASCO E, MORA A. Deterministic tableau-decision procedure via reductions for modal logic K[J]. Advances in intelligent systems and computing, 2014, 239: 429-438.

[2]SCHMIDT R A, TISHKOVSKY D. Using tableau to decide description logics with full role negation and identity[J]. ACM transactions on computational logic, 2012, 15(1): 136-156.

[3]REYNOLDS M. A tableau for temporal logic over the reals[J]. Advances in modal logic, 2014, 10: 439-458.

[4]NALON C, DIXON C. Clasusal resolution for normal modal logics[J]. Journal of algorithms, 2007, 62: 117-134.

[5]ANGELO M, ALBERTO P, MATTEO S. Alternative translation techniques for propositional and first-order modal logics [J]. Journal of automated reasoning, 2002, 28(4): 397-415.

[6]MARK K, TOBIAS T. InKreSAT: Modal reasoning via incremental reduction to SAT[C]∥Proceedings of the 24th International Conference on Automated Deduction, Lake Placid, USA, 2013, 436-442.

[9]刘全,崔志明,高阳,等.一种逻辑强化学习的tableau推理方法[J].智能系统学报,2008,3(4):355-360.

LIU Quan, CUI Zhiming, GAO Yang, et al. Tableau reasoning method based on logical reinforcement learning [J]. CAAI transactions on intelligent systems, 2008, 3(4): 355-360.

[10]郝国舜,马世龙,眭跃飞.一种扩展的动态描述逻辑语言及其Tableau算法[J].智能系统学报,2009,4(3):226-233.

HAO Guoshun, MA Shilong, SUI Yuefei. An extended dynamic description logic language and its Tableau algorithm[J]. CAAI transactions on intelligent systems, 2009, 4(3): 226-233.

[11]郭新峰,马世龙,吕江花,等.扩展断言知识检验一致的需求建模方法[J].智能系统学报,2015,10(1):81-90.

GUO Xinfeng, MA Shilong, LYU Jianghua, et al. Extension abox requirements modeling method[J]. CAAI transactions on intelligent systems, 2015, 10(1): 81-90.

[12]刘全,孙吉贵,崔志明.基于布尔剪枝的多值广义量词Tableau推理规则简化方法[J].计算机学报,2005,28(9):1514-1518.

LIU Quan, SUN Jigui, CUI Zhiming. A method of simplifying many-valued generalized quantifiers Tableau rules based on boolean pruning[J]. Chinese journal of computers, 2005, 28(9): 1514-1518.

[13]刘大有,赖永,王生生.Tableau算法的优化及模型规约技术[J].计算机学报, 2014, 37(8): 1647-1657.

LIU Dayou, LAI Yong, WANG Shengsheng. Techniques about optimizing Tableau algorithm and reducing models[J]. Chinese journal of computers, 2014, 37(8): 1647-1657.

[14]TAO J, SLUTZKI G, HONAVAR, V. PSPACE Tableau algorithms for acyclic modalized ALC[J]. Journal of automated reasoning, 2012, 49(4): 551-582.

[15]HIDALGO-DOBLADO M J, ALONSO-JIMÉNEZ J A, BORREGO-DAZ J, et al. Formally verified Tableau-based reasoners for a description logic[J]. Journal of automated reasoning, 2014, 52(3): 331-360.

[16]DUBOIS D, LANG J, PRADE H. Possibilistic logic [C]// In: GABBAY D, HOGGER C J, ROBINSON J A (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming. New York: Oxford University Press, 1994: 439-513.

[17]周北海. 模态逻辑导论[M]. 北京：北京大学出版社, 1997: 69-102.

ZHOU Beihai. Modal logic: an introduction[M]. Beijing: Peking University Press, 1997: 69-102.

[18]BALSIGER P, HEUERDING A, SCHWENDIMANN S. A benchmark method for the propositional modal logics K, KT, S4[J]. Journal of automated reasoning, 2000, 24(3): 297-317.

[19]STRACCIA U. Reasoning within fuzzy description logics[J]. Journal of artificial intelligence research, 2001, 14(1): 137-166.

本文引用格式：

刘磊,王强, 吕帅. 模糊命题模态逻辑的Tableau方法[J]. 哈尔滨工程大学学报， 2017， 38(6)： 914-920.

LIU Lei， WANG Qiang， LYU Shuai. Tableau approach of fuzzy propositional modal logic[J]. Journal of Harbin Engineering University， 2017， 38(6)： 914-920.

Tableau approach of fuzzy propositional modal logic

LIU Lei1， WANG Qiang1， LYU Shuai1,2

(1.College of Computer Science and Technology, Jilin University, Changchun 130012, China; 2.College of Mathematics, Jilin University, Changchun 130012, China)

In order to improve the reasoning ability of fuzzy propositional modal logic (FPML), we propose a tableau approach to FPML, including a reduction strategy and tableau rules based on FPML. We also propose a method known as tableau approach of fuzzy propositional modal logic (TFPML) to check the consistency of FPML, and a computing method known as CID to determine the degree of inconsistency of a fuzzy assertion set. The soundness and completeness of these two methods are proven, and their correctness and effectiveness are illustrated.

Tableau approach; modal logic; fuzzy propositional modal logic; uncertainty reasoning; consistency checking

2016-03-23. 网络出版日期：2017-03-30.

国家自然科学基金项目(61300049，61402195)；教育部高等学校博士学科点专项科研基金项目(20120061120059)；吉林省科技发展计划项目(20130206052GX，20140520069JH).

刘磊(1960-), 男, 教授, 博士生导师； 吕帅(1981-), 男, 副教授.

吕帅，E-mail：lus@jlu.edu.cn.

10.11990/jheu.201603080

http://www.cnki.net/kcms/detail/23.1390.u.20170330.0957.010.html

TP181

A

1006-7043(2017)06-0914-07