（计算机软件与理论专业论文）基于描述逻辑的语义web知识推理研究.pdf

摘要 描述逻辑( d e s c r i p t i o nl o 西c ) 燕基予对象的知识寝示的形式化，它依据提供的构造器，在 简单鲍概念靼关系上构造出复杂懿概念和关系。本文在基本攒述逻辑艇c 妁綦破上添艇搀造 嚣：最大罄数魏窳( s n r c ) 、最小蓥数约柬( ) n r e ) 、传递* 系( r + ) 、反关系( r 一) 、关系并 ( r l u 对、关系复台( r l 。) 、个体实例祭( 8 ) ) 黠其进褥了扩熙，提出了接述灌瓣能一并给 出了描述逻辑a l 矿鼹语法豁笈它的语义，形式纯公理体系，还给出了一些基本性质，包括幂等 律、交换律、缩食律等：然后分辑论诞了语法接沦与避义推论的关系。检测撵逃逻辑鼹袭示 的概念的可满足蝰是摇港逻辑接璎的一个关键滴题，在s c h m i d t s e b a 坤和s m o l k a 为检验地e 概念的可满足性提出的t a b l e a u 舞法的基础上，绘出了a l c + 表黎的一般概念麴霹满怒性梭测 方法并讨论了菸健熏要接理阔题概念包含简鼷、概念等价间题、橛念不稿交闷越) 可以转 化为检测概念可满足性另外，由踟的创始人b e r n e r s - l e e 在2 0 0 1 年正式提出的语义# 曲，主 要蒸予魏l ； 葵r d f p l d f s ，势在扰蓥戮上拇建本侮鞍逻辑猿理瓶癸j ，玖竞畿基于语义韵知识表 示和推理，从而自& 够为计算机所理解和处理，w 3 c 等研究豳体提出了针对语义w e b 表达瓣键多 建议穰语富，这臻浯誊包括d a m l ( 融r 戳a g e n tm a r k u pl a n g u a g e ) 、o i l ( o n t o l o g yi n f e r e n c e l a y e r ) 、d a 瓶l + o i l 、o w l ( w e bo n t o l o g yl a n g u a g e ) ，构成了语义w e b 的基础，我们绘如t a l c “ 与w e b 本体港言o w l 煞对漱燕系，主簧楚语法上豹对酸，甑掭构造器的对映和可以厢a l c + 来插 述o w l 中的部分公理接饕，给出了个用a l c + 插述o w l 表示的知识及攘理的示铡擐惹撮出 了今后的孵究方离，筏帮j 提出麴播涟逻辑a l e + 其有一定静理论靳实用价值，它适合于通过概 念分类来表示知识的应箱领域。 关键试：语义w e b ：接述逻辑：a l c ：a l c + ：概念哥满足性；t a b l e a u ：o w l r e s e a r c ho i ls e m a n t i cw e b k n o w l e d g er e a s o n i n gb a s e d o nd e s c r i p t i o nl o g i c a b s t r a c t d e s c r i p t i o nl o g i ci st h eo b j e c t b a s e df o r m a lw a yt or e p r e s e n tk n o w l e d g e ，i t d e p e n d so nt h ep r o v i d e dc o n s t r u c t o r sa n dc o n s t r u c tt h ec o m p l e xc o n c e p t sa n dr o l e s o nt h es i m p l ec o n c e p t sa n dr o l e s t h i sa t t i c t e ，o i lt h eb a s i so ft h eb a s i nd e s c r i p t i o n l o g i ca l c ，a d d st h ec o n s t r u c t o r ss u c ha sm a x c a r d i n a l i t yr e s t r i c t i o n ( - - n r 。e ) ，t r a m s i t i v er o l e ( r + ) 。i n v e r s er o l e ( r - ) ，u n i o no f r o l e s ( r i u r 2 ) ，c o m p o s i t i o no fr o l e s ( r l 。r 2 ) ，i n d i v i d u a l ss e t ( a ) t oe x t e n dt h e d e s c r i p t i o nl o g i c t h e nw ep u tf o r w a r dt h ed e s c r i p t i o nl o g i ca l c + a n dw eg i v et h e s y n t a xa n ds e m a n t i c so fa l c + ，a n di t sf o r m a la x i o ms y s t e m ，w ea l s og i v es o m eb a s i c p r o p e r t i e s ，w h i c hi n c l u d e st h ei d e m p o t e n e yl a w ，t h ec o m m u t a t i o nl a w ，t h ec o m b i n a t i o n a we t c ：t h e nw ea n a l y s ea n dp r o o ft h er e l a t i o nb e t w e e nt h es y n t a xi n f e r e n c ea n d s e r e a n t i ci n f e r e n c e c h e c k i n gt h es a t i s f i 如i l i t yo ft h ec o n c e p tt h a ti sr e p r o s e n t e d b yd e s c r i p t i o nl o g i ci sak e yp r o b l e mo ft h ed e s c r i p t i o nl o g i cr e a s o n i n gp r o b l e m ，o n t h e b a s i s o ft h et a b l e a ua l g o r i t h m 。w h i c hw a sp u tf o r w a r db ys c h m i d t s e h a u da n d s m o l k a ，t oc h e c k t h es a t i s f l a b i l i t yo fa l cc o n c e p t s ，w eg i v et h ew a yt oc h e c kt h e g e n e r a lc o n c e p t st h a ti sr e p r e s e n t e db ya l e + q a b l e a u a l g o r i t h mo fa l c + , w ea l s o a n a l y s ea n dp r o o ft og e tt h ee o n c l 船8 i 8 n t h a to t h e ri m p o r t a n tr e a s o n i n gp r o b l e m s ( s u c h a st h ec o n c e p t ss u b s a m p t i o np r o b l e m ，t h ec o m t e p t se q u i v a l e n c ep r o b l e m t h ec o n c e p t s d i s j o i n t n a s sp r o b l e m ) c a nb er e d u c e dt oc h e c k i n gt h es 8 t i $ f i a b i l i t yo fc o n c e p t s i n a d d i t i o n ，s e m a n t i cw e b ，w h i c hi sp u tf o r w a r db yb e r n e r s l e ew h oi st h eb e g i n n e ro f w * wi n2 0 0 1 ，m a i n l yb a s e so n 嫩纯a n dr f r d f s ，i tc r e a t e st h eo n t o l o g ya n dt h el o g i c a l r e a s o n i n gr u l e so l lt h i sb a s i si no r d e rt oa c c o m p l i s ht h ek n o w l e d g er e p r e s e n t a t i o n a n dr e a s o n i n go nt h eb a s i so fs e m a n t i c s 。t h e ni ti sa b l et ob eu n d e r s t o o da n dd e a l e d w i t hb yc o m p u t e r t h er e s e a r c hg r o u p ss u c ha sw 3 cp u tf o r w a r dm a n ya d v i c ea n d l a n g u a g e st h a ta i ma tt h er e # r e s e n t a i o no fs e m a n t i cw e b w h e s el a n g u a g e s ，w h i c h i n c l u d e sd a l i l ( d a r p aa g e n tm a r k u pl a n g u a g e ) + o i l ( o n t o l o g yi n f e r e n c e l a y e r ) ，d 删l + o i l ，铆l w o bo n t o l o g yl a n g u a g e ) ，e o n s t i t u t e st h eb a s i s o fs e m a n t i c w e b ，w eg i v et h ec o r r e s p o n d i n gr e l a t i o nb e t w e e na l c + a n dw e bo n t o l o g yl a n g u g eo w ，i t i st h es y n t a xm a p p i n g ，i n c l u d e st h ec o n s t r u c t o rm a p p i n ga n du s i n ga g ot od e s c r i b e t h e 口a r t i a la x i o m so fo w l n e x t l y ，w eg i v ea ne x a m p l et h a ti su s i n ga l c + t od e s c r i b e t h ek n o w l e d g et h a ti sr e p r e s e n t e db yo w la n dr e a s o n f i n a ll y ，w ep u tf o r w a r dt h e r e s e a r c ha s p e c t si nt h ef u t u r e t h ed e s c r i p t i o nl o g i ca l rw h i c hm ep u tf o r w a r dh a s ac e r t a i nt h e o r e t i c a la n dp r a c t i c a lv a l u e ，i ti ss u i t e df o rt h ea p p l i c a t i o nd o m a i “ t h a t t h ek n o w l e d g er e p r e s e n t e db yt h ec o n c e p t sc l a s s i f y i n g ， k e yw o r d s ：s e m a n t i cw e b ；d e s c r i p t i o nl o g i c ；a l c ：a l c + ：c o n c e p ts a t i s f i a b i l t i y t a b l e a u ：o w l 独创性声豫 本人声明新呈交的学位论文是我个人在导师指导下进 行的研究工作及取得的研究成果尽我所知，除文中已经标 明引用的内容外一本论文不包含任何其他个人或集体已经发 表或撰写过的磷究成栗。对本文的蛩究擞出贡献的个人和集 体，均已在文中以明确方式标明本人完全意识到本声明的 法律结果由本人承担 学位论文作者签名：文斌 癣g 月g 豳 学位论文版权使用授权书 本学位论文作者凳全了解学校有关保留、使用学位论文 的规定，即：学校有权保留并向国家有关部门或机构送交论 文赡复印 牛和电子版，允许论文被查阅和惜阌。本人授权云 南师范大学可以将本学位论文的全部或部分内容缡入有关 数据库进行检索，可以采用影e p 、缩印或扫描等复制手段保 存翔汇编本学位论文+ 学位论文作者签名：文j 式 。酶月名日 指导教师签名：一酚巾 _ 坷r 年6 周7 日 1 。1 褒究背景 第一章前言 落义w e b 是由# 姆豹刽始天b e r n e r s - l e e 在2 0 0 1 冬正式掇出鲢 t i mb e r n e r s l e e ， 2 0 0 i w 3 c 它的提出，立即引起了人们极大的兴趣，在2 0 0 1 年就召开了两次慕于语义w e b 的专题学术讨论会语义w e b 研究鲍主要霹的就是扩展当前的删，使得阚络中信息都魑具 有语义的，趄计算机能够理解和处理的，便予入和计算机之间的交互与合作e 攀立 宇，2 0 0 3 因而其研究的侧燕点就是如何把信息表示为计箕机能够理解和处理的形式，即带 有语义语义w e b 主安基予x m l 帮r d f r d 裕 李青出，2 0 0 2 3 自简强，2 0 0 4 ，并在蓝蓥张上 构建雄体和逻辑推理规则，以完成蒸于语义的知识表示和推理，从而能够为计算机所理解和 楚理。在语义w e b 的研究中，翔谖袭示 麓炎椽，2 0 0 3 3 、零体论裳洋，2 0 0 4 3 、镣轻主缮【李 晶，2 0 0 3 等都是其照要的研究内容，它们都是不可分割的在知识的语义表示和推理中， 毒嚣个层次瓣婿究：一是在理论上，基于逻辑形式纯熬璎究王终，朝以一羚谭词逻辑为代表 的各种逻辑体系；二是基于这些逻辑理论的本体论的研究，可以稽作是舆体的应用研究 甘 键撰，2 0 0 4 3 。 描述逻辑建立程概念( c o n c e p t ) 和关象( r e l a z i o n 。r o l e ) 之上，其中概念解释为对象 的集合，关麓解释为对象之间的二惩关系，描述逻辑具裔合适定义的语义和很强的表选能 力一个描述逻辑系统包含陷个基本组成部分：表示概念稀关系的构造器：t b o x 包含断言； a b o x 实例断富；t b o x 和a b o x 上的推理机制一个描述逻辑系统的表达能力和推理能力取决 于对鞋上死个要素的选择戮及不漆静俊设( 蓑疆稽，2 0 0 3 3 【宋薅，2 0 0 4 3 。 在众多知识表承的形式化方法中，描述逻辑在十多年来受到人们的特别关注。主要原因 在予：它翻蠢清糍的模型一褒论辍翱；稷适合子逶：过概念分类学采表示瘦嚣领域：共疆缴了 很用的推理服务 f r a a zb a a d e r ，2 0 0 3 燕先来蓑一个嬲子，它滋鹱慧撵熏攒述逻辑寒表承起识，攒述家藏疆域巾豹一数概 念如果p e r s o n 是一个原子概念表示人个体攥，m a l e 是一个原子概念表示男性个体 集，h a s c h i l d 是一个原子笑系表示肖孩子。鄹么可以用描述逻辑提供的构造器来构造不阉的 概念否定( 记为_ 1 ) 袭示概念的补，如、m a l e 表示女性个体集：概念交( 记为c n d ) 表示既瘸子 概念c 又属于概念d 的个体实例集，如p e r s o n n m a l e 表示男人：概念并( 记为c u d ) 表示麟于 概念e 或者瘸子概念d 的个体实铡集。如m a l e u - m i a l e 表示勇往或者女性个俸实黼集：全蔺约 束( 记为v r c ) 表示与一些个体实例( 要求j 袅些个体实例都属于概念c ) 有装系r 的个体实例 缝盛鹣个俸嶷饲集，魏v h a s c h i i d 。m a l e 表示谴粕静孩子都是凳性懿母体实铡集：存在约束 ( 记为b r c ) 袭示与属于概念c 的个体实例有关系r 的个体实例组成的个体实例集，如 3 h a s c h i i d m a l e 表承霄菝予是男性豹个薅实铡集： 避基本描述逻辑a l c ( a t t r i b u t i v ec o n c e p td e s c r i p t i o nl a n g u a g ew i t h c o m p l e m e n t s ) s a t t l e ru ，1 9 9 6 只掇供了否定、概念交、概念并、全局约豢、存在约束构造 器，它有一定的表达能力和推理能力但在a l c 中要表达，如至少有两个粥孩的八，至多只有 三个女孩的人，这样的知识就比较鼷赃了。于是我们对基本糕述a l c 进行扩展，褥到a + ，它 是在a l c 的基础上添加构造器：最大基数约束、最小基数约束、传递关系、反关系、关系并、 关系复合、个体实例粲而得到的最大基数约束( 记为n r ，c ) 表示与至多n 个体变例( 并鼠返 n 个个体实例属予概念c ) 有关系r 的个体蜜倒集 b a n d e ra n ds a t t l e r ，1 9 9 6 3 ，弼， p e r s o n n 3 h a s c h i1 d m a l e 褒示至多有3 个孩子是女孩的人：嫒小基数约束( 记为n r c ) 表 示与至少r 1 个体实例( 并麓这i i 个个体蜜例耩子概念c ) 商蓑系r 的个体实铡集，如， p e r s o n n 2 h a s c h i l d 。m a l e 袭示至少蠢2 个孩子是勇弦戆人；健递关系( 记为r + ) 表精一个美 蓉是可以传遵的，妇h a s d e s e e n d a n t 是一个传递关系；反关系( 记为r - ) 表示一个关系蛉邀关 系，如h a s p a r e n t 是h a s c h i l d 的反关系；关系并( 记为r l u r 2 ) 表示俩个关系的并，如 h a s s 。n 醵a s d 8 u 秘t e r 袭示h a s s o n ，h a s d a u g h t e r 这辫个关系静并，鞠当予芙系h a s c m l d ：关 悉复合( 记为r l 。嗡表示嚣个关系懿复合，妇誊h a s p a r e n t 褒拳毒父母关系，h a s b r o t h e r 表示 有兄弟关系，那么h a s p a r e n t o h a s b r o t h e r 袭示有叔伯关系，它相当予关系h a s u n c l e ：个体实 稍榘 记为 a t ) 表勇专由个体实铡a 组戏的集合，弼 小髑 表示幽夺明这个人缀成的个体察例 集 1 2 研究内容 本文的移 究内容魁糖： ( 1 ) 在基本描述逻辑a l c 的羹础上，添加椅溉器：娥大蒸数麴柬、最小基数约束、传递关 系、反关系、关系并、装系复合、个体实例集对描述逻辑a l c 迸彳予扩展，提出了摘述谶辑 她矿绘出了扩矮君静撼述逻辑舡矿瓣语法、瓣义以及璎藏纯公理体系，还给穗了一些蒸本 性质并对其进行了分析论证，然席分析论证丁语法推论与谮义推论的关系 ( 2 ) 讨论了撩疆闯蕊中的关键问题一概念可满足性问题t a b l e a u 演算怒一种一阶逻辑 驰公式冒淹蹙犍诞骧方法 羰键，2 0 0 0 ，s e 抵i d t s c h 秘s m o l k a 戈检验a 酩壤念簸零满足 性提出了其对应的t a b l e a u - 辣法 d o n i n ie ta l + ，2 0 0 0 ，程此基础上我们绘出? a l c + 的基于 语义表( 即t a b l e a u ) 的概念可满足性检测方法- - a l c * 的t a b l e a u - 算法，分析了其性质，包括 终虚性、霹纛性、完全性：然鑫涎论了其缝一些夔要攘理鞠惩裂概念母满怒性瓣题豹转纯： ( 3 ) 讨论了描述逻辑a l c + 与w e b 本本体语言o w l 的对映关系，主螫是诱法上的对蛱，龟撼 构造的对映和用a l c + 插述o w l 中的部分公理 4 ) 鼹矮绘出了w e b 率体语富o w l 表示抟熊谖蘑撰述逻辑a l c 袭示觳襁联靛示翻，并措 出了今席进步的研究王作 1 3 文章的组织结构 文章组织结构如下： 第一章靛京，介绍了研究背景以及要研究的内容； 第二章扩矮描述逻辑a l c + 形式纯系统定义了扩震擒选逻辑a l e + 的形式化模型、语 法、语义l 三 及势绘出了形式纯公理，褥到了一鍪基本矬艨：然螽分接论诞了语法与落义麴关 系 第三章扩袋描述逻辑a l c * 的概念可满建健问题播述遴辑的推理闯慰包括概念_ 町满 是渡蠢鼷、糕念惫岔趣鬏、糍念等傍怒疆、概念不提交阚鬏，主簧讨论了壤念胃满是槛游惩， 并证明了篡地重要推理闽题w 以转换为概念可满足性阏题 第翻章扩展描述逻辑a l c 与w e b 本体语宵o w l 的对映美系主要讨论了语法上的对 映关系。 第羹章w e b 本体语寓o w l 描述的知识熙a l c 十表示及摊理的示倒， 结柬语 2 第二章扩展描述逻辑a l o + 形式系统 基本攒述逻辑a l c 提供了否定、概念交、概念并、垒局约束、存在约束构造嚣，它肖一 定的表达能力为了让描述耀辑具有更强的表达能力，我们引入了新的描述逻辑a l c + ，它悬在 a l c 的基础上增加了传递关系( 记为r 十) 、葳关系( 记为r ) 、关系并( 记为r l u r 2 ) 、关系复合 ( 记为r l o k 2 ) 、个髂实铡巢( 话为避势帮一曦数量约束( 记海美漫c ，s 基r ) 构造器。下露霹 a l c + 中静语法窝语义的形式化定义和一些褴艨进行阐述。 2 1a l c + 的形式化公理体系 2 1 1 描述逻辑a l c + 的语法 a l c + 将中耍蔫到的符譬表示如下 原子概念繁蚤o ：垂。= e 1 ，白， ： 原子关系集n o ：r i 。= r l ，r 3 ， ： 对象个体( 寓例) 集o ：o = f a ，b ， ； 连接词：( 等价) ，一( 包盘子 ， 梅造器：。( 取反) ，u ( 著) ，疆( 交) ，t 渲耀念) ，土( 空概念) ，嚷。e 全蜀翡寨，j r c 存在豹寒) n r ，c ( 最小数量约束) ，t - n r c ， ( 1 c ) 1 = 1 c = a | a e 壤8 e 1 ： ( 5 ) ( c u d ) k c i u d z ： a e 1 l a e c 域者a d 1 ； ( 6 ) ( c i l d ) k e l n d f - f a 1 l a e c l 且a d i ： ( 7 ) ( v r c ) a e 1 i v b 使得( 8 ，b ) r 溯b e c 、； ( 8 ) 臼r ，0 ； 糖i s b 俊 ；辱( b ) e r l 盥b c 2 ： ( 9 ) n r c u _ n r d ) 等价表示为卜五r ( c u d ) 一n r c u _ n r d 公理1 1 卜、- m r ( 。c u d ) u 、( 1 n r c u - 1 _ n r d ) 等价表示为f n r ( c f i d ) 一劭r c 几n r d 公理1 2 卜一j r 一v r c u c 等价表示为旧r 一v r c c 公理1 3 卜、( n r c u _ _ n r c ) 等价表示为 _ 一h r c h _ n r + c u _ n r d 表暴在论域中，概念c 蔽者概念d 中躬至少n 个个体实例有关系r 的个体实例集，包含予跟概念c 中的至少n 个个体实例有关系r 的个体 实例巢与跟概念d 中的至少1 1 个个体实例有关系r 的个体实例集并集； 公理l l 卜 n r ( c n d ) - - _ n r c n _ n r d 表示在论域中，躐概念c 中的至少n 个个体实例 ( 并且这些个体实剿也鼷于橛念d ) 寿关系r 的个体实铡榘，毽含予蹑概念c 中静至少n 个个 体实例有关系r 的个体实例集与跟概念d 中的歪少n 个个体实例鸯关系r 姆个体实例集的交 集： 公理1 2 卜j r v r e c 表示在论域中，如果一个个体实倒祸子躁与一些个体实例有关 蓉r 并且这些个俸实例属于概念c ) 豁个体集中翡个体实倒有关燕r 静反关系r 一静个体实例 煞，1 5 么该个体实例属于概念c ； 6 公理1 3 - - ， - n r ，c + + 魏- l g e 表示在论域串，一个个体实箭不属于与概念c 中的至少n 个个体实铡寒关系r 鲍个体实铡集，当虽仅当该个俸实铡耩予与概念e 中捐至雾n - i 令个俗 实铡糍关系r 鲍个体安摄集； 公理1 4 翔聚k a 一0 ，置k 一，那么h 8 卜一表示在论域中，一个个体实磷蒋于概念 c ，辫是概念c 又包窘手概念玩嚣概念c 是掇念d 酌子集，鄹么该个体实铡也满予概念d ； 公理1 5 卜 8 一e u d 当旦仅当h 8 一c 或者卜f 8 一b 表示在论域中，一个个体安铡耩 予概念e 鄹概念d 的势，巍虽慢巍滚个体实铡攥予概念e 或者属于橛念d ： 公理1 6 卜 8 一e 融当量饺警 8 一c 藏卜 a 一d 袭零在论域中，个个侮实铡瘸子 壤念e 秘概念b 的交，当虽投姿谈个体实镶凝属于概念c 翌耩手概念d ： 公理1 7 妇果k d ，虽b c ，瓣么k h 表示在论躐牵，概念c 锻含予概念，笄虽褫 念d 又包含予檄念e ，那么概念c 与概念d 等羚： 公理1 8 姆聚沁一玟鼠一e ，酆么k s 表示在论域中，概念c 雹含予概念d ，著量横 念d 叉包禽予概念毪那么概念c 包含于概念e ； 公理1 9k - - d n e 当且仅墨k d 虽k e 表拳程论壤中，檄念c 锻鸯予概念d 帮壤 念e 的交，当且仪当援念c 包禽予概念d 且壤念c 包含于概念；也就是概念c 搿表示的个髂 实例集包宙予概念d 所表示熊个体实例纂和概念d 赝袭示熬个体实铡集戆交袋，当且便当壤 念c 厨表示鲶个体嶷铡熊包金子壤念d 霞袭示熬个体实铡集并虽瞧怠畲予概念掰袭拳静个 体实例集。 下面给出语法诹明、语法推论以及落义推论的定义。 定义2 。7 ( 语法的“诞哽”) 设r 譬厶，c e l 当我们说“c 是从蹦证鳃”，是摆存戎着魄元 囊的霄限序列龟，其中岛= e ，显每个( k = l ，2 ，n ) 潢足t “) c k e r , 或。 ( 2 ) c k 是“公理”，或 ( 3 ) 存在i ，j k ，使c l 嗡一c b 具毒上述性质的商照j 芋列c l ，岛，岛叫做c 从r 鲍“证明”。 定义2 。8 ( 谣法箍论) 设r 二，c a l 然后规定： ( 1 ) 如果公式c 是从公式熊r 可 雁，那么我们记为rk ，这时r 中的公式叫做“假设”，c 叫做瑕 定集r 的语法推论 ( 2 ) 若g 卜c ，则称c 箍a l c + 中的“定理”，记为k c 在_ a l c + 中从够的证明，艇称为在a l c + 中 的证明 ( 3 ) 在一个证明中，当q = q - - 魄( i ，j l 对，有蟊静哥麓：d ，d 或者d 鼹公理，蔽d 是健瘸辩嚣得赛静，前三释清况 与( 1 ) 中的兰种情况一样处理就行了只用讨论d 由d 汲d j = d i d 使用m p 而得到的情形因为 i ，j n ，由爨纳弦我， 如果r uf c 卜d j ，那么r 卜c d i 如果r u e b ，邦么f 卜c 一毽躲r 晦一趣”d ) 。 于摄就有c - - d 从r 的证明： ( 1 )、 卜c d i 从r 的 芷明 ( k ) c 一瑾 f n l ) l 、 _ c 一( d i 一一d ) 从r 的证明 ( 1 ) c 一d i 一 ( 1 + 1 ) c 一( d i d ) 一( ( c d i ) 一( c d ) ) l + 2 ) 密一珐) 一( e 一) ( 1 + 3 ) c d 这就是归鳃过程 ( 公理2 ) 1 ) ，( 1 + 1 ) ，m p ( k ) ，( 1 + 2 ) ，m p 涯毕 由上面给出的公理，我们可推辱出下黼的命题 命题2 。1k c 证明：下面是c c 的一个证明， ( 1 ) c 一( ( c c ) 一c )公理1 ( 2 ) ( e 一( ( e e ) - c ) ) 一( ( c 一( c c ) ) 一( c c ) ) 公理2 ( 3 ) ( c 一( c c ) ) 一( c c )( 1 ) ，( 2 ) ，舯 4 ) 0 一( c e )公理1 ( 5 ) ( c c )( 3 ) ，( 4 ) ，m p 迁攀。 命题2 2 卜，c 一( c d ) 证唆：下垂是聚要靛 歪羁， ( 1 ) h d 一一c ) 一( c d ) 公理3 ( 2 ) ( ( 一d 一一c ) 一( e d ) 一b e 一( ( 司一国一( c - - d ) ) ) 公理1 ( 3 ) 一c 一( 一d 一一c ) 一( c - - 1 ) ) ) ( 1 ) ，( 2 ) ，m p ( 4 ) “c 一( ( 、d 一一e ) 一( c d ) ) ) 一，e ，沙叫e 一贮( 0 一b ) 公理2 ( 5 ) ( 、e 一( 一d 一# ) ) 一b c 一( c d ) ) ( 3 ) ，( ，船 ( 6 ) ，c h d 一、c )公理l ( 7 ) ，e 一( c d )( 5 ) ，( 6 ) ，m p 证毕 螽戆2 ，3 ( ，c e ) 一e 证明；由演绎定理，只用证明 c c lf c 下覆虢是c 玖 、c - - c 挎一个涯羁， ( 1 ) ，c 一( c 一一1 ( - , c c ) )命题2 2 ( 2 ) ( 、c 一( c 一、( 、c c ) ) ) 一( ( ，c c ) 一( 矗，一h c c ) ) ) 公理2 ( 3 ) ( _ 1 c c ) 一( ，c 一，( ，c c ) )( 1 ) ，( 2 ) ，胛 ( 4 ) 一，c c假定 ( 5 ) 、c - 、( 、c c )( 3 ) ，( 4 ) ，m p ( 6 ) ( c 一，( c - - c ) ) 一( ( ，c c ) 一c ) 公理3 ( 7 ) ( 、c c ) 一c( 5 ) ，( 6 ) ，m p ( 8 ) c( 4 ) ，( 7 ) ，m p 命题2 4 ( c d ) 一( 1 d 一- 1 c 证明：由演绎定理，只用证明 c d 卜1 d 一- - - , c ，下匿是- 1 d 一1 c 从c d 的一个证明过程， ( 1 ) ，c c双重否定律 ( 2 ) c d假设 ( 3 ) 、，c d( 1 ) ，( 2 ) ，公理1 8 ( 4 ) d 一，、d双重否定律 ( 5 ) 一，c 一一d ( 3 ) ，( 4 ) ，公理1 8 ( 6 ) ( ，一c - + 一一d ) 一( ，d 一- 1 c ) 公理3 ( 7 ) ，d ，c( 5 ) ，( 6 ) ，m p 证毕 命题2 5 、( c d ) 一( d c ) 证明：e h 演绎定理，只用证明( 一( c d ) ，d ) 卜c ( 1 ) 、( c d ) 一( ( c d ) 一c )命题2 2 ( 2 ) _ 1 ( c d )假设 ( 3 ) ( c d ) 一c( 1 ) ，( 2 ) ，m p ( 4 ) 、c 一( c d )命题2 2 ( 5 ) 一c c ( 3 ) ，( 4 ) ，公理1 8 ( 6 ) ( 一c c ) 一c 命题2 3 ( 7 ) c( 5 ) ，( 6 ) ，m p 证毕 定理2 2 ( 反证律) r u 卜，c 卜d1 卜r 卜c r u 、c 卜 d 一 证明：根据已知条件( d 和_ 1 d 都存在从r u ，c 的证明) ，可以先写出d 从r u 一c 的证明如 下， ( 1 ) 、 _ d 从r u ( 一c 1 的证明 ( k ) d 一 ( k + 1 ) 、 - 一d 从r u 一c 的证明 ( 1 )- 1 dj ( 1 + 1 ) 、d 一( d c )命题2 2 ( 1 + 2 ) d c( 1 ) ，( 1 + 1 ) ，m p ( 1 3 ) c ( k ) ，( 1 + 2 ) ，m p 至此证明了r u 卜，c ) 卜c 用一次演绎定理，可得r 卜_ 1 c c 由此可将c 从1 1 的证明如下 构造出来， 9 ( i ) 、 卜- c - - c 从r u 蜘诞鹳 ( m ) 一c o ( m + 1 ) ( 一e e ) 一c ( 十2 ) c 于是有r 卜c 命题2 ，3 ( 瓣) ，( 瓣+ i ) ，耩p 雁毕， 定琏2 3 ( 癌谬簿) r u c 卜d - i 卜fh e f “ c b o 证明：因为已知r u c f d ，数存农d s i r u c 弱诞踞，程这个诞明中爨毒出现的缓定e 之前 都插入一1 坷和。一c 这两项，于是该证明就变成了d 从r u 卜、_ 1 c 的一个证明，从而得到 1 ) f u 一e j 一 同嘲由r 知条件r u c 卜、o 可褥 ( 2 ) r u 1 _ 1 c 卜- 1 d 盎j ( 1 ) ，2 ) 霜葳证褥褥r 卜1 c + 这群壶获诞撑维滋了箔谬律 诞华 命题2 6 、( c d ) 一一d 诞鹱；由演绎定蓬，是羯诞磷 ，( c 一秘j _ ，b 把d 作为凝缓设，于是鸯， ( l ) 一( c d ) ，d 卜c d ( 2 ) ， c 一秘，b 卜、( e n ) 由( 1 ) ( 2 ) 用蛸谬搏褥 一( c d ) h d ， 下盈是 。( c d ) ，d 卜c d 的一个证孵过程， 1 ) b 一( c - - d ) 公理i ( 2 ) 霰竣 ( 3 ) c d( 1 ) ，( 2 ) ，m p 诞华 套联2 7 ，( e b ) 一e 证明：由演绎是理，只用证明卜( c d ) 卜c ， 把，e 作为新假设，于是商， ( 1 ) ，( e d ) ，一e 卜e b ( 2 ) - - , ( c d ) ， 一( e d ) 由( 1 ) ( 2 ) 用反证律可得f 一( c d ) 卜c ， 下嚣是 。( e o ) ，e k d 的一个谨鞠进程， ( 1 ) 、c假设 ( 2 ) 、e 一e d ) 命题2 2 ( 3 ) e d( 1 ) ，( 2 ) ，m p 涯毕。 a l 。c + 还有下面的重要性质： 性爨2 1 鞯等律：( 1 ) c h c c ( 2 ) c u e 辛e 性质22 交换橼：( 1 ) c n d d n c ( 2