（交通信息工程及控制专业论文）基于格蕴涵代数的广义格值模态逻辑及其归结自动推理的研究.pdf

西南交通大学博士研究生学位论文第i t 摘要 格是一 类重要的 代数结构， 现实世界中的 很多现象都可以 用格来刻画， 尤 其是不可比 较性。而建立在格上的格值逻辑系统把己有多值逻辑的链状真值域 拓展到较一般的格上，既能处理全序性信息，又能处理非全序性信息，从而更 有效地描述人类推理、 判断和决策的不确定性。 广义模态逻辑属哲学逻辑范畴， 对于刻画事物的“ 势态” 、 人物的“ 情态” 和过程的“ 时态” 是一种十分有效的 工具。 本文在格值命题逻辑系统l p ( x) 和格值一阶逻辑系统l f ( x)的基础 上，讨论了 广义格值模态逻辑系统的语义及语法性质，并对其a一 归结原理做 了初步探讨，主要在下述三个方面取得了 研究成果: 第一部分:关于格值模态命题逻辑系统及其归结方法的研究 在此部分，把模态算子n ( 必然)和p ( 可能)引入格值命题逻辑系统 l p ( x ) ， 建 立了 新的 格值模态命题 逻辑系 统l m p ( x ) ， 并 研究了 它的 语义刻画 及语法结构， 证明了在此语义解释和语法框架下的系统仍是a 一 可靠的和协调 的: 在此基 础上， 进一步研究了 基于格值 模态命 题逻辑系统l m p ( x ) 的a 一 归 结原理， 给出了 计算a 一 直接归结式和a 一自 归结式的规则， 并总结出 具体的归 结方法. 第二部分:关于格值时态命题逻辑系统及其归结方法的研究 此部分的主要工作是在格值命题逻辑系统l p ( x ) 中引进时态算子e ( 曾 经) 、f ( 将会)及其对偶算子h ( 曾经总是) 、g ( 将会总是) ，提出了以时 轴为 语境的 格值时态命题逻辑系 统l t p ( x ) ， 并给出 其具体的 语义解释和语法 结构，并讨论了它的一些性质，证明了该系统的可靠性和协调性。此外， 研究 了 与时间 有关的( a , t 卜归结原理， 给出了 计算时态归结式的规则，并提出了 时 态归结的具体方法 第三部分:关于格值模态一阶逻辑系统及其归结原理的研究 第i i 页西南交 通大学博士 研究 生学 位论文 这一部分主 要是 在格值模 态命题逻辑系统l m p ( x ) 中引 进量词和谓词， 建 立格值模态一阶逻辑系统l m f ( x ) ，并给出其语义解释和语法结构，证明了 系 统的可靠性和协调性;另外，为了判断公式的可满足性， 定义了格值模态一阶 公式的 s k o l e m标准型和h - 解释;在此基础上， 对基于系统l m f ( x ) 的a 一 归 结原理进行了初步探讨. 关键词格蕴涵代数广义格值模态逻辑定理自 动证明归结原理 西南交通大学博士研究生学位论文 第 i i i 页 ab s t r a c t t h e l a tt i c e i s a k i n d o f i m p o r t a n t a l g e b r a i c s t r u c t u r e . i n o u r l i f e , m a n y p h e n o m e n a c a n b e d e s c r i b e d b y l a tt i c e , e s p e c i a l l y n o n - c o m p a r a b i l i t y . l a tt i c e - v a l u e d l o g i c s y s t e m b as e d o n l a tt i c e e x t e n d s l i n e a r v a l u e d f i e l d o f m u l t i - v a l u e d l o g i c t o l a tt i c e , t h u s n o t o n l y c a n d e a l w it h o r d e r i n f o r m a t i o n , b u t a l s o c a n d e a l w i t h n o n - o r d e r i n f o r m a t i o n , c o n s e q u e n t l y d e s c r i b e t h e u n c e r t a i n t y o f h u m a n r e as o n i n g , j u d g i n g a n d d e c i s i o n - m a k i n g m o r e e ff e c t iv e l y . g e n e r a l i z e d m o d a l l o g i c b e l o n g s t o p h i l o s o p h y l o g i c c a t e g o ry . i t i s a v e ry e ff e c t i v e t o o l t o d e s c r i b e t h e t e n d e n c y o f t h i n g s , a tt i t u d e o f p e o p l e a n d t e n s e o f c o u r s e . b a s e d o n l a t t i c e - v a l u e d p r o p o s i t i o n a l l o g i c s y s t e m l p ( x ) a n d l a tt i c e - v a l u e d f i r s t - o r d e r l o g i c s y s t e m l f ( x ) , t h e a u t h o r s t u d ie d s e m a n t i c a n d s y n t a x p r o p e rt i e s o f g e n e r a l i z e d l a tt i c e - v a l u e d m o d a l l o g i c s y s t e m , a n d p r o b e d i n t o a 一 r e s o l u t i o n p r i n c i p l e . t h e s p e c i f i c c o n t e n t s a r e a s f o l l o w s : p a r t o n e t h e s t u d y o f l a t t i c e - v a l u e d mo d a l p r o p o s i t i o n a l l o g i c s y s t e m a n d i t s re s o l u t i o n me t h o d i n t h i s p a rt , w e i n t r o d u c e d m o d a l o p e r a t o r s n ( n e c e s s a r y ) a n d p ( p o s s i b l e ) i n t o l a t t i c e - v a l u e d p r o p o s i t i o n a l l o g i c s y s t e m l p ( x ) , s e t u p a n e w l a t t i c e - v a l u e d m o d a l p r o p o s i t i o n a l l o g i c s y s t e m l mp ( x ) , s t u d i e d i t s s e m a n t i c p r o p e rt i e s a n d s y n t a x s t r u c t u r e , p r o v e d t h e s o u n d n e s s a n d c o n s i s t e n c e o f t h i s s y s t e m . b a s e d o n t h e s e w o r k , d i s c u s s e d a 一 r e s o lu t i o n p r i n c ip l e o f l a tt i c e - v a l u e d m o d a l p r o p o s i t i o n a l l o g ic s y s t e m l mp ( x ) , g a v e o u t t h e r u l e s o f c o m p u t i n g a一 d i r e c t r e s o l v e n t a n d a 一 s e l f r e s o l v e n t , a n d p r o p o s e d d e t a i l e d r e s o l u t i o n m e t h o d . p a r t t w o t h e s t u d y o f l a t t i c e - v a l u e d t e n s e p r o p o s i t i o n a l l o g i c s y s t e m a n d i t s re s o l u t i o n m e t h o d 第 i v 页西南交通大学博士研究生学位论文 t h e m a i n w o r k o f t h i s p a rt i s t o in t r o d u c e f o u r t e n s e o p e r a t o r s e ( e v e r ) , f ( w i l l ) , x ( e v e r a l w a y s ) a n d g ( w i l l a lw a y s ) i n t o l p ( x ) , p u t u p l a tt i c e - v a l u e d t e n s e p r o p o s i t i o n a l l o g i c s y s t e m up 江)w h i c h t a k e s t i m e a x i s a s l a n g u a g e c ir c u m s t a n c e , g a v e d e t a i l e d s e m a n t i c i n t e r p r e t a t i o n a n d s y n t a x s t r u c t u r e , a n d d i s c u s s e d s o m e p r o p e r t i e s o f i t , t h e n p r o v e d s o u n d n e s s t h e o re m a n d c o n s i s t e n c e th e o r e m . f u r t h e r m o r e , s t u d i e d ( a , t ) 一 r e s o l u t i o n 州n c i p l e w h i c h i s r e l a t e d t o t i m e , g a v e s o m e r u l e s o f c o m p u t i n g t e n s e re s o l v e n t , a n d p u t f o r w a r d th e m e t h o d o f t e n s e r e s o l u t i o n . p a r t t h r e e t h e s t u d y o f l a t t i c e - v a l u e d mo d a l f i r s t - o r d e r l o 梦 c s y s t e m a n d i t s r e s o l u t i o n p r i n c i p l e i n t h is p a r t , w e i n t r o d u c e d q u a n t i f i e r s a n d p r e d i c a t e i n t o l m p ( x ) , p u t u p l a tt i c e - v a lu e d m o d a l fi r s t - o r d e r l o g i c s y s t e m l mf ( x ) , a n d g a v e i t s s e m a n t i c in t e r p r e t a t i o n a n d s y n t a x s t r u c t u r e , p r o v e d s o u n d n e s s t h e o r e m a n d c o n s i s t e n c e th e o re m . m o r e o v e r , i n o r d e r t o j u d g e t h e s a t i s f r a b i l i t y o f f o r m u l a , d e f i n e d s k o l e m s t a n d a r d t y p e a n d h - i n t e r p re t a t i o n . b a s e d o n t h e s e w o r k , m a d e a p r i m a ry d i s c u s s i o n o f a 一 r e s o l u t io n p r i n c i p l e b a s e d o n l m f ( x ) . k e y w o r d s ) l a tt i c e i m p l i c a t i o n a l g e b r a , g e n e r a l i z e d l a t t i c e - v a l u e d mo d a l a u t o m a t e d t h e o r e m p r o v i n g ,p r i n c i p l e 西南文通大学 学位抢文版权使用授权书 本学位论文作者完全了 解学校有关保留、 使用学位论文的规定， 同意学校保留并向国家有关部门或机构送交论文的复印件和电子 版，允许论文被查阅和借阅。本人授权西南交通大学可以将本学位 论文的全部或部分内容编入有关数据库进行检索，可以采用影印、 缩印或扫描等复制手段保存和汇编本学位论文。 本学位论文属于 1 、保密口，在_年解密后适用本授权书; 2 、不保密曰，适用本授权书。 ( 请在以上方框内打 “ j ) 学 位 论 文 作 者 签 名 : 办之 、 指 导 教 师 签 名 : 徐t i 日期: .又 找 子年 1月 巧 日日期: ;,2 : t 3年 1月 巧 日 舀 南 文 通 大 学 学 位 伦 文 创 折 性 声 朋 本人郑重声明:所呈交的学位论文，是本人在导师指导下独立 进行研究工作所取得的成果。除文中己经注明引用的内容外，本论 文不包含任何其他个人或集体已经发表或撰写过的研究成果，对本 文的研究做出贡献的个人和集体，均已 在文中作了明确的说明。 本 人完全意识到本声明的法律结果由本人承担。 本学位论文的主要创新点如下: l 、 在格 值命 题 逻 辑 系 统l p ( x 中 引 进模 态 算 子n( 必然 和尹 : l x l - ) l 是一映射， ( l ,v , n , ， 一 称为 拟格蕴涵 代数( 简 记为q - l i a ) ， 如 果对所有x , y , z e l ， 下列性质成立: ( 1 1 ) x - ( y - ) . z ) = y- - ( x -*z ) ; ( 1 2 ) x - - x =i ; ( 1 3 ) x - y 二 y , - + x ; ( 1 4 ) 若x -+y = y - * x = i ， 则x = y ; ( 1 5 ) ( x - y ) - y= ( y - x ) 一x . ( l , v ， 八 ， ， ， 分) 称为格蕴涵代数 ( 简记为 l i a ) ， 如果它是一个 q - l i a ，并且 对所有x , y , z e l ， 满足下列性质: ( 1 1 ) ( x v y ) - z = ( x - + z ) 八 ( y - - z ) ; ( 1 2 ) ( x n y ) 一z 二 ( x - - z ) v ( y - z ) 一个格蕴涵代数( l , v , n , , -+) 称为h 一 格蕴涵代数 ( 简记为h - l i a ) ，如果对 所有x y , z l ，x v 夕 v ( ( x 人 夕 ) 冲z ) 二 i . 定 理1 . 4 . 1 0 设( l ,v ,a , , -+ ) 是 一 格 蕴涵 代数， 对 于 任 意x , y , z l ， ( i )x - 。= x ; ( 2 ) x y = i ; ( 3 ) ( x -+y ) - y =x v y; ( x - z ) - 4 ( y 一z ) ( z - * x ) - ( z - * y ) y - ), ( x v z ) = ( z - a x ) -+( y - f x ) ; ( x n z ) - 4y = ( x - 4 z ) -+ ( x - j y ) : ( x - - y ) 一 ( ( y- - z ) -+( x - - z ) ) = i . 、卫产、，产、.2 4116 了子了、f 定 理1 . 4 . 2 0 设( l ,v ,人 厂 ， 峥 ) 是 一 格 蕴 涵 代数， 则( l ,v , n , , 斗 ) 是h 一 格蕴 涵 代 数当 且仅当 对所有x , y e l : ( 1 )x vx =i; c 2 ) x 一y = x v y . 西南交通大学博士研究生学位论文第 1 3 页 定 理1 . 4 . 3 0 ( l ,v ,a , , - ) 是 一 个 格 蕴 涵 代 数当 且 仅当 满 足 下 列 条 件: ( 1 )它是一个q - l i a ; ( 2 ) ( l ,v , a ) 是分配格: ( 3 ) 对所有x , y e l ，( x -y ) -y = x v y : ( 4 ) 对所有x , y e l ，x y = i . 注1 . 4 . 2 0 在一 个q - l ia ( l ,v ,a , , -+ ) 中 ， 引 进 算子 如 下: x 0 y = ( x - y y 对 任 意x , y e l ， ( 1 ) x . y = i n f z lx ， 。: ; ( 2 ) 因此 算子 满足结合律. 对任意a e l，n e n，递归地定义 a o = i , a 1 = a .a , a m . = a oa . 定 理1 . 4 . 4 0 在 格蕴 涵 代 数( l ,v ,n , ， 一 ，。 ) 中 ， 对任 意a , b , c e l ， 下面的 性 质 成立: ( 1 )a ob _。 ab c = b - ( a - - c ) ; ( 8 ) ( a - ), b ) 0( b - + c ) a - c ; ( 9 ) a - - ( b (9 c ) ? b (9 ( a - ) c ) ; ( 1 0 ) a .( b v c ) = ( a 0 b ) v ( a ( ( 川a 0 ( b a c ) = ( a qb ) 。 ( a 0 c ) ; 第1 4 页西南 交通大学博士研究生学 位论文 ( 1 2 ) a ob = ( a v b ) o( a n b ) ; ( 1 3 ) a v b = i 蕴涵a - + ( b o c ) = b o( a - c ) ; ( 1 4 ) a v b = 1 蕴涵( a o a ) v ( b o b ) 二 i ; ( 1 5 ) a vb =i 蕴涵a v b = 1 ; ( 1 6 ) ( a v b ) = a v b ，( a r b ) = a a b ， 对任意n e n. 定 理1 . 4 . 别 w )所有 格 蕴 涵 代数的 全体构 成一 个 真 类 定义 1 . 4 . 6 ，设l 是一 个格蕴涵代数，j c l 称为l 的 一个滤子 下列条件: 若j 满足 ( 1 )i ej; ( 2 ) 对任意x , y e l ， 若x j 且x - - y e j ， 则y e j . 称j 是l 的 一 个 关 联 滤 子， 如 果 对任意x , y , z e l ， ( 3 ) i j; ( 4 ) 若x - - y 6 j , x - + 伽峥约e j 若对任意关联滤子k, kcj 则x - + z e j. 则称j 是最大关联滤子. 定理1 . 4 . 6 a ” 设l 是一个格蕴涵代数，j cl ， ( 1 )若j 是l 的关联滤子，则i 是l 的滤子; ( 2 ) l 是格h - 蕴涵代数当 且仅当:l 的每一滤子都是关联滤子. 西南交通大学博士研究生学位论文第 15 页 第二章基于格蕴涵代数的格值 模态命题逻辑及其归结方法的研究 本章研究基于格蕴涵代数的格值模态命题逻辑系统中的归结方法，主要完 成下列工作: 1 、 建 立格值模态命题逻 辑系统l 五 护( x ) 并 讨论它的 语义及 语法性 质; 2 、 讨论格值模态命题逻辑系统l 五 护( x ) 中的a 一 归结原理， 并给出具体的 归结算法. 夸 2 . 1 可能世界语义学 在经典逻辑中，传统的命题是不依赖时间和地点的，也就是说，命题的真 或假是无条件的.但在哲学逻辑中，情况却发生了变化.例如:考察 “ 芜橄舫 定关刃忍跪” 这个命题， 在1 9 99年它是正确的， 但现在却是错误的. 如果我们 把这个命题改为“ 芜林抓萝 经走芜国澎统 ， ， 那么它又是正确的. 该例表明， 即 使是对同一事物，在不同的限制条件下， 其反映的本质也不尽相同，这正代表 了哲学中发展的观点.其实， 在现实世界中， 这样的例子还很多， 如: “ 有一天 人类可能会飞上太空” 、 “ 地球一定是圆的” 、 “ 明天将要下雨”等等这类命题 有一个共同点，那就是:它们的真值不仅依赖于人们给出的解释，还与具体的 语言 环境有关，我们称这样的语言环境为可能世界. 其实， “ 可能世界” 一词首先源自 莱布尼兹的无矛盾可能性思想: 只要事物 的情况或事物情况的组合推不出逻辑矛盾，该事物的情况或事物情况的组合就 是可能