多值知识编译

2011-12-27 03:50谷文祥郭鸿鹤殷明浩王金艳刘日仙
关键词:子句知识库定理

谷文祥,郭鸿鹤,殷明浩,王金艳,刘日仙

(1.东北师范大学计算机科学与信息技术学院,吉林长春 130117;2.金华职业技术学院信息工程学院,浙江金华 321017)

多值知识编译

谷文祥1,郭鸿鹤1,殷明浩1,王金艳1,刘日仙2

(1.东北师范大学计算机科学与信息技术学院,吉林长春 130117;2.金华职业技术学院信息工程学院,浙江金华 321017)

定义了一类新的易处理理论:s-EPCCL理论.在此基础上,提出了一种以s-EPCCL理论为目标语言的多值知识编译方法.该方法与现有知识编译方法不同的是,它可以对多值知识库进行编译.经过多值编译后,任意查询都可以在多项式时间内得到应答.

多值逻辑;知识编译;标记逻辑;EPCCL

0 引言

近年来,知识编译已经成为自动推理研究中的一个重要方向[1-10].其主要思想是将推理分为两个阶段:离线编译阶段和在线推理阶段.在离线编译阶段,将给定知识库编译成与之等价的易处理的目标语言理论;在后一阶段,利用目标语言回答查询.知识编译方法的关键在于它将大部分计算时间花费在离线编译阶段,编译只需一次,而且编译所花的时间可以通过对同一个知识库的多次询问得到补偿.

自知识编译方法提出后,涌现出许多知识编译的目标语言,如BDD[11],OBDD[2],IP/PI[1,3],Horn clauses[3],DNNF[6-7],FNNF[8]等.另一方面,文献[12]提出了一类新的目标语言理论-EPCCL,并提出了以EPCCL作为目标语言的知识编译方法.该方法与现有其他知识编译方法的一个重要的不同是,不论在编译阶段还是查询阶段都是基于扩展规则的,而其他方法都是基于归结原理的.对于互补因子较高的知识库,基于扩展规则的知识编译方法比基于归结的知识编译方法更为高效.因此,它被看做是与归结方法互补的一种方法.

然而,现有知识编译方法处理的知识库都是以经典的布尔变量为基础的.经典逻辑对知识的表示能力是有限的,而多值逻辑比经典逻辑具有更强的表示能力,更能适应实际需要.本文提出了一种基于扩展规则的多值逻辑推理方法.这里,我们关注标记逻辑.因为对于任意一个多值逻辑知识库,我们都可以找到一个与之等价的标记逻辑知识库.反之亦然.

本文工作如下:首先,基于经典的扩展规则,提出了标记扩展规则的概念.第二,在经典的易处理可满足性和易处理蕴含[12]之上我们提出了标记易处理蕴含类的概念.只有满足易处理蕴含类性质的语言才可以作为知识编译的目标语言.第三,在标记扩展规则基础上提出了一种新的知识编译语言s-EPCCL,并且证明了s-EPCCL是在易处理蕴含类中的.第四,提出了一种基于标记扩展规则知识编译算法SKCER.并证明了该算法的完备性和可靠性.即给定一个任意标记知识库,都可以转化为一个等价的s-EPCCL理论.

1 背景知识

假定语言Λ,其中的逻辑公式由原子集合、连接符集合和逻辑常量集合组成.语言Λ的真值集合是Δ,Λ的解释是从原子集合到真值集合Δ的一个映射.

定义1.1[13](标记) 一个标记是真值集合Δ的一个子集,一个标记公式是形式为S:F的表达式,其中S是一个标记,F是Λ中的一个公式.如果F是Λ中的一个原子,则称S:F是一个标记原子.

我们可以在多值逻辑上应用标记逻辑进行元推理.标记原子只有两个真值:真或假.标记逻辑是经典逻辑的一种,它为多值逻辑推理提出了一个经典逻辑框架.

为了能够应答任意查询,将Λ中的公式映射为经典命题逻辑Λs中的公式,即标记公式语言.

定义1.2[13](标记公式语言) 在Λs中,如果原子是标记公式,连接符是经典的合取和析取,那么Λs称为标记公式语言.

与Λ的真值集不同的是,Λs的真值集为{1,0},即真和假.

在介绍正规标记公式之前,假定真值集Δ是有排序≤的一个完备格.用Sup和Inf表示真值集Δ子集的最小上界和最小下界.

令(P;≤)是一个任意的偏序集,且Q⊆P.则定义↑Q={y∈P|(∃x∈Q)x≤y}.如果Q是一个单元素集{x},则简写为↑x.

