经典命题逻辑公理系统定理证明算法设计

真诚为您提供优质参考资料，若有不当之处，请指正。Http:/ 逻辑与认知 Vol.2, No.4, 2004-收稿日期：2004-11-25；作者简介：杜国平，1965 年生，男，汉族，江苏盱眙人，南京大学副教授。基金项目：国家社科基金项目（02CZX008）；南京大学引进人才基金项目；南京大学笹川青年教育基金项目。联系方式：210093 南京大学哲学系 Email: dgpnju 电话：025-835971611经典命题逻辑公理系统定理证明算法设计杜国平 1，2（1. 南京大学哲学系 210093；2.南京航空航天大学计算机系 210016）内容提要：本文利用演绎定理的证明思路给出了一个由演绎证明构造公理证明的一般程序，并增加了一条简化命令，使该程序既严格又具有实际可操作性。关键词： 演绎证明 公理证明 程序中图分类号：B81 文献标识码：A在经典命题逻辑常见的公理系统中，仅仅从公理和推理规则出发进行定理的形式证明一般没有能行的程序，对于初学者而言是比较困难的。但是，在经典命题逻辑公理系统中，演绎定理成立，而使用演绎定理来构造定理的形式证明是比较简单的。实际上，演绎定理的证明过程已经表明：有了一个使用演绎定理的形式证明（简称为演绎证明），就可以构造出仅仅从公理和推理规则出发的形式证明（简称为公理证明）。本文拟对由演绎证明构造公理证明的具体算法和技巧进行一些探讨。为了说明的方便，我们取如下的命题逻辑公理系统PC 来进行讨论。系统 PC 由如下三条公理模式和一条推理规则构成：公理模式为：(Ax1) A (B A)(Ax2) (A (B C)(A B)(B C)(Ax3) (A B)(AB) A)推理规则即分离规则（Modus ponens）：由A和AB可以推出B。简记为MP。在系统 PC 中显然可以证明：演绎定理(DT )：如果S ， A + B，那么S + AB。因为任一证明序列都是有限长的，因此，演绎证明中需要引入的假设也是有限的。所以我们只考虑假设集S 为有限集的情况，令 1 2 1 , , , , m m A A A A - S = L 。假设有一个 0 SU A + B的演绎证明，该证明的公式序列为： 1 2 , , , n C C L C = B。那么我们可按照下述程序构造出一个S + 0A B的演绎证明。经典命题逻辑公理系统定理证明算法设计21 如果A0 Cn是公理或者0 n A C S，则执行如下子程序1，即直接写入：0 n A C2 如果n C 是公理，则执行如下子程序2 ：n C0( ) n n C A C0 n A C3 如果n C 是0 A ，则执行如下子程序3 ：0 0 0 A (B A ) A )0 0 0 0 0 0 0 (A (B A ) A )(A (B A )(A A )0 0 0 0 (A (B A ) (A A )0 0 A (B A )0 0 A A4 如果n k C = A S，k 1, 2, L , m，则执行如下子程序4 ：k A0( ) k k A A A0 k A A5 如果n C 是由i C ， ( ) ( , 1, 2, , 1) j i n C = C C i j L n - 经使用分离规则而得到，则对j C 执行如下子程序5 ：0 0 0 ( ( ) ( ) ( ) i n i n A C C A C A C0 0 ( ) ( ) i n A C A C0 n A C6 对4中出现的i C ， j C 重复执行程序16。7 若程序全部进入14，则执行完1 4 ，程序终止。对 S + 0A B 反复使用上述程序m 次之后， 就可以得到一个+ 1 1 0 ( ( ( ) ) m m A A A A B - L L 的公理证明。例 1 在系统PC中构造定理+ (A B)C)(BC)的公理证明。首先，我们构造一个(A B)C), B + C的演绎证明。证明1 ：1 (A B) C 假设2 B 假设3 B(A B) (Ax1)4 AB 2、3 MP5 C 1、4 MP其次，由(A B) C，B + C的演绎证明构造(A B) C+ BC的演绎证明。1、这可以通过回溯检查逐步完成。证明1的第5 行为C，进入程序1检查BC，发现它既不是公理也不属于假设集(A B)C)；进入程序25发现C由第1、4行(A B) C和AB分离而得。因此，执行子程序5：逻辑与认知 Vol. 2, No.4, 20043(B (A B)C)(B(A B)(B C)(B (AB)(BC)BC2、进入程序6，对(A B) C和AB执行程序16。3、进入程序1，检查B(A B)C) ，发现它既不是公理也不属于假设集(A B)C)；进入程序25发现(A B) C属于假设集(A B)C)。因此，执行子程序4 ：(A B) C(A B)C)(B (A B)C)B(A B)C)4、进入程序1，检查B(A B)，发现它是公理。因此，执行子程序1：B(A B)5、程序已经全部进入14，并且已经执行完子程序1 4 ，因此程序终止。所以我们得到一个(A B) C+ BC的演绎证明。证明1 ：1 (A B) C 假设2 (A B)C)(B (A B)C) (Ax1)3 B(A B)C) 1、2 MP4 B(A B) (Ax1)5 (B (A B)C)(B(A B)(B C) (Ax2)6 (B (AB)(BC) 3、5 MP7 BC 4、6 MP再次，由(A B) C+ BC的演绎证明构造+ (A B)C)(BC)的公理证明。1、进入程序1 检查(A B)C)(BC)，发现它不是公理（此时，因为假设集是空集，所以它也当然不属于假设集）；进入程序25发现BC由第4、6 行B(A B)和(B (AB)(BC)分离而得。因此，执行子程序5：(A B)C)(B(A B)(B C)(AB)C)(B(A B)(A B)C)(B C)(A B)C)(B(A B)(A B)C)(BC)(A B)C)(BC)2、进入程序6，对B(A B)和(B (AB)(BC)执行程序16。3、进入程序1，检查(A B)C) (B (A B)，发现它不是公理；进入程序25发现B(A B)是公理。因此，执行子程序2 ：B(A B)经典命题逻辑公理系统定理证明算法设计4(B (AB)(A B)C)(B(A B)(A B)C) (B (A B)4、进入程序1 检查(A B)C)(B(A B)(B C)，发现它不是公理；进入程序25发现(B (AB)(BC)由第3、5行B(A B)C)和(B (A B)C) (B(A B)(B C) 分离而得。因此，执行子程序5 ：(A B)C)(B(A B)C) (B(A B)(B C)(A B)C)(B (A B)C)(A B)C)(B(A B)(B C)(A B)C)(B (AB)C)(A B)C)(B(A B)(B C)(A B)C)(B(A B)(B C)5 、进入程序6 ， 对B(A B)C) 和(B (A B)C)(B(A B)(B C) 执行程序16。6、进入程序1，检查(A B)C)(B (A B)C)，发现它是公理。因此，执行子程序1 ：(A B)C)(B (A B)C)7 、进入程序1 ， 检 查 (A B)C) (B(A B)C)(B(A B)(BC) ， 发现它不是公理； 进入程序2 5 发现(B (A B)C)(B(A B)(B C)是公理。因此，执行子程序2 ：(B (A B)C)(B(A B)(B C)(B(A B)C)(B(A B)(B C)(A B)C)(B(A B)C)(B(A B)(BC)(A B)C)(B(A B)C)(B(A B)(BC)8、程序已经全部进入14，并且已经执行完子程序1 4 ，因此程序终止。这样我们就得到一个+ (A B)C)(BC)的公理证明。证明1 ：1 (A B)C)(B(A B)C) (Ax1)2 (B (A B)C)(B(A B)(B C) (Ax2)3 (B(A B)C)(B(A B)(B C)(A B)C)(B(A B)C)(B(A B)(BC) (Ax1)4 (A B)C)(B(A B)C)(B(A B)(BC) 2、3 MP5 (A B)C)(B(A B)C) (B(A B)(B C)(A B)C)(B (A B)C)(A B)C)(B(A B)(B C) (Ax2)逻辑与认知 Vol. 2, No.4, 200456 (A B)C)(B (AB)C)(A B)C)(B(A B)(B C) 4、5 MP7 (A B)C)(B(A B)(B C) 1、6 MP8 (A B)C)(B (A B)(BC)(AB)C)(B(A B)(A B)C)(B C) (Ax2)9 (A B)C)(B(A B)(A B)C)(BC) 7、8 MP10 B (A B) (Ax1)11 (B (AB)(A B)C)(B(A B) (Ax1)12 (A B)C) (B (A B) 10、11 MP13 (A B)C)(BC) 9、12 MP构造程序的27也可以构成一个独立的公理证明构造程序，这是演绎定理的证明中显示出来的，但该程序很繁琐。程序1是一个简化程序，它的加入，可以使构造程序大为简化，尽管它多了一条程序命令。但是这样就增加了该程序的实际可操作性。参考文献：1 宋文坚. 逻辑学M. 人民出版社,1998. P86-92.2 陆钟万. 面向计算机科学的数理逻辑M. 科学出版社,2002. P86-92.3 周礼全. 逻辑百科辞典M. 四川教育出版社,1994. P685.4 A.G.Hamilton. Logic for MathematiciansM. 清华大学出版社,2003. P32-34.5 张清宇 郭世铭 李小五. 哲学逻辑研究M. 社会科学文献出版社,1997.The Arithmetic Design for Theorem Provingin the Axiom System of Classical Propositional LogicDu Guo-ping1,2(1.Nanjing University. Nanjing 210093,China; 2.Nanjing University of Aeronautics andAstronautics, Nanjing 210016,China)Abstract: The article uses the proving of deduction theorem to give general program ofconstruction theorem proving, and adding a piece of simplification command. Theprogram is gotten strict and exercisable.Key words: deduction prove; axiom prove; program5 / 5