基于语境依赖语义的公开宣告逻辑矢列演算系统
发布时间：2019-04-22 18:31
【摘要】：公开宣告逻辑被广泛用于刻画在公开交流中知识的变化的推理问题,然而,公开交流下知识的表示和推理往往是复杂而多变的,虽然PAL语义一定程度上刻画了宣告行为引起的知识变化,但面对复杂的知识推理,需要一个更容易把握证明内定理思路的推演系统。一个可行的解决方案是构造公开宣告逻辑的带标的矢列演算系统,然而现有的G3PAL和GPAL都不同程度的存在一些问题。本文在总结前人研究的基础上,结合“语境依赖”语义构造新的PAL矢列演算系统G3PALC。首先表明G3PALC能够证明某些G3PAL中不能证明的内定理,并且G3PALC不需要针对宣告组合公理添加额外的规则。另外,G3PALC相对于GPAL而言,不需要添加相应的关系表达式规则,并且能够不借助引理直接证明宣告组合公理,同时G3PALC还具有GPAL所不具有的G3型系统特点,即收缩规则和弱化规则在系统内都是可允许的。最后我们证明G3PALC与HPAL和GPAL系统之间的等价性,以及语境依赖语义与删除世界语义和删除关系语义的等价性。本文结构安排如下:第一章:前言部分,介绍研究背景和研究现状。第二章:对公开宣告逻辑的标准语义和公理化系统HPAL进行介绍,并简述HPAL证明可靠性和完全性的一般方法。第三章:介绍公开宣告逻辑已有的矢列演算系统G3PAL和GPAL,并对两者的优缺点进行讨论。第四章:在G3PAL和GPAL的基础上,依据语境依赖语义构造公开宣告逻辑的矢列演算系统G3PALC,指出它相对于G3PAL和GPAL的优势,并证明它的可靠性和完全性,它与G3PAL和GPAL的等价性,以及语境依赖语义与标准语义和删除世界语义的等价性。
[Abstract]:Public declaration logic is widely used to describe the change of knowledge in open communication. However, the representation and reasoning of knowledge in open communication are often complex and changeable. Although the semantics of PAL depict the change of knowledge caused by declarative behavior to some extent, facing the complex knowledge reasoning, we need a inference system which is easier to grasp the idea of proving the inner theorem. A feasible solution is to construct a vector calculus system with open declaration logic. However, the existing G3PAL and GPAL have some problems in varying degrees. On the basis of summarizing the previous studies, this paper constructs a new PAL vector sequence calculus system G3PALC based on the semantic meaning of "context dependence". First, it is shown that G3PALC can prove some inner theorems which cannot be proved in G3PAL, and G3PALC does not need to add additional rules to declare combinatorial axioms. In addition, compared with GPAL, G3PALC does not need to add corresponding relational expression rules, and can directly prove the declared combination axiom without Lemma. At the same time, G3PALC also has the characteristics of G3 system that GPAL does not have. That is, shrinkage rules and weakening rules are allowed in the system. Finally, we prove the equivalence between G3PALC and HPAL and GPAL systems, as well as the equivalence between context dependent semantics and deletion world semantics and deletion relational semantics. The structure of this paper is as follows: chapter one: preface, introduces the research background and research status. In chapter 2, the standard semantics and axiomatic system HPAL of open declaration logic are introduced, and the general methods of proving reliability and completeness of HPAL are briefly described. In chapter 3, we introduce the vector sequence calculus system G3PAL and GPAL, and discuss their advantages and disadvantages. Chapter 4: on the basis of G3PAL and GPAL, the vector sequence calculus system G3PALC is constructed according to context-dependent semantics. It points out its advantages over G3PAL and GPAL, and proves its reliability and completeness. It is equivalent to G3PAL and GPAL. And the equivalence of context dependent semantics with standard semantics and deleted world semantics.
【学位授予单位】：西南大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：B812.3
本文编号：2463090
[Abstract]:Public declaration logic is widely used to describe the change of knowledge in open communication. However, the representation and reasoning of knowledge in open communication are often complex and changeable. Although the semantics of PAL depict the change of knowledge caused by declarative behavior to some extent, facing the complex knowledge reasoning, we need a inference system which is easier to grasp the idea of proving the inner theorem. A feasible solution is to construct a vector calculus system with open declaration logic. However, the existing G3PAL and GPAL have some problems in varying degrees. On the basis of summarizing the previous studies, this paper constructs a new PAL vector sequence calculus system G3PALC based on the semantic meaning of "context dependence". First, it is shown that G3PALC can prove some inner theorems which cannot be proved in G3PAL, and G3PALC does not need to add additional rules to declare combinatorial axioms. In addition, compared with GPAL, G3PALC does not need to add corresponding relational expression rules, and can directly prove the declared combination axiom without Lemma. At the same time, G3PALC also has the characteristics of G3 system that GPAL does not have. That is, shrinkage rules and weakening rules are allowed in the system. Finally, we prove the equivalence between G3PALC and HPAL and GPAL systems, as well as the equivalence between context dependent semantics and deletion world semantics and deletion relational semantics. The structure of this paper is as follows: chapter one: preface, introduces the research background and research status. In chapter 2, the standard semantics and axiomatic system HPAL of open declaration logic are introduced, and the general methods of proving reliability and completeness of HPAL are briefly described. In chapter 3, we introduce the vector sequence calculus system G3PAL and GPAL, and discuss their advantages and disadvantages. Chapter 4: on the basis of G3PAL and GPAL, the vector sequence calculus system G3PALC is constructed according to context-dependent semantics. It points out its advantages over G3PAL and GPAL, and proves its reliability and completeness. It is equivalent to G3PAL and GPAL. And the equivalence of context dependent semantics with standard semantics and deleted world semantics.
【学位授予单位】：西南大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：B812.3
【相似文献】
相关期刊论文 前7条
1 赵祖军;;试论地理学公理系统[J];安徽师大学报(自然科学版);1984年02期
2 林夏水;论数学的本质[J];哲学研究;2000年09期
3 李娜;;一个含有原子的自然模型∑(A)[J];逻辑学研究;2008年03期
4 王琼;浅谈中学几何公理系统[J];西藏大学学报(汉文版);1994年02期
5 李醒民;;科学公理:基本概念和基本假设[J];江苏社会科学;2007年05期
6 张清宇;;A命题的系统[J];毕节学院学报;2010年11期
7 柳昌清;渗透集合论及辩证逻辑的公理系统论纲[J];中州学刊;1988年03期
相关会议论文 前1条
1 马垣;;连接依赖的有效完备公理系统[A];第十届全国数据库学术会议论文集[C];1992年
相关博士学位论文 前1条
1 舒新峰;投影时序逻辑的完备公理系统与形式验证[D];西安电子科技大学;2010年
相关硕士学位论文 前3条
1 党学哲;基于语境依赖语义的公开宣告逻辑矢列演算系统[D];西南大学;2017年
2 张威;可观测共变—逆变模拟及其公理系统的研究[D];南京航空航天大学;2014年
3 梁东芝;从欧氏几何的公理模式到希尔伯特的公理化思想[D];山西师范大学;2014年
，本文编号：2463090
本文链接：https://www.wllwen.com/shekelunwen/ljx/2463090.html
