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