定义1.3[14](正规集)Q是P的子集,如果对于某一x∈P,Q=↑x或Q=(↑x)′(↑x的补集),则称Q是正规的.前一种情况,我们称Q是正的;后一种情况,我们称Q是负的.

定义1.4[14](正规标记公式) 如果一个标记公式中出现的所有标记都是正规的,则称该标记公式是正规的.

这里,给出正规标记归结的简单定义.首先介绍互补标记文字的定义.

定义1.5[14](互补标记文字) 两个标记文字↑a:A和(↑b)′:A,如果满足a≥b,则称这两个标记文字互补.

定义1.6[14](正规标记归结) 给定两个带有标记的子句S1∨D1和S2∨D2,其中S1和S2是互补标记文字,则两个子句在标记文字S1和S2上的标记归结式是D1∨D2.

2 标记扩展规则

定义2.1[8]给定一个子句C和一个集合M:C′={C∨a,C∨﹁a|a是一个原子,a∈M且a不在C中出现}.我们称从C到C′的操作为C上的扩展规则,称C′是扩展规则的结果.

在定义标记扩展规则之前,我们给出如下假设:语言中有两类变量——布尔变量和标记变量.标记变量都是正规标记变量,多值逻辑变量的域是以在某一排序≤下的完备格.

根据经典的扩展规则,我们可以定义正规标记公式上的扩展规则,简称为标记扩展规则.标记扩展规则可以看作是正规标记归结的逆操作.

给定一个子句C,一个标记变量集合S,↑a:A是S中的一个标记原子,则子句C在该标记原子上应用扩展规则得到结果是{C∨↑a:A,C∨(↑b)′:A},其中↑a:A和(↑b)′:A是互补文字.

为了减少由于使用扩展规则而出现的文字个数,我们用(↑a)′:A代替(↑b)′:A.下面定义了标记原子上的扩展规则.

定义2.2(标记扩展规则) 给定一个子句C,一个标记原子集合S:C′={C∨↑a:A,C∨(↑a)′:A|↑a:A是一个标记原子,↑a:A∈S并且↑a:A不出现在C中}.

我们称从C到C′的操作是C上的标记扩展规则.

定理2.1一个子句C逻辑上等价于标记扩展规则的结果C′.

定理2.1保证了标记扩展规则是一个合法的规则.

定义2.3一个标记子句是集合M上的最大项(包括布尔和标记原子)当且仅当它或以正文字形式或以负文字形式包含M中的所有原子.

定理2.2给定一个标记子句的集合Σ,其中的原子集合为M(|M|=m),如果Σ中的子句都是M上的最大项,则Σ是不可满足的当且仅当它包含2m个子句.

上述定理描述了一个最大项公式集合可满足时的条件.

所有子句都扩展为最大项所需要的空间是不可估计的.针对这一问题,我们使用容斥原理计算在Σ上应用经典和标记扩展规则后得到的最大项数目.

给定一个子句集合Σ={C1,C2,…,Cn},M是Σ中出现的所有原子的集合,并且在子句集合中存在标记子句.令Pi为在Ci上应用经典和标记扩展规则得到的所有最大项的集合.令S为在Σ上应用经典和标记扩展规则后得到的不同最大项的个数.可以得到:

基于上述公式,我们可以通过计算最大项的数目来确定子句集的可满足性.由公式可知,如果知识库中子句间两两包含互补对,计算最大项数目的过程简化为只计算公式的前N项.所以,我们可以利用经典的和标记的扩展规则方法更有效率地得到一个标记知识库的可满足性.

另外,在带有标记变量的知识编译中,如果需要在一个标记变量上扩展某一子句,则使用标记扩展规则方法;否则,使用经典的扩展规则方法.

3 标记EPCCL理论

定义3.1(标记EPCCL理论) 一个标记EPCCL理论(s-EPCCL)是一个带有标记文字的子句集合,其中每一对子句之间都存在互补文字,或者是互补的布尔文字,或者是互补的标记文字.

标记EPCCL理论的可满足性可以由经典扩展规则和标记扩展规则在线性时间内得到.

Del Val证明了“易处理蕴含”与“易处理可满足性”之间的关系.文献[12]证明了一个泛化的定理,说明EPCCL理论在“易处理蕴含”类中.

定理3.1[12]令L为满足下述条件的任意一类理论:(1)Σ∈L是不可满足的当且仅当Σ├p□;(2)如果Σ∈L,则对于每个单元子句l,Σ∪{l}∈L,或在一个多项式过程之后满足Σ∪{l}∈L.则对于任意的Σ∈L,关于Σ的任意查询可以在多项式时间内被回答.

