命题逻辑中一种矛盾体生成新方法_黎兴玉.pdf

命题逻辑中一种矛盾体生成新方法*黎兴玉1,何星星1,马 雪1,李莹芳2(1.西南交通大学数学学院,四川 成都 6 1 0 0 3 1;2.西南财经大学计算机与人工智能学院,四川 成都 6 1 1 1 3 0)摘 要:人工智能是用计算机来模拟人的某些思维过程和智能行为的学科。自动推理中的归结原理是一种简洁、可靠且完备的推理规则。矛盾体的动态多子句协同演绎理论不仅是归结原理的重要延拓,而且具有较高的推理演绎效率。由于矛盾体的结构复杂、生成策略较少,因此在矛盾体的动态演绎可靠性和完备性的基础上,提出复合2个或多个矛盾体的部分子句的不同策略,为矛盾体的构造提供了一种有效的方法。关键词:命题逻辑;矛盾体;矛盾体的复合性质;不可满足性中图分类号:T P 1 8 1文献标志码:Ad o i:1 0.3 9 6 9/j.i s s n.1 0 0 7-1 3 0 X.2 0 2 3.0 6.0 2 1A n e w c o n t r a d i c t i o n g e n e r a t i o n m e t h o d i n p r o p o s i t i o n a l l o g i cL I X i n g-y u1,HE X i n g-x i n g1,MA X u e1,L I Y i n g-f a n g2(1.S c h o o l o f M a t h e m a t i c s,S o u t h w e s t J i a o t o n g U n i v e r s i t y,C h e n g d u 6 1 0 0 3 1;2.S c h o o l o f C o m p u t i n g a n d A r t i f i c i a l I n t e l l i g e n c e,S o u t h w e s t e r n U n i v e r s i t y o f F i n a n c e a n d E c o n o m i c s,C h e n g d u 6 1 1 1 3 0,C h i n a)A b s t r a c t:A r t i f i c i a l I n t e l l i g e n c e(A I)i s a d i s c i p l i n e t h a t s i m u l a t e s s o m e t h i n k i n g p r o c e s s e s a n d i n t e l-l i g e n t b e h a v i o r s o f h u m a n b e i n g s w i t h c o m p u t e r s.T h e r e s o l u t i o n p r i n c i p l e i n a u t o m a t i c r e a s o n i n g i s a c o n c i s e,r e l i a b l e a n d c o m p l e t e r e a s o n i n g r u l e.T h e c o n t r a d i c t i o n s e p a r a t i o n b a s e d d y n a m i c m u l t i-c l a u s e s y n e r g i z e d a u t o m a t e d d e d u c t i o n i s n o t o n l y a c r u c i a l e x t e n s i o n o f r e s o l u t i o n p r i n c i p l e,b u t a l s o h a s h i g h-e r d e d u c t i v e e f f i c i e n c y.D u e t o t h e c o m p l e x s t r u c t u r e o f c o n t r a d i c t i o n s a n d f e w e r g e n e r a t i o n s t r a t e g i e s,t h e p a p e r p r o p o s e s d i f f e r e n t s t r a t e g i e s f o r c o m p o u n d i n g t h e p a r t i a l c l a u s e s o f t w o o r m o r e c o n t r a d i c t i o n s o n t h e b a s i s o f t h e d y n a m i c d e d u c t i o n r e l i a b i l i t y t h e o r e m a n d c o m p l e t e n e s s t h e o r e m o f c o n t r a d i c t i o n s,w h i c h p r o v i d e s a n e f f e c t i v e m e t h o d f o r t h e c o n s t r u c t i o n o f c o n t r a d i c t i o n s.K e y w o r d s:p r o p o s i t i o n a l l o g i c;c o n t r a d i c t i o n;c o m p o u n d p r o p e r t i e s o f c o n t r a d i c t i o n s;u n s a t i s f i a b i l i t y1 引言自1 7世纪末叶,德国数学家L e i b n i z创立了数理逻辑以来,广大研究人员就开启了探索用计算机模拟人类证明命题逻辑定理的推理过程,并随着 逻辑理论机 的面世,自动定理证明AT P(A u t o-m a t i c T h e o r e m P r o v e r)1进入了人们的视野。自动定理证明在软硬件领域2、专家系统3、问答系统4、语义网、知识图谱等知识表示和知识推理领域5,以及人工智能中的模型推理研究6和数学定理证明7,8等领域都扮演着重要的角色。1 9 6 5年,R o b i n s o n9在H e r b r a n d1 0定理的基础上,提出了归结原理。1 9 7 2年,W o s等1 1建立了一个以归结方法为推理规则的自动推理系统AUR A(AU t o-m a t e d R e a s o n i n g A s s i s t a n t),推动了自动定理证明的发展。在自动定理证明的发展中,产生了许多归结的*收稿日期:2 0 2 1-0 8-2 5;修回日期:2 0 2 1-1 2-2 7基金项目:国家自然科学基金(6 2 1 0 6 2 0 6);教育部人文社科项目(1 9 Y J C Z H 0 4 8,2 0 X J C Z H 0 1 6);中央高校基本科研业务费专项资金(2 6 8 2 0 2 0 Z T 1 0 7)通信作者:何星星(x.h e h o m e.s w j t u.e d u.c n)通信地址:6 1 0 0 3 1 四川省成都市西南交通大学数学学院A d d r e s s:S c h o o l o f M a t h e m a t i c s,S o u t h w e s t J i a o t o n g U n i v e r s i t y,C h e n g d u 6 1 0 0 3 1,S i c h u a n,P.R.C h i n a C N 4 3-1 2 5 8/T PI S S N 1 0 0 7-1 3 0 X 计算机工程与科学C o m p u t e r E n g i n e e r i n g&S c i e n c e第4 5卷第6期2 0 2 3年6月 V o l.4 5,N o.6,J u n.2 0 2 3 文章编号:1 0 0 7-1 3 0 X(2 0 2 3)0 6-1 1 3 4-0 7改进策略,例如锁归结、语义归结1 2,1 3和线性归结1 4等。这些归结变体及改进策略通过限制子句或文字归结减少归结式的产生,从而提高归结效率,但仍存在许多未能解决的实际问题。基于此,X u等1 5建立了基于标准矛盾体分离的动态多子句协同自动演绎理论,该理论具有可靠性与完备性。将矛盾体分离理论的动态多子句协同演绎用于自动推理系统,能更有效地提高自动推理系统的演绎能力和效率。在此理论的基础上,徐扬等1 6将命题逻 辑提升到一 阶逻辑,先 后提出了C S E(C o n t r a d i c t i o n S e p a r a t i o n E x t e n t i o n)和C S E_E等证明器。且自2 0 1 8年以来,证明器在自动定理证明系统竞赛中连续获得亚军。C a o等1 7将C S E证明器用于定理证明,为进一步改进基于矛盾体分离演绎理论与方法,设计了C S E与E的结合版本C S E_E,并通过实验检验,证明了其性能要优于E的。紧接着,C a o等1 8进一步提出了2种新的基于优化证明搜索的多子句动态推导算法。随后,C a o等1 9将S-C S(S t a n d a r d C o n t r a d i c t i o n S e p a r a t i o n)规则与P r o v e r 9结合,提出了一种基于标准矛盾分离规则的新型一阶逻辑定理证明器,不仅提高了演绎能力,而且成功解决了1 0 3个 其 他 证 明 器 均 未 解 决 的 问 题。继 而,Z h o n g等2 0提出了一种新的多子句动态标准矛盾体分离推理规则及其自动推导理论,提升了证明器的效率。实验表明,矛盾体本身延拓了归结方法的优越性,且矛盾体与自动推理具有良好的适应性,因此,矛盾体在推动自动定理证明的发展中具有重要意义。在命题逻辑中,标准矛盾体与不可满足的命题逻辑公式等价1 5,例如MU(1)MU(2)等2 1皆为矛盾体,将其结构类型提供给证明器,能进一步提高证明效率。然而,到目前为止,针对矛盾体结构的研究较少,为了更好地发挥矛盾体的作用,需要提出矛盾体构造的有效方法。唐雷明等2 2研究了矛盾体的结构性质,总结出一些生成矛盾体的删除文字策略,但用删除文字策略生成新的矛盾体的效率较低,且得到的矛盾体结构简单,类型不够丰富。基于此,本文采用复合2个或多个矛盾体的部分子句的形式,提出一种新的矛盾体生成复合策略。根据矛盾体之间子句复合个数,分为单子句析取复合和多子句析取复合2部分进行研究。通过分析矛盾体的结构发现,单子句析取复合中,不需要添加新的子句即可生成矛盾体;而多子句析取复合中,则需要考虑复合子句中是否含有相同的命题变元等因素,再选择添加适当子句,生成新的矛盾体。同时,根据本文提出的多个复合策略及算法,通过实例分析,可以得到多个互异的矛盾体,展示了复合策略的有效性和多样性。以本文提出的理论作为依据,编写矛盾体的生成算法,为进一步在计算机上实现矛盾体的生成提供基础。下面给出相关预备知识:定义1(文字、子句、子句集2 3)在命题逻辑公式中,称原子公式及其否定为文字,有限多个文字的析取为子句,子句集S为S中所有子句合取构成的公式。定义2(合取范式2 3)有限多个子句的合取叫做合取范式,记为C1C2Cn,其中Ci是子句,i=1,2,n。定义3(互补对2 3)设p是一个原子,文字p和p称为一个互补对。定义4(不可满足性2 4)S是命题逻辑中的子句集,若存在一个赋值v,使得S在v下的真值为1,则子句集S是可满足的,否则子句集S是不可满足的。定义5(标准矛盾体1 5)设S=C1,C2,Cm 是子句集。如果对任意(p1,p2,p