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

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

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))((AB)(B C))

(Ax3)(AB)((AB)A)

推理规则即分离规则（Modus ponens）：由A和AB可以推出B。简记为MP。

在系统 PC 中显然可以证明：

演绎定理(DT)：如果，A + B，那么+ AB。

因为任一证明序列都是有限长的，因此，演绎证明中需要引入的假设也是有限的。所以 我们只考虑假设集为有限集的情况，令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 ((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 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 jL 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中构造定理+((AB)C)(BC)的公理证明。

首先，我们构造一个((AB)C), B + C的演绎证明。

证明1' ：(AB)C 假设B 假设B(AB)(Ax1)AB 2、3 MPC 1、4 MP

其次，由(AB)C，B + C的演绎证明构造(AB)C+ BC的演绎证明。

1、这可以通过回溯检查逐步完成。证明1'的第5 行为C，进入程序[1]检查BC，0 0 0

发现它既不是公理也不属于假设集((AB)C)；进入程序[2]～[5]发现C由第1、4 行(AB)C和AB分离而得。因此，执行子程序[5']：

逻辑与认知 Vol.2, No.4, 200

4(B ((AB)C))((B(AB))(B C))

(B (AB))(BC)

BC2、进入程序[6]，对(AB)C和AB执行程序[1]～[6]。

3、进入程序[1]，检查B((AB)C)，发现它既不是公理也不属于假设集

((AB)C)；进入程序[2]～[5]发现(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、程序已经全部进入[1]～[4]，并且已经执行完子程序[1'] ～[4']，因此程序终止。所以我们得到一个(AB)C+ BC的演绎证明。

证明1'' ：(AB)C 假设((AB)C)(B ((AB)C))(Ax1)B((AB)C)1、2 MPB(AB)(Ax1)(B ((AB)C))

((B(AB))(B C))(Ax2)(B (AB))(BC)3、5 MPBC 4、6 MP

再次，由(AB)C+ BC的演绎证明构造+((AB)C)(BC)的公

理证明。

1、进入程序[1] 检查((AB)C)(BC)，发现它不是公理（此时，因为假

设集是空集，所以它也当然不属于假设集）；进入程序[2]～[5]发现BC由第4、6 行 B(AB)和(B (AB))(BC)分离而得。因此，执行子程序[5']：

(((AB)C)((B(AB))(B C)))

((((AB)C)(B(AB)))

(((AB)C)(B C)))

(((AB)C)(B(AB)))

(((AB)C)(BC))

((AB)C)(BC)

2、进入程序[6]，对B(AB)和(B (AB))(BC)执行程序[1]～[6]。

3、进入程序[1]，检查((AB)C)(B(AB))，发现它不是公理；进入程 序[2]～[5]发现B(AB)是公理。因此，执行子程序[2'] ：

B(AB)

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

(B (AB))(((AB)C)(B(AB)))

((AB)C)(B(AB))

4、进入程序[1] 检查((AB)C)((B(AB))(B C))，发现它不是 公理；进入程序[2]～[5]发现(B (AB))(BC)由第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 ((AB)C)))

(((AB)C)((B(AB))(B C))))

((AB)C)((B(AB))(B C)))、进入程序[6]，对B((AB)C)和(B ((AB)C))

((B(AB))(B C))执行程序[1]～[6]。

6、进入程序[1]，检查((AB)C)(B ((AB)C))，发现它是公理。因 此，执行子程序[1'] ：

((AB)C)(B ((AB)C))、进入程序[1]，检 查((AB)C)((B((AB)C))

((B(AB))(BC)))，发现它不是公理； 进入程序[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))(BC))))

((AB)C)((B((AB)C))

((B(AB))(BC)))

8、程序已经全部进入[1]～[4]，并且已经执行完子程序[1'] ～[4']，因此程序终止。这样我们就得到一个+((AB)C)(BC)的公理证明。