上述定理是基于经典逻辑的,而一个s-EPCCL理论并不属于经典逻辑.下面我们将上述定理进行泛化,得到标记易处理蕴含,并证明s-EPCCL理论属于“标记易处理蕴含”类.

定理3.2(标记易处理蕴含) 令L是满足下述条件的任意一类标记逻辑理论:(1)Σ∈L是不可满足的当且仅当Σ├p□;(2)如果Σ∈L,对于任意一个经典的或标记的单元子句l,有Σ∪{l}∈L成立,或在一个多项式过程之间满足Σ∪{l}∈L.则对于每个Σ∈L,Σ上的任意查询都可以在多项式时间内得到应答.即Σ属于“标记易处理蕴含”类.

上述定理说明s-EPCCL可以作为多值逻辑(可转化为标记逻辑)知识编译的目标语言.也就是说,标记子句集可以由经典扩展规则和标记扩展规则编译得到一个等价的s-EPCCL理论.编译得到的子句集可以在多项式时间内应答任意查询.这一过程称作基于经典和标记扩展规则的多值知识编译.

定理3.3标记EPCCL理论上的任意查询都可以在多项式时间内得到应答.

证明对于任意标记EPCCL理论,它的可满足性可以由标记扩展规则在多项式时间内决定.定理3.2的第一个条件满足.下面证明第二个条件也是满足的.新添加的子句l或者是以布尔文字组成的经典的单元子句,或者是一个标记单元子句.如果添加的单元子句是前者,那么根据定理3.2的证明过程可知,加入新单元子句后的子句集一定满足第二个条件.如果添加的单元子句是标记单元子句,则需要对原始子句集中的每一个子句进行处理,使之与新添加单元子句之间存在互补文字.有三种情况:如果两个子句之间已经存在互补文字,不需要做任何处理;如果新添加的标记单元子句蕴含某一原始子句,即当标记单元子句为真时原始子句也为真,则删除被蕴含的原始子句;除了上述两种情况,其他的子句都必须在标记单元子句的标记文字上用标记扩展规则进行扩展,然后用扩展得到的结果代替原子句.在这三种情况里,子句集的大小不会增加.以上证明了如果向原始理论中加入一个标记单元子句,可以在多项式时间内得到一个等价的标记EPCCL理论.根据定理3.2,标记EPCCL理论属于“标记易处理蕴含”类.

由上述定理及证明过程可知,标记EPCCL理论可以看做是多值逻辑知识编译的目标语言.

4 标记EPCCL知识编译

在文献[12]中提到的变量都是布尔变量,公式都是经典的CNF.然而,在许多领域里,我们不仅需要布尔变量,还需要一些多值变量去表示实体的一些属性.但是,直接向经典公式中加入多值变量可能会增加原始问题的难度.另外,目前也没有一种有效的方法可以处理带有多值变量的公式集.因此,我们提出了一种可以处理多值变量的新的知识编译方法.

在标记公式中标记文字和布尔文字有着相同的定义域,所以标记知识编译算法与经典的应用扩展规则的知识编译算法类似.

下面我们给出一个带有标记的知识编译算法,即标记EPCCL知识编译算法.其基本思想是基于“桶删除(bucket elimination)”的思想.

定理4.1算法SKCER中,Σ3逻辑上等价于Σ1,Σ3是一个s-EPCCL理论.

证明由于删除规则和扩展规则(经典和标记扩展规则)都具有等价保持性质,所以Σ3逻辑上等价于Σ1.下面我们证明Σ3是一个s-EPCCL理论.算法SKCER中,如果一个子句移入Σ2,该子句扩展后的结果一定与Σ1中所有其他的子句之间有互补文字(布尔或/和标记互补文字).很显然,在一个子句被移入Σ2之前,Σ3中的所有子句都一定已经与之有互补文字.将子句移入Σ2中后,扩展该子句并不会使得原本已经存在的子句间的互补文字消失.所以,当算法结束时,Σ3中的所有子句都与知识库中的所有其他子句含有互补文字.因此,算法的输出一定是一个s-EPCCL理论.

由于编译后子句集的大小直接关系到在线推理的时间,为了能使编译后子句集的规模尽量小,我们给出了下面一条策略.

策略1在使用带标记的扩展规则进行知识编译过程中,如果需要扩展一个子句来确保它与其他子句包含互补文字,则优先选择布尔变量作为子句扩展时的扩展原子;如果所有的布尔变量都无用,选择一个适当的标记变量.

文献[12]给出了两条策略来优化编译后的知识库规模.

