格值一阶逻辑系统的α广义归结原理

许伟涛,张闻强,徐 扬,张德贤

(1.河南工业大学信息科学与工程学院,河南郑州 450001; 2.西南交通大学数学学院,四川成都 610031)

格值一阶逻辑系统的α广义归结原理

许伟涛1,张闻强1,徐 扬2,张德贤1

(1.河南工业大学信息科学与工程学院,河南郑州 450001; 2.西南交通大学数学学院,四川成都 610031)

在基于格蕴涵代数的格值逻辑系统框架下,笔者扩展了基于格值逻辑系统的α归结原理,将广义子句集上的归结扩展到一般广义子句集上,提出了基于格值一阶逻辑系统LF(X)的α广义归结原理,建立了格值一阶逻辑系统中α广义归结原理的可靠性定理.通过给出的提升引理,证明了该原理的弱完备性定理.这将为建立基于格值逻辑系统的广义归结方法提供新的自动推理技术.

格值一阶逻辑;一般广义子句;局部极复杂广义文字;广义归结;自动推理

自动推理是人工智能领域的重要研究内容.基于归结原理的自动推理是自动推理研究的重要方法. Robinson于1965年提出了基于经典逻辑的归结原理[1],为基于归结原理的自动推理提供了重要的研究基础.之后,自动推理的研究也取得了较多的研究成果[2-9].

基于经典二值逻辑的归结自动推理理论,已形成各种各样的归结自动推理方法,典型的有语义归结、锁归结和线性归结.这些归结方法在证明定理时要将定理的否定写成一阶逻辑中的公式,再把公式化成Skolem标准型,然后将标准型的母式化为合取范式,而合取范式中的每一项都是一个子句,把该合取范式对应一个子句集,即只需证明这个子句集是不可满足的,就相当于完成了该定理的证明[8].为更自然、直观地对问题描述形成的公式所对应的子句集进行归结,王湘浩和刘叙华将传统的归结原理推广到广义子句集上,提出了基于经典二值逻辑的广义归结原理[8],使得演绎过程更加接近自然推导.

对确定性问题可以用经典二值逻辑解决,但是在处理含不确定性信息或知识时,问题的解决往往是困难的.为处理带有不确定性或不可比较性的信息,徐扬结合格和蕴涵代数提出了格蕴涵代数的概念[10],随后徐扬等建立了基于格蕴涵代数的格值命题逻辑系统LP(X)和格值一阶逻辑系统LF(X)[4,11],为基于格值逻辑系统的自动推理提供了良好的逻辑基础.基于格蕴涵代数的格值逻辑系统,既有逻辑公式的形式演绎,同时又有形式演绎真值的合理传递.在格值命题逻辑系统和格值一阶逻辑系统框架下徐扬等分别建立了α归结原理[12-13],也给出了49种情况下广义文字可归结性的判定方法[14].

借鉴经典逻辑的广义归结原理,徐扬提出了基于格值命题逻辑系统LP(X)的α广义归结原理,将广义子句集推广到了一般广义子句集上,使一般广义子句直接参与归结过程[15-16].笔者依据以上的研究成果,进一步研究基于格蕴涵代数的格值一阶逻辑系统LF(X)的α广义归结原理,为建立基于格值逻辑系统的广义归结自动推理方法提供基础.

1 预备知识

格值一阶逻辑系统LF(X)指基于格蕴涵代数L=(L,∨,∧,′,→,O,I)的格值一阶逻辑系统,格蕴涵代数的概念及主要性质参看文献[4,10],下面将简要给出基于格值一阶逻辑系统LF(X)的α归结原理.

定义1 在格值一阶逻辑系统LF(X)中,设α∈L,且广义子句[4]

如果广义文字gi和hj在替换σ下使得则

称为C1和C2的α归结式,记作Rα(C1,C2).(gi,hj)称为一个α归结对,记作(gi,hj)-α.

定义2 在格值一阶逻辑系统LF(X)中,设S={C1,…,Ci,…,Cn},是一个广义子句集,α∈L.如果满足下列条件[4]之一:

(1)Di∈S,

(2)存在j,k＜i,使得Di=Rα(Dj,Dk),

则称ω={D1,…,Di,…,Dm},是一个从广义子句集S出发到广义子句Dm的α归结演绎.

定理1(α归结原理的可靠性)[4]设S是格值一阶逻辑系统LF(X)的一个广义子句集,α∈L,ω={D1,…,Di,…,Dm},是一个从S出发到广义子句Dm的α归结演绎.如果Dm=α,则S≤α,即如果Dm≤α,则S≤α.

