探析基于格蕴涵代数的格值逻辑系统及格值归结原理的研究

《探析基于格蕴涵代数的格值逻辑系统及格值归结原理的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、西南交通大学博士学位论文基于格蕴涵代数的格值逻辑系统及格值归结原理的研究姓名：刘军申请学位级别：博士专业：交通信息工程及控制指导教师：诸昌钤;徐扬19981101摘戮要I}经典逻鞲姥研究一蛊是人工智镪镇壤申非常受人关注酶一令掰突方向。弱前，基于非经典逻辑的自动定理证明系统由于窀加速了人工智能的发展尚正愈采愈il匙人们的广泛重观。本文在借烬国内外该镊城研究成恭的基础上，对疆播蕴涵代数为冀值城的谘值遗裤系统及基于这种播德逶辑系统磷建立的一种格值自动推理⋯格值归结原理与方'法作了较细致的研究。主要做了滋下三方面魏王谗：1．荚于格数涵代数的研究，i

2、本文在已有的袼蕴涵代数研究结果藤础上，首先研究了格藻涵代数中蕴涵滤子、崇蕴涵滤予、极大蕴涵滤子和超滤等的性矮和趣至的关系，然后重点较系统拖研究了两类覆蘸面较广酶袼簸涵代敬：完备的且源予的格簸涵代数和内射的格蕴涵代数。对前者，研究了表示问题，并证明了表示定嫂，从而给鑫了藏囊络蕴涵戒数的缍药特征窝画；对蘑孝，舜}究了葵中馥手代数娃质、积代数性质，并给出丁它的一些结构特征刻画。由于前者包含了有限的格蕴涵戎数，后老是一类晃隈穗格蕴涵代数，虽察是i#链结魏，嚣雨葜骞较广泛的意义。这些研究结瀑为建立格值逻辑系统中的一娅重要髂论奠定了很好畿基础。一．，歹

3、，2．基于格蕴涵代数的格檬逻辑系统的研究；拳文蒸予己寄的辑究工嚣躐及奉交燕子貉蕴涵代数鞠研究结果，首先研究了格值命题逻辑系统LP(X)中的协调性、可满足紧性等逻辑性质，然后萋螯深入探鸯了三P{弱斡宛蚤蛙藏题。建立了：《1)基于Lukasiewiez骞隈链的榕值命题逻辑系统工P(柳的完钰性定理；(2)瓣于完备的且原子的格蕴涵代数砖播馕命题逻姆系统LP(X)的完备拣定理；{3≥基于恕拳戆格蕴满伐数的格值命题逻辑系统￡，∞的完督性定理。这些研究结暴进一步丰富和完善了格值令题逻辑系统￡P∞。经典逻撂申，Horn子奄逻辑理论其毒广泛镑应躅，因而，本文

4、中特别建立了基于格蕴涵代数的格值．类Horn子句逻辑，并证明了可靠性和完备性定蠼，这为建立一类基于格值逻辑这种##经典邋辑鲢人工磐鬻{毒害将产生重要蟪锋焉。。。一摘要3．基于格蕴涵代数的格值逻辑中归结推理的理论与方法研究，{归结原理由于其简洁性一直是自动定理证明中一个受到广泛重视的研究领域，因而建立基于非经典逻辑的归结方法对于非经典自动定理证明有着重要的意义。本文在已构建的基于格蕴涵代数的格值逻辑系统的基础之上，探讨了其中的归结推理的理论与方法。首先探讨了一类可化为某种广义范式的格值命题逻辑公式的有效性问题，给出了判定几种定义下的此类公式可

5、满足性的归结方法，并证明了归结方法的可靠性和完备性。进一步，类似于经典情形下寻求判定一个公式恒真的半可判定算法，建立了判定基于格蕴涵代数的格值逻辑中一类格值公式在一定真值水平口下恒假(即甜恒假)的a-归结方法，并证明了其可靠性和完备性。针对经典归结以及一些非经典归结方法中对蕴涵联结词假设的局限性，又探讨了可处理格蕴涵代数中蕴涵联结词的格值类归结方法，给出了可靠性定理。作为特殊情形，特别研究了基于格蕴涵代数的格值Horn子句的类归结方法，并对建立其上的格值Prolog语言作了一定的探讨。j，，。．【关键词l格蕴涵代数格值命题逻辑自动定理证明归

6、结原理——垒曼!!堡垒!!．．!!ABSTRACTTheresearchofnon—classicallogichasalwaysbeenaveryattractivedirectionofartificialintelligence．Inrecentyears，automatedtheoremprovingbasedonnon—classicallogics，whichspeedupthedevelopmentofartificialintelligence，hasbeenpaidcloseattentionbymanyresearche

7、rs．Usedthepreviousinternalandexternalstudyinthesedirectionforreference，theauthorstudiedalattice·—valuedlogicsystemwithtruth-valuesinlatticeimplicationalgebras，onthebasisofwhich，wealsodiscussedindetailsaboutthelattice—valuedautomatedreasoning--lattice—valuedresolutionprinci

8、pleandmethods．Thespecificcontentsareasfollows：1．Thestudyoflatticeimplicationalgebras．Onth