策略2[12]如果同时有两个子句需要扩展,扩展较长的那个.

策略3[12]在编译过程中优先考虑单元子句.

在带有标记的知识编译过程中综合考虑上述三条策略,我们可以将编译后知识库的大小进行优化,保证编译的简洁性,并且降低子句的复杂性.

5 总结

现有的知识编译方法都是以经典命题理论为基础的.然而,在我们的现实世界中,很多问题更倾向于用现有知识编译方法不能处理的多值公式来表示.因此,我们提出了一类新的目标语言理论,即标记EPCCL理论.在此基础上,进一步提出了一种基于标记扩展规则的多值知识编译方法,该方法用标记扩展规则对带有标记的公式进行处理,得到一个与原理论逻辑等价的标记EPCCL理论.

[1]REITER R,DE KLEER J.Foundations of assumption-based truth maintenance systems:preliminary report[J].AAAI,1987,87:183-189.

[2]BRYANT R E.Symbolic Boolean manipulation with ordered binary decision diagrams[J].ACM Computing Surveys,1992,24(3):293-318.

[3]SELMAN B,KAUTZ H.Knowledge compilation and theory approximation[J].J of the ACM,1996,43(2):193-224.

[4]CADOLI M,DONINI F M.A survey on knowledge compilation[J].AI Communications,1997,10:137-150.

[5]DARWICHE A,MARQUIS P.A knowledge compilation map[J].JAIR,2002,2:229-264.

[6]DARWICHE A.Decomposable negation normal form[J].Journal of the ACM,2001,48(4):608-647.

[7]DARWICHE A.A compiler for deterministic,decomposable negation normal form[J].AAAI,2002,2:627-634.

[8]HAHNLE R,MURRAY NV,ROSENTHAL E.Normal forms for knowledge compilation[J].Proceedings of the International Symposium on Methodologies for Intelligent Systems,Lecture Notes in Computer Science,2005,3488:304-313.

[9]刘日仙,袁利永,谷文祥.智能规划学习和学习型智能规划系统架构研究[J].东北师大学报:自然科学版,2010,42(2):44-49.

[10]蔡增玉,甘勇,谷文祥,等.基于应对规划的入侵防护系统设计与研究[J].东北师大学报:自然科学版,2010,42(3):43-47.

[11]BRYANT R E.Graph-based algorithms for Boolean function manipulation[J].Transactions on Computers,1986,8:677-691.

[12]LIN HAI,SUN JIGUI.Knowledge compilation using the extension rule[J].Journal of Automated Reasoning,2004,32:93-102.

[13]JAMES J LU,NV MURRAY.A framework for automated reasoning in multiple-valued logics[J].Journal of Automated Reasoning,1998,21:39-67.

[14]JAMES J LU,MURRAY NV,ERIK ROSENTHAL.Duction and search strategies for regular multiple-valued logics[J].Journal of Multiple-valued logic and soft computing,2005,11:375-406.

Compiling multi-valued knowledge base

GU Wen-xiang1,GUO Hong-her1,YIN Ming-hao1,WANG Jin-yan1,LIU Ri-xian2

(1.College of Computer Science and Information Technology,Northeast Normal University,Changchun 130117,China;2.Institute of Information Engineering,Jinhua College of Profession and Technology,Jinhua 321017,China)

In this paper,a new class of tractable theories are defines:s-EPCCL theories.Using s-EPCCL theories as a target language,a method for multiple-valued knowledge compilation is Proposed.Different from the existing knowledge compilation,the proposed method is used to compile on multiple-valued knowledge base.With the compilation method,any query on the multiple-valued knowledge theories can be answered in polynomial time in the size of the compiled knowledge base.

multiple-valued logic;knowledge compilation;signed logic;EPCCL

TP 301

520·20

A

1000-1832(2011)04-0044-05

2010-12-18

国家自然科学基金资助项目(60803102;61070084;60573067);浙江省教育厅科研计划项目(Y200908315).

谷文祥(1941—),男,教授,博士研究生导师,主要从事智能规划与规划识别研究.

陶 理)

猜你喜欢
子句知识库定理
命题逻辑中一类扩展子句消去方法
J. Liouville定理
命题逻辑可满足性问题求解器的新型预处理子句消去方法
A Study on English listening status of students in vocational school
基于TRIZ与知识库的创新模型构建及在注塑机设计中的应用
西夏语的副词子句
“三共定理”及其应用(上)
高速公路信息系统维护知识库的建立和应用
基于Drupal发布学者知识库关联数据的研究
命题逻辑的子句集中文字的分类