定理2(α归结原理的弱完备性)[4]设S是格值一阶逻辑系统LF(X)的一个广义子句集,S*是广义子句集S的广义Skolem标准型,α∈L,α＜I.如果S*≤α,则存在一个从S*出发到α的α归结演绎.

定义3 在格值命题逻辑系统LP(X)中,设C是一个广义子句,g是广义文字,A(C)和A(g)分别是C和g的原子集.如果A(C)∩A(g)=ø,则称C和g是相互独立的[16].

定义4 在格值命题逻辑系统LP(X)中,g是一个广义文字.如果存在一个赋值v使得v(g)=I,则称g是正规的[16].

格值逻辑系统、基于格值逻辑系统的α归结原理的详细内容参看文献[4].

2 基于格值一阶逻辑系统LF(X)的α广义归结原理

这一节将推广基于格值一阶逻辑系统LF(X)的α归结原理,给出LF(X)中一般广义子句的概念,并提出基于格蕴涵代数L的格值一阶逻辑系统LF(X)的α广义归结原理.

定义5 设g1,g2,…,gn是格值一阶逻辑系统LF(X)中的广义文字,Φ(g1,g2,…,gn)是由逻辑联结词“∨,∧,′,→,↔”连接这些广义文字构成的一个格值逻辑公式,则称这个逻辑公式是LF(X)中的一般广义子句.

例1 设LF(X)是基于格蕴涵代数L的格值一阶逻辑系统,则

是一般广义子句,这里,a∈L,p,q,r是关系符号,x,y,z是个体变元.

根据格值一阶逻辑系统LF(X)中对公式的语义解释,给出一般广义子句作为一个格值逻辑公式的α可满足性、α真和α假的定义.

定义6 设Φ是格值一阶逻辑系统LF(X)中的一般广义子句,α∈L,α＜I.

(1)如果存在解释ID=,有vD(Φ)＞α,则称Φ是α可满足.

(2)如果对任意的解释ID=,有vD(Φ)＞α,则称Φ是α真.

(3)如果对任意的解释ID=,有vD(Φ)≤α,则称Φ是α假.

对于一个格值逻辑公式,如果含有存在量词或广义量词,可以借助于下面定理对该公式进行等价变形.

定理3 在格值一阶逻辑系统LF(X)中,设Φ和Ψ是格值逻辑公式,x不是Φ中的自由变元,则下列结论成立:

(1)Φ→(∀x)Ψ=(∀x)(Φ→Ψ),Φ→(∃x)Ψ=(∃x)(Φ→Ψ).

(2)(∃x)Ψ→Φ=(∀x)(Ψ→Φ),(∀x)Ψ→Φ=(∃x)(Ψ→Φ).

(3)Φ∨(∀x)Ψ=(∀x)(Φ∨Ψ),Φ∧(∀x)Ψ=(∀x)(Φ∧Ψ).

(4)Φ∨(∃x)Ψ=(∃x)(Φ∨Ψ),Φ∧(∃x)Ψ=(∃x)(Φ∧Ψ).

在格值一阶逻辑系统LF(X)中,设S=Φ1∧…∧Φi∧…∧Φn,Φi(i=1,2,…,n)是一般广义子句,则称S为一般广义子句集,记作S={Φ1,…,Φi,…,Φn}.

定义7 设S是格值一阶逻辑系统LF(X)中的一般广义子句集,x1,x2,…,xn是S中的所有自由变元,则逻辑公式∀x1∀x2…∀xnS*称为S的格值全称化,即,逻辑公式∀x1∀x2…∀xnS*称为S的格值全称封闭公式.

特别地,如果逻辑公式S中没有自由变元,则S的格值全称封闭公式为S本身.

下面所提到的格值一阶逻辑系统LF(X)中的一般广义子句集都是指一个格值全称封闭公式.

定义8 设Φ是格值一阶逻辑系统LF(X)中的一般广义子句,如果某些局部极复杂广义文字gi(i=1,2,…,r)存在一个最一般合一σ,则称Φσ是Φ的一个因子.

定义9 设Φ(g1,g2,…,gi,…,gn)和Ψ(h1,h2,…,hj,…,hn)是格值一阶逻辑系统LF(X)中两个没有公共变元的一般广义子句,α∈L.如果存在最一般合一σ、τ和替换ρ满足条件:

(1)Φσ是通过合一Φ中局部极复杂广义文字gi1,gi2,…,gis的因子,

(2)Ψτ是通过合一Ψ中局部极复杂广义文字hj1,hj2,…,hjs的因子,

为了得到α广义归结原理的可靠性定理,先给出下面一个定理,即广义归结式是两个一般广义子句的逻辑结果.

