基于语义tableau的一阶逻辑自动定理证明

1、!""#$!计算机工程与应用基于语义 !"#$%& 的一阶逻辑自动定理证明刘全孙吉贵"!苏州大学计算机科学与技术学院"苏州 #"$%&#!吉林大学计算机科学与技术学院"长春 !%"($)*+,-./01,2.-13415,6751682摘要自动推理作为自动定理证明的扩展是人工智能研究的基础工作" 许多重要的人工智能系统都是以推理系统为其核心部分9其中的 :,;.7,1 方法"由于具有通用性%直观性及易于计算机实现等特点"至今成为重要的自动推理方法之一& 在 :,

2、;.7,1 方法基础上"讨论了一阶逻辑中的自动定理证明理论"提出使用模型存在定理证明其可靠性和完备性的方法& 同时也给出了带等词 :,;.7,1 方法的证明过程&关键词语义 :,;.7,1有效性完备性文章编号 %""!&(%&!""#$!&%(*%!文献标识码 )中图分类号 <=">(!)*&!%+ ,-%).%* /.)0123 4&5%+ )2 6%*&2!17 ,&#$%&12 81.5!9:.+%. ;)317;1 <&

3、amp;262 =131!?24:-:1:7 A B+C1:7D E8-7287 ,25 <78F2.GH"E8FI J2-K7D4-:H"E1LF1 (M$%&#(!B.7G7 A B+C1:7D E8-7287 ,25 <78F2.GH"N-.-2 J2-K7D4-:H"BF,2G8F12 M!O%"($(#5!.&7!> P1:+,:75 57518:-2 IF-8F -4 7Q:724-2 : ,1:+,:75 :F7D7+ CDK-2G -4 , ;,4-8 IDR A ,D:-A-8-,.-2:7.

4、-G7287ST,2H -+CD:,2: 4H4:7+4 A ,D:-A-8-,. -2:7.-G7287 D7G,D5 57518:-2 4H4:7+ ,4 8D7 C,D:S<5,H :,;.7,1 +7:F5F,4 ;78+7 27 A :F7 +,-2 57518:-24"78,147 -: -4 12-K7D4,. ,25 -2:1-:-2-4:-8",25 7,4H : ;7 -+C.7+72:75SU,4752 :,;.7,1 :F7 :F7D-74 A ,1:+,:75 :F7D7+ CDK-2G -2 A-D4:*D57D .G-8 ,D7 5-48

5、14475SVD CDK-2G :F7 41252744 ,25:F7 8+C.7:72744":F7 +7:F54 A :F7D7+ CDK-2G 14-2G :F7 +57. 7Q-4:7287 :F7D7+ ,D7 CD7472:75S?2 :F7 +7,2 :-+7":F-4 C,C7D 4FI4 CDA CD8751D7 A :,;.7,1 I-:F 701,.-:HS?%A).+5% 47+,2:-8 :,;.7,1"41252744"8+C.7:72744基金项目!国家自然科学基金&编号%&%(W!%>%"&

6、amp;%XW!%!$资助作者简介!刘全&%*+*$"男"博士"副教授"研究方向为智能信息处理"自动推理"地理信息系统 孙吉贵!%*+(*$"男"博士"教授"博士生导师"研究方向为人工智能"自动推理"引言研究证明理论通常的方法有多种" 不同的方法对于不同的逻辑系统处理能力各有优劣" 其中的归结法和语义 :,;.7,1法适合于自动推理"归结法与合取范式或子句的形式相联系"语义 :,;.7,1 法与析取范式或对偶子句的形式

7、密切相关 归结法对于经典逻辑非常有效"但对于非经典逻辑却存在困难"对于不同的逻辑需构造不同的归结过程" 因此本文讨论自动定理证明主要采用 :,;.7,1"按照文献Y%Z的方法"研究语义 :,;.7,1的证明过程语义 :,;.7,1 由 U7:F!M$(-2:-RR,!M$引入的 <,;.7,1是按照某种规则在有向二叉树的每个节点上都标记有一个合式公式而构成 换句话说"通过引入相应的谓词公式"将二元关系的性质用逻辑公式表示出来"对于不同的逻辑系统"只是对公式构造集进行扩展 因此"这种方法有较

8、强的通用性和直观性"并易于计算机实现自动推理(:,;.7,1 扩展规则:,;.7,1 方法中":,;.7,1 的扩展规则如下/规则 M 合取规则! 规则$!"!#!$"!"!$"$!"!%"$"!"""!规则 ! 析取规则!" 规则$"!&!$"!#"!$""!%"!"""!"!规则 ( 否定规则""!"("(规则 ,

9、全称规则!# 规则$对于 #$%&中的任意项 "有%!)($()"!*($"$()规则 # 存在规则!% 规则$对于新的参数 $"有%"!)($"$()$!*($()$(计算机工程与应用 !""#$!"#$%&( 证明过程定义 ) 令*!)!+!"!",为公式的有限集合#$)%下面一个分枝树为*!)!+!"!",的一个 "#$%&#(-!)!+!"$+%如果 # 为*!)!+!"!",的一个 "

10、;$%&(!且 $% 为 $ 采用 "$%&( 扩展规则后的结果!那么 $% 是*!)!+!"!",的一个 "$%&(#定义 + 一个 "$%&( 的一个分枝 ! 被称为封闭的! 如果 &和"& 出现在其上!或#出现在 ! 上# 如果 和"! 出现在 !上(其中 ! 为原子或者#!那么被称为原子封闭!如果每个分枝都为$原子%封闭.那么 "$%&( 为$原子%封闭#定义 / & 的 "$%&( 证明对于*"&,是一个封

11、闭的 "$%&(!如果 & 有一个 "$%&( 证明! 那么 & 为 "$%&( 系统的一个定理!表示为$)*&#定义 0 一个 "$%&( 是严格的! 如果在它的构建过程中!在同一分枝上!一条表扩展规则在其上只作用一次#定义 1 令 +$,!-!.%为一语言!简记为 /# 令 )01 为一个常量符号的可数集合!与 2 不相交!称集合的成员为 )01 参数#/$,!-!2%)01%简记为 /)01#下面为$&3%24$3%5$3%3(2$)3%4$3%$&3%5$3%3的"

12、$%&( 证明过程$)%"*$&3%24$3%5$3%3(2$)3%4$3%$&3%5$3%3,$+%$&3%24$3%5$3%3$/%"2$)3%4$3%$&3%5$3%3$0%"$)3%4$3%$1%"$&3%5$3%$4%"5$6%$5%"4$6%$6%4$6%5$6%$7%4$6%$)8%5$6%说明&这里$)%为被证明公式的否定$+%和$/%来自$)%使用规则 " $0%和$1%来自$/%使用规则 "$4%来自$1%使用规则 #!6 为一新参数$5%

13、来自$0%!$6%来自$+%使用规则 $!允许使用 +)01任何封闭项#0"$%&( 证明的有效性和完备性定义 4 "$%&( 分枝是可满足的! 如果在其上公式集是可满足的# 一个 "$%&( 是可以满足的!如果某一分枝是可以满足的#引理 ) 令 7 为公式集!并且 $ 和 % 为公式#$)%如果 7%*$,是可满足的!那么 7%*$!$*%,对于任意封闭项 * 也是可满足的#$+%如果 7%*%,是可满足的!那么 7%*%!%$)%,对于任意对7 和 % 是新的常量符号 ) 也是可满足的#证明&$)%假设在模型 89:;!<

14、9中!7%*$,是可满足的# 只要证明在同一模型下 7%*$( $*%,是可以满足的#因为 $ 在模型中为真!因此$&3%$3%也为真!这里 3 对 $来说也是新变量!那么对任何赋值 =!2$3%3<!=为真# 现在!令 =为一个赋值!使得 3=9*<!可得2$*%3<!=:2$*3>*,3<!=:2$3%3<!=:*!即7%*$!$*%,在模型 89;!<9中是可以满足的#$+%假设在模型 89:;!<?中!7%*%,可满足的# ) 对 7 和 %为新的常量符号!只要证明在任意模型下 7%*%!%$)%,是可以满足的#因为 % 在模型中

15、为真(因此$)3%$3%$3 对于 % 是新的%和2%$3%3!=对于某一赋值 = 也为真#构造新的模型 8%9:;!A9!有同样的定义域!一个解释 A 除了 ) 外与 完全相同!作为特例设 )A93=!因此这两个模型只是在常量符号 ) 处不同!这样 7%*%,在模型 8% 中是可以满足的!且2%$3%3A!=也是真的# 又因 3=:)A!有2%$3%3A!=92%*3>),3A!=:2%$3%3A!=:*#因此 7%*%!%$)%,在 8% 中是可以满足的!因此在 8 中也是可以满足的#引理 ! 如果任何 "$%&( 扩展规则被应用到可满足的表!其结果为另一个可满足的

16、表#证明&假设 $ 是一个可满足的 "$%&(!对于 $ 的分枝 ! 应用表扩展规则产生 &!生成一个 "$%&( $%# 下面证明 $% 也是可以满足的#因为 $ 是可以满足的!$ 至少有一个可满足的分枝! 选择这一分枝!记为 &#$)%&*!# 规则应用到 ! 上!& 仍为 $% 的分枝!因此 $% 是可以满足的#$+%&9!#! 本身是可满足的!布尔赋值 将 ! 中的所有公式映射为 *#!&9"# 那么 ! 被扩展为 ") 和 "+ 而产生 $%# 由于 "

17、 产生在 ! 上!有 $"%9*!$"%!$")%+$"+%!因此 必将 $")%和$"+%都映射为 *# 这样 将在 "% 的 ! 扩展的每个公式都映射为 *!因此 $% 是可以满足的#"&9(# 那么将左右儿子加到 ! 的最后节点上!标记为 ()和 (+!而产生 $%!由于 ( 产生在 ! 上!$(%9*!但 $(%!$(%$(!%! 将 (% 或 (+ 映射为 *! 将左侧或右侧的扩展分枝映射为 *# 只要存在其一!$% 就有可满足的分枝!因此 $% 是可以满足的#其它情况&& 是&q

18、uot;"B!",或"#!易证 $% 是可以满足的#另外!含量词的两种情况!引理 % 已证#定理 ) 如果公式集 7 存在一个 "$%&(! 那么 7 是不可满足的#证明&假设公式集 7 存在一个 "$%&(!7 是可满足的#对 7 构造一个开始于 7 封闭的 "$%&(! 由于 7 是可满足的!那么初始标记为 7 的 "$%&( 是可满足的!根据引理 +!7 的"$%&( 的 每 个 子 "$%&( 都 是 可 满 足 的! 包 括 最 后 封 闭

19、 的"$%&(!这显然是矛盾的!因此!7 是不可满足的#定理 + $有效性%如果 & 有一个 "$%&( 证明!那么 & 是有效的#证明&假设 & 有一个 "$%&( 证明但是无效的#我们推出矛盾#由于 & 是无效的!因此有一个模型使得"& 为真!对 & 的"$%&( 证明开始于标有"& 的一个分枝! 并且是可满足的"$%&(# 由引理 + 可知!每个后继 "$%&( 都是可满足的!包括最后的封闭的 &q

20、uot;$%&(#但封闭的 "$%&( 不能是可满足的#因此推出矛盾# 所以如果 & 有一个 "$%&( 证明!那么 & 是有效的#+/!""#$!计算机工程与应用定义 % 对于语言 ! 的模型 "#$%!&是 "#$%$&( 模型!如果"#)$% 是 ! 的项集%&*$对于每个项 (!(&#(定义 & 令 ! 为某一一阶语言! 的子句集 ) 称为一阶"+,+-& 集!如果"#.(对于任何命题字母 */ *!) 和&q

21、uot;*!) 不同时存在&0(#$)!"%$)%&!(""+&)+&)%&1(!&)!)&) 且 !0&)%&2("&)".&) 或 "0&)%&3(对于 ! 的每一个封闭项 (!#&)#&(&)%&4(对于 ! 的某一个封闭项 (!$&)$&(&)引理 &"+,+-& 引理(假设 ! 为含非空封闭项集合的语言!如果 ) 为一个一阶 "+,

22、+-& 集!那么在一个 "#$%$&( 模型中 ) 是可以满足的$定义 5 令 ! 为一阶语言! 令 , 为 !-./子句集合的集合!我们称 , 具有一阶相容性!如果对于每个 0&,"&.(对于任何命题字母 *!*&0 和"*&0 不同时存在%&0(#$0!"%$0%&!(""+&00(6+7&,%&1(!&00(6!.!*7&,%&2("&00(6".7&, 或 0(6"*7&

23、amp;,%&3(对于每一个 !-./封闭项 (!#&)#&(&)%&4(对于某一 !-./的参数 -!$&)$&(&)定理 ! &一阶模型存在定理(如果 , 具有一阶相容性!0 为! 的公式集!并且 0&,!那么 0 是可以满足的根据相容性的定义可证定义 .8 !-./子句的有限集合 0 是表相容的! 如果对 0 没有封闭的 ,&%9#&:引理 1 所有表相容集合的集合是一阶相容性证明"这里只证 " 情况假设 0 为 !-./句子的有穷集!"&0!但 0(6&

24、quot;.7和 0(6"!7都不是 ,&%9#&: 相容的!我们证明 0 也不是 ,&%9#&: 相容的由于 0(6".7不是 ,&%9#&: 相容的!因此有一个封闭的 ,&%;9#&:!称其为 1. 对于 0(6"!7同样有一个封闭的 ,&%9#&:!称其为 1! 这些 ,&%9#&: 过程中可能通过 $ 规则引入一个参数!需作如下假设"假设 1 是一个 ,&%9#&:!2 是其中引用的一个参数!且 3 是一个在 1 中没出现的参数 令 1

25、4 与 1 除了用 3 代替 1中出现的 2 以外!其它完全一样如果 1 封闭!那么 14 也封闭这样 1. 和 10 结合在一起产生一个封闭的 ,&%9#&:!如下"0<6"!5.!)!567"5.)56!"."0将左分枝的 ,&%9#&: 1. 和右分枝的 ,&%9#&: 1! 联系在一起!对 0 产生一个封闭的 ,&%9#&:定理 1 #一阶 ,&%9#&: 的完备性(如果 ! 的子句 5 是有效的!5 有一个 ,&%9#&: 证明证明&

26、quot;对于6"57如果没有一个 ,&%9#&: 证明!即没有封闭的 ,&%9#&:!那么6"57是 ,&%9#&: 相容的!因此满足一阶模型存在定理!且 5 是无效的2含等词的 ,&%9#&: 证明定义 .相等规则自反规则 句子 (*( 加到子句集 0 的 ,&%9#&: 的任何一个分枝末尾产生另一个 ,&%9#&:这里 ( 是 !-./的任何项直观表示为"(*(替换规则 如果 (*7 和 %#(产生在 0 的 ,&%9#&: 分枝上!%#7(被加到 ,&%9#&: 后!产生另一个 ,&%9#&: 这里 ( 和 7 是 !-./的任何封闭项(*7%#(%#7(例如"#.("#+8(#+9(#+:(#8*9,9*:(8*:(#0("#+9(#+:(#.*9,9*:(.*:(#!("#+:(#.*;,;*:(.*:(#1("#.*;,;*2(.*2(#2(.*;,;*2#3("