证明1''' ：((AB)C))(B((AB)C))(Ax1)(B ((AB)C))((B(AB))(B C))(Ax2)((B((AB)C))((B(AB))(B C)))

(((AB)C)((B((AB)C))

((B(AB))(BC))))(Ax1)((AB)C)((B((AB)C))

((B(AB))(BC)))2、3 MP(((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, 200

46(((AB)C))(B ((AB)C)))

(((AB)C)((B(AB))(B C))))4、5 MP((AB)C)((B(AB))(B C)))1、6 MP(((AB)C)((B (AB))(BC))))

((((AB)C)(B(AB)))

(((AB)C)(B C)))(Ax2)(((AB)C)(B(AB)))

(((AB)C)(BC))7、8 MPB (AB))(Ax1)(B (AB)))

(((AB)C)(B(AB)))(Ax1)((AB)C)(B(AB))10、11 MP((AB)C)(BC)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 Classical 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

第二篇：证明、公理、平行线性质定理

证明的必要性、公理与定理、平行线的判定（公）定理、平行线的性质（公）定理

基础知识1.证明：

2.公理：3.定理:

4.等量代换：公理：

5.平行线的判定定理：定理：公理

6.平行线的性质定理定理:基础习题 1.下列说法正确的是（）

A.所有的定义都是命题B.所有的定理都是命题

C.所有的公理都是命题D.所有的命题都是定理 22.若P（P5）是一个质数，而P1除以24没有余数，则这种情况（）

A.绝不可能B.只是有时可能

C.总是可能D.只有当P=5时可能

3.下列关于两直线平行的叙述不正确的是()

A.同位角相等,两直线平行；B.内错角相等,两直线平行毛

C.同旁内角不互补,两直线不平行；D.如果a∥b,b⊥c,那么a∥c 14.如左图，下列说法错误的是（）lllll3A、∵∠1＝∠2，∴3∥4B、∵∠3＝∠4，∴3∥4 lllll4C、∵∠1＝∠3，∴3∥4D、∵∠2＝∠3，∴1∥2 ll55.已知：如图，下列条件中，不能判断直线1∥2的（）l1A、∠1＝∠3B、∠2＝∠

3C、∠2＝∠4D、∠4＋∠5＝180 6.若两条平行线被第三条直线所截，则下列说法错误的（）l

2A、一对同位角的平分线互相平行B、一对内错角的平分线互相平行

C、一对同旁内角的平分线互相平行D、一对同旁内角的平分线互相垂直

7.如图，AB∥CD，∠α＝（）BAA、50°B、80°C、85°D、95° C8.已知∠A＝50°，∠A的两边分别平行于∠B的两边，则∠B＝（）AB

A、50°B、130°C、100°D、50°或130° 9.如图，AB∥CD，AD、BC相交于O，∠BAD＝35°，∠BOD＝76°，则∠C的度数是（）A、31°B、35° C、41°D、76°

填空

10.如图，（1）如果AB∥CD，必须具备条件∠______＝∠________，D根据是____________________。（2）要使AD∥BC，必须具备条件∠______＝∠________，根据是

4____________________。B

11.如图，给出了过直线外一点作已知直线的平行线的方法，其依据是________。

D12.如图，已知∠1＝30°，∠B＝60°，AB⊥AC。（1）计算：∠DAB＋∠B=

（2）AB与CD平行吗？（）AD与BC平行吗？（）B

简答题：

13.如图，已知∠ADE＝60°，DF平分∠ADE，∠1＝30°，求证：DF∥BE 证明：∵DF平分∠ADE（已知）A 1∴________=∠ADE（）

2∵∠ADE＝60°（已知）D∴_________________＝30°（）

∵∠1＝30°（已知）

∴____________________（）BC∴____________________（）

14.已知：如图，∠B=∠C.(1)若AD∥BC，求证：AD平分∠EAC；

(2)AD平分∠EAC，求证：AD∥BC.15、如图，已知DE∥BC，CD是∠ACB的平分线，∠B＝70°，∠ACB＝50°，求∠EDC和∠BDC的度数.能力提升

16.（1）如图（1），AB∥EF.求证：（1）∠BCF=∠B+∠F.（2）当点C在直线BF的右侧时，如

图（2），若AB∥EF，则∠BCF与∠B，∠F的关系如何？请说明理由.D

BC

第三篇：armstrong公理系统证明

 Armstrong公理系统的证明

① A1自反律：若Y X U，则X→Y为F所蕴含

证明1

设Y X U。

对R的任一关系r中的任意两个元组t,s：

若t[X]=s[X]，由于Y X，则有t[Y]=s[Y]，所以X→Y成立，自反律得证。

② A2增广律：若X→Y为F所蕴含，且Z U，则XZ→YZ为F所蕴含

证明2

设X→Y为F所蕴含，且Z U。

对R的任一关系r中的任意两个元组t,s：

若t[XZ]=s[XZ]，由于X XZ，Z XZ，根据自反律，则有t[X]=s[X]和t[Z]=s[Z]；

由于X→Y，于是t[Y]=s[Y]，所以t[YZ]=s[YZ]；所以XZ→YZ成立，增广律得证。

③ A3传递律：若X→Y，Y→Z为F所蕴含，则X→Z为F所蕴含

证明3

设X→Y及Y→Z为F所蕴含。

对R的任一关系r中的任意两个元组t,s：

若t[X]=s[X]，由于X→Y，有t[Y]=s[Y]；

再由于Y→Z，有t[Z]=s[Z]，所以X→Z为F所蕴含，传递律得证。

④ 合并规则：若X→Y，X→Z，则X→YZ为F所蕴含

证明4

因X→Y（已知）

故X→XY（增广律），XX→XY即X→XY

因X→Z（已知）

故XY→YZ（增广律）

因X→XY，XY→YZ（从上面得知）

故X→YZ（传递律）

⑤ 伪传递规则：若X→Y，WY→Z，则XW→Z为F所蕴含

证明5

因X→Y（已知）

故WX→WY（增广律）

因WY→Z（已知）

故XW→Z（传递律）

⑥ 分解规则：若X→Y，Z Y，则X→Z为F所蕴含

证明6

因Z Y（已知）

故Y→Z（自反律）

因X→Y（已知）

故X→Z（传递律）

第四篇：命题与证明之公理定理

公理和定理

教学要求：了解公理与定理到概念，以及他们之间的内在联系；了解公理与定理都是真命题，它们都是推理论证的依据；掌握教材十条公理和已学过的定理。

重点难点

十条公理和已学过的定理。

一 选择题（每小题5分，共25分）下面命题中：

（1）旋转不改变图形的形状和大小，（2）轴反射不改变图形的形状和大小

（3）连接两点的所有线中，线段最短，（4）三角形的内角和等于180°

属于公理的有（）

A1个B2个C3个D4个下面关于公理和定理的联系说法不正确的是（）

A 公理和定理都是真命题，B公理就是定理，定理也是公理，C 公理和定理都可以作为推理论证的依据D公理的正确性不需证明，定理的正确性需证明 3推理：如图∵ ∠AOC=∠BOD，∴∠AOC+∠AOB=∠BOD+∠AOB,这个推理的依据是（）

A 等量加等量和相等，B等量减等量差相等C 等量代换 D 整体大于部分推理：如图：∵∠A=∠ACD,∠B=∠BCD,(已知)∴AD=CD,CD=DB(等腰三角形的性质)AD=DB()

括号里应填的依据是（）

A 旋转不改变图形的大小 B

C等量代换 D 5（）

A 两条直线被第三条直线所

截，若同位角相等，则这两条 直线平行

B 线段垂直平分线上的点到线段 4题图 两个端点的距离相等 3题图

C平行四边形的对角线互相平分

D对顶角相等

∴

二 填空题（每小题5分，共25分）人们在长期实践中总结出来的公认的真命题，作为证明的原始依据，称这些真命题为____运用基本定义和公理通过推理证明是真的命题叫_______;

7定理： “直角三角形两直角边的平方和等于斜边的平方”的逆定理是：___________________ _______________________________________;____________________________________________________是定理“两条直线被第三条直线所截，如果同旁内角互补，那么这两条直线平行”的逆定理如图，Rt△ABC沿直角边BC所在的直线向右平移得到△DEF，下面结论中

（1）△ABC≌△DEF,（2）∠DEF=90°，(3)AC=DF(4)AC∥DF(5)EC=CF 正确的是______________(填序号)，你判断的依据是_______________________________________要使平行四边形ABCD成为一个菱形，需要添加一个条件，那么你添加的是 _____________,依据是______

三 解答题（3×12+14=50分）11 仔细观察下面推理，填写每一步用到的公理或定理 如图：在平行四边形ABCD中，CE⊥AB，E

为垂足，如果∠A=125°，求∠BCE

解：∵四边形ABCD是平行四边形(已知)

∴AD∥BC（）∵∠A=125°（已知）∴∠B=180°-125°=55°（）

∵△BEC是直角三角形（已知）∴∠BCE=90°-55°=35°()如图将△AOB绕点O逆时针旋转90°，得到△A’OB’若A点

11题图

A

D

D

BE

CF

B

C

9题图

10题图

为（a,b）,则B点的坐标

为

（13题图），你用到的依.据是________________________________________________

13如图所示，在直角坐标系xOy中，A(一l，5)，B(一3，0)，C(一4，3)．根据轴反射的定义和性质完成下面问题：(1)在右图中作出△ABC关于y轴的轴对称图形△A′B′C′；(2)写出点C关于y轴的对称点C′的坐标

14如图，在四边形ABCD中，AB=AD，BC=DC，AC、BD相交于O，用所学公理、定理、定义说明（1）△ABC≌△ADC,(2)OB=OD,AC⊥BD

第五篇：初中几何证明的所有公理和定理

初中几何证明的所有公理和定理

1过两点有且只有一条直线两点之间线段最短同角或等角的补角相等

同角或等角的余角相等过一点有且只有一条直线和已知直线垂直 直线外一点与直线上各点连接的所有线段中，垂线段最短 平行公理 经过直线外一点，有且只有一条直线与这条直线平行如果两条直线都和第三条直线平行，这两条直线也互相平行 同位角相等，两直线平行

内错角相等，两直线平行同旁内角互补，两直线平行

12两直线平行，同位角相等两直线平行，内错角相等

两直线平行，同旁内角互补定理 三角形两边的和大于第三边；

推论 三角形两边的差小于第三边三角形内角和定理 三角形三个内角的和等于180°推论1 直角三角形的两个锐角互余 推论2 三角形的一个外角等于和它不相邻的两个内角的和推论3 三角形的一个外角大于任何一个和它不相邻的内角全等三角形的对应边、对应角相等

22边角边公理 有两边和它们的夹角对应相等的两个三角形全等角边角公理 有两角和它们的夹边对应相等的两个三角形全等推论 有两角和其中一角的对边对应相等的两个三角形全等边边边公理 有三边对应相等的两个三角形全等 斜边、直角边公理 有斜边和一条直角边对应相等的两个直角三角形全等定理1 在角的平分线上的点到这个角的两边的距离相等 定理2 到一个角的两边的距离相同的点，在这个角的平分线上角的平分线是到角的两边距离相等的所有点的集合等腰三角形的性质定理 等腰三角形的两个底角相等

推论1 等腰三角形顶角的平分线平分底边并且垂直于底边

等腰三角形的顶角平分线、底边上的中线和高互相重合33 推论3 等边三角形的各角都相等，并且每一个角都等于60°

等腰三角形的判定定理：如果一个三角形有两个角相等，那么这两个角所对的边也相等（等角对等边）

推论1 三个角都相等的三角形是等边三角形

推论 2 有一个角等于60°的等腰三角形是等边三角形

在直角三角形中，如果一个锐角等于30°那么它所对的直角边等于斜边的一半

直角三角形斜边上的中线等于斜边上的一半

定理 线段垂直平分线上的点和这条线段两个端点的距离相等

逆定理到一条线段两个端点距离相等的点，在这条线段的垂直平分线上

线段的垂直平分线可看作和线段两端点距离相等的所有点的集合

定理1 关于某条直线对称的两个图形是全等形

定理 2 如果两个图形关于某直线对称，那么对称轴是对应点连线的垂直平分线

44定理3 两个图形关于某直线对称，如果它们的对应线段或延长线相交，那么交点在对称轴上

45逆定理 如果两个图形的对应点连线被同一条直线垂直平分，那么这两个图形关于这条直线对称

46勾股定理 直角三角形两直角边a、b的平方和、等于斜边c的平方，即a+b=c

47勾股定理的逆定理 如果三角形的三边长a、b、c有关系a+b=c，那么这个三角形是直角三角形

48定理 四边形的内角和等于360°

49四边形的外角和等于360°

50多边形内角和定理 n边形的内角的和等于（n-2）×180°

51推论 任意多边的外角和等于360°

52平行四边形性质定理1平行四边形的对角相等

53平行四边形性质定理2平行四边形的对边相等

54推论 夹在两条平行线间的平行线段相等

55平行四边形性质定理3平行四边形的对角线互相平分

56平行四边形判定定理1 两组对角分别相等的四边形是平行四边形

57平行四边形判定定理2 两组对边分别相等的四边形是平行四边形

58平行四边形判定定理3 对角线互相平分的四边形是平行四边形

59平行四边形判定定理4 一组对边平行相等的四边形是平行四边形

60矩形性质定理1 矩形的四个角都是直角

61矩形性质定理2 矩形的对角线相等

62矩形判定定理1 有三个角是直角的四边形是矩形

63矩形判定定理2 对角线相等的平行四边形是矩形

64菱形性质定理1 菱形的四条边都相等

65菱形性质定理2 菱形的对角线互相垂直，并且每一条对角线平分一组对角

66菱形面积=对角线乘积的一半，即S=（a×b）÷2 67菱形判定定理1 四边都相等的四边形是菱形

68菱形判定定理2 对角线互相垂直的平行四边形是菱形

69正方形性质定理1 正方形的四个角都是直角，四条边都相等

70正方形性质定理2正方形的两条对角线相等，并且互相垂直平分，每条对角线平分一组 对角