定理4 设Φ和Ψ是格值一阶逻辑系统LF(X)中的两个一般广义子句,α∈L,α＜I.如果在Φ和Ψ中分别存在局部极复杂广义文字g和h在替换ρ下满足gρ∧hρ≤α,且Rf(α-g)-g(Φ,Ψ)是Φ和Ψ的α广义归结式,则

证明 因为在Φ和Ψ中分别存在局部极复杂广义文字g和h在替换ρ下满足gρ∧hρ≤α,根据文献[16]中的定理3.1,则Φρ∧Ψρ≤Φρ(gρ=α)∨Ψρ(hρ=α).

而Φ∧Ψ≤Φρ∧Ψρ,所以,Φ∧Ψ≤Φρ(gρ=α)∨Ψρ(hρ=α).

定义10 设S是格值一阶逻辑系统LF(X)中的一般广义子句集,α∈L,α＜I.ω={D1,…,Di,…,Dm},是从广义子句集S出发到一般广义子句Dm的一个α广义归结演绎,如果满足

(1)Di∈S,或者

下文给出基于格值一阶逻辑系统LF(X)的α广义归结原理的可靠性,同时建立提升引理,给出该原理的弱完备性定理.

定理5(可靠性) 设S是格值一阶逻辑系统LF(X)中的一般广义子句集,α∈L,α＜I.ω={D1,…,Di,…,Dm},是从广义子句集S出发到一般广义子句Dm的一个α广义归结演绎.如果Dm是α″,则S≤α,即Dm≤α,则S≤α.

证明 根据定理4容易得到.证毕.

证明 设Φ1和Φ2是LF(X)中的两个一般广义子句.如果Φ1和Φ2中没有公共变元,则分别设为x1,x2,…,xn和y1,y2,…,yn;否则重新命名Φ1和Φ2中的变元,使得它们没有公共变元.假设Φ1和Φ2中已经没有公共变元.

图1 α广义归结原理的提升引理

