余代数模态逻辑若干问题的研究

《余代数模态逻辑若干问题的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、NanjingUniversityofAeronauticsandAstronauticsTheGraduateSchoolCollegeofComputerScienceandTechnologyResearchonSomeIssuesofCoalgebraicModalLogicAThesisinTheoreticalComputerSciencebyWuWenluAdvisedbyProf.ZhaohuiZhuSubmittedinPartialFulfillmentoftheRequirementsfortheDegreeofMasterofEngineering

2、December,2011承诺书本人声明所呈交的博/硕士学位论文是本人在导师指导下进行的研究工作及取得的研究成果。除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含为获得南京航空航天大学或其他教育机构的学位或证书而使用过的材料。本人授权南京航空航天大学可以将学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。（保密的学位论文在解密后适用本承诺书）作者签名：日期：南京航空航天大学硕士学位论文摘要余代数是一种基于状态刻画动态系统的数学结构，该结构以范畴上的自函子为参量可以统一描述常见

3、的动态系统，从而为研究动态系统的性质提供了抽象平台。余代数逻辑是用于描述余代数性质的逻辑语言，它是模态逻辑在余代数上的自然推广，它和余代数之间的关系类似于等式逻辑与代数之间的关系。本文将基于对偶理论对余代数模态逻辑若干问题开展研究，主要工作包括如下方面：1.基于对偶理论给出了Rank-1模态逻辑都有余代数语义的一种新的证明方法，并且证明通过对偶理论构造出来的函子和Schröder所构造的函子是等价的。2.对Rank-1模态逻辑的一步可靠性和一步完备性进行研究，证明了一步可靠性等价于ClemensKupke对偶理论中提出的d具有函数性，一步完备性等价于d是单射的，从而证明了

4、余代数模态逻辑都是Rank-1可公理化的。3.把布尔模态逻辑推广到余代数框架下，提出了模态词带布尔结构的余代数模态逻辑系统，并研究了其可靠完备性。关键词：余代数，余代数模态逻辑，斯通对偶，Rank-1模态逻辑，可靠性，完备性，布尔余代数模态逻辑I余代数模态逻辑若干问题的研究ABSTRACTCoalgebrashavebeenrecognizedasmodelsforalargevarietyofdynamicsystemsbasedonstates.Thetheoryofcoalgebrasissetupparametricinaparticularfunctorfors

5、omecategory,providingaunifyingframeworkfordifferenttypesofsystems.Onthelogicalside,modallogichasemergedastheadequatespecificationlanguageforcoalgebraicallymodelledsystems.Modallogicforcoalgebrasisdualtoequationallogicforalgebras.Thispaperaimstoexploresomeissuesofcoalgebraicmodallogicbased

6、onthetheoryofduality.Ourmainworkinvolves:1.WereprovebymeansofdualitytheorythatRank-1modallogicsarecoalgebraicandprovethatthefunctorweconstructisequivalenttothatofLutzSchröder.2.Westudytheone-stepsoundnessandone-stepcompletenessofrank-1modallogic,andshowthattheone-stepsoundnessisequivalent

7、tothatdisfunctionalandone-stepcompletenessisequivalenttothatdisinjectivefromClemensKupke’stheory.Further,wedrawtheconclusionthattheclassofcoalgebrasforanendofunctorcanalwaysbeaxiomatizedinrank-1.3.WeestablishthenotionofBooleancoalgebraicmodallogicandstudythesoundnes