(2)Φ1=Φ1(g1,g11,g12,…,g1r1)满足条件{g1,g11,g12,…,g1r1}={h|h是Φ1中的局部极复杂广义文字,},Φ2=Φ2(g2,g21,g22,…,g2r2)满足条件{g2,g21,g22,…,g2r2}={h|h是Φ2中的局部极复杂广义文字,.于是,其中,Φ1(g1,g11,g12,…,g1r1)表示在Φ1中的局部极复杂广义文字g1,g11,g12,…,g1r1是可以合一的表示将g1,g11,g12,…,g1r2合一为后得到的一般广义子句.Φ2=Φ2(g2,g21,g22,…,g2r2)表示在Φ2中的局部极复杂广义文字g2,g21,g22,…,g2r2是可以合一的.表示将g1,g11,g12,…,g1r2合一为后得到的一般广义子句.

定理7(弱完备性) 设S是格值一阶逻辑系统LF(X)中的一般广义子句集,α∈L,α＜I,HS={g1,g2,…,gn},是S中一般广义子句的局部极复杂广义文字集合.如果满足下列条件:

(1)S≤α,

(2)h1和h2分别是一般广义子句Φ和Ψ中的局部极复杂广义文字,使得在替换ρ下有hρ1∧hρ2≤α,且和分别与一般广义子句集Sρ*是相互独立的,其中,则存在一个从一般广义子句集S出发到α的α广义归结演绎.

证明 如果一般广义子句集S≤α,根据文献[4]中的定理11.4.5,则存在一般广义子句集S的一个有限基例集S0,使得S0≤α.通过文献[16]中的定理3.3,存在从一般广义子句集S0出发到α的α广义归结演绎ω0.根据定理6和α广义归结演绎ω0,存在从一般广义子句集S出发到α的α广义归结演绎ω.证毕.

3 结束语

在基于格蕴涵代数的格值一阶逻辑系统LF(X)中,笔者推广了传统的α归结原理,将广义子句集上的归结问题推广到一般广义子句集上,即归结过程中的子句将直接使用一般广义子句,而不再转换为合取范式,使归结过程更加直观、自然.笔者基于格值一阶逻辑系统提出了一般广义子句集上的α广义归结原理,建立了该原理的可靠性定理,通过提升引理给出了α广义归结原理的弱完备性定理.这些研究工作将为进一步探索基于格值逻辑系统的α广义归结方法奠定一定的基础.

[1]Robinson J P.A Machine-Oriented Logic Based on the Resolution Principle[J].Journal of ACM,1965,12(1):23-41.

[2]Chang C L,Lee R C T.Symbolic Logic and Mechanical Theorem Proving[M].New York:Academic Press,1973.

[3]Wos L.Automated Reasoning:33 Basic Research Problems[M].Englewood Cliffs:Prentice Hall,1988.

[4]Xu Y,Ruan D,Qin K Y,et al.Lattice-Valued Logic—an Alternative Approach to Treat Fuzziness and Incomparability [M].New York:Springer-Verlag,2003.

[5]Sofronie-Stokkermans V.Automated Theorem Proving by Resolution in Non-Classical Logics[J].Annals of Mathematics and Artificial Intelligence,2007,49(1-4):221-252.

[6]Riva A,Nuzzo A,Stefanelli M,et al.An Automated Reasoning Framework for Translational Research[J].Journal of Biomedical Informatics,2010,43(3):419-427.

[7]Lu Zhirui,Augusto J,Liu Jun,et al.A Linguistic Truth-Value Temporal Reasoning(LTR)System and Its Application to the Design of an Intelligent Environment[J].International Journal of Computational Intelligence Systems,2012,5(1):173-196.

[8]王湘浩,刘叙华.广义归结[J].计算机学报,1982,5(2):81-92. Wang Xianghao,Liu Xuhua.Generalized resolution[J].Chinese Journal of Computers,1982,5(2):81-92.

[9] 刘叙华.基于归结方法的自动推理[M].北京:科学出版社,1994.

[10]徐扬.格蕴涵代数[J].西南交通大学学报,1993,89(1):20-27. Xu Yang.Lattice Implication Algebra[J].Journal of Southwest Jiaotong University,1993,89(1):20-27.

[11]Xu Y,Liu J,Song Z M,et al.On Semantics of L-Valued First-Order Logic Lvft[J].International Journal General Systems,2000,29(1):53-79.

[12]Xu Y,Ruan D,Kerre E E,et al.α-Resolution Principle based on First-Order Lattice-Valued Logic LF(X)[J]. Information Sciences,2001,132(1-4):221-239.

[13]Xu Y,Ruan D,Kerre E E,et al.α-Resolution Principle based on Lattice-Valued Propositional Logic LP(X)[J]. Information Sciences,2000,130(1-4):195-223.

[14]Xu Y,Liu J,Ruan D,et al.Determination ofα-resolution in Lattice-valued First-order Logic LF(X)[J].Information Sciences,2011,181(10):1836-1862.

[15]徐扬.基于格值逻辑的语言真值α-广义归结自动推理研究[J].学术动态(西南交通大学),2009,(4):1-12. Xu Yang.Linguistic Truth-valuedα-generalized Resolution Automated Reasoning Research Based on Lattice-valued Logic [J].Xushu Dongtai(Southwest Jiaotong University),2009,(4):1-12.

[16]Xu Y,Xu W T,Zhong X M,et al.α-Generalized Resolution Principle Based on Lattice-valued Propositional Logic LP(X)[C]//Proceedings of the 9th International FLINS Conference.Singapore:World Scientific Publishing,2010:66-71.

(编辑:李恩科)

α-generalized resolution principle based on the lattice-valued first-order logic system

XU Weitao1,ZH ANG Wenqiang1,XU Yang2,ZH ANG Dexian1
(1.College of Information Science and Engineering,Henan Univ.of Technology,Zhengzhou 450001,China;2.School of Mathematics,Southwest Jiaotong Univ.,Chengdu 610031,China)

In the framework of the lattice-valued logic system based on the lattice implication algebra,the α-resolution principle based on the lattice-valued logic system is extended from generalized clauses set to general generalized clauses set.In this paper,theα-generalized resolution principle is presented in the lattice-valued first-order logic system LF(X).At the same time,the soundness theorem is established in LF(X).By using the lift lemma,the weak completeness theorem is also proved.This work can provide a new automated reasoning technology in order to establish novel generalized resolution methods for latticevalued logic systems.

lattice-valued first-order logic;general generalized clause;local extremely complex generalized literal;generalized resolution;automated reasoning

TP391

A

1001-2400(2014)01-0135-05

10.3969/j.issn.1001-2400.2014.01.024

2012-11-08 < class="emphasis_bold">网络出版时间:

时间:2013-09-16

国家自然科学基金资助项目(61175055);国家自然科学青年基金资助项目(61300123);国家高技术研究发展计划(863计划)资助项目(2012AA101608);河南省教育厅自然科学资助项目(13B520945);河南工业大学高层次人才基金资助项目(2012BS012)

许伟涛(1979-),男,讲师,博士,E-mail:hnxmxwt@163.com.

http://www.cnki.net/kcms/detail/61.1076.TN.20130916.0926.201401.168_020.html