首页 | 本学科首页   官方微博 | 高级检索  
相似文献
 共查询到17条相似文献,搜索用时 109 毫秒
1.
描述两个模型的模态等价性,同态显得太弱,同构又显得太强,寻找一个介于同态与同构之间的概念就导致了互模拟的产生。在模态逻辑中,互模拟沿着同态-强同态-有界态射-互模拟的轨迹而产生。在无穷模态语言的背景下或在像有穷的克里普克模型上,两个模型模态等价当且仅当它们是互模拟的。今天,互模拟在模态逻辑、集合论和计算机科学等领域中得到广泛的应用,显示了互模拟强大的理论价值和实践价值。  相似文献   

2.
首先介绍模态逻辑的两种语义:克里普克模型和非良基集合模型,表明这两种语义的相互可推演性,证明非良基模型,描述互模拟等价的克里普克模型类;接着,从模型的视角讨论集合上的互模拟与模态等价的关系;最后,运用互模拟和集合翻译等概念讨论非良基集合与模态逻辑的关系,证明:"一个集合论公式在集合上的互模拟下是不变的当且仅当它等价于一个模态公式的标准集合论翻译"。  相似文献   

3.
互模拟已成为模态逻辑模型论的一个核心概念。笔者在克里普克模型上定义了互模拟和互模拟不变性概念,接着证明模态逻辑具有互模拟不变性,最后讨论了互模拟与模态等价之间的关系。  相似文献   

4.
文[1]中给出模态描述逻辑MALC的语法与语义,同时给出MALC两个模型之间的互模拟关系,讨论MALC的模型之间互模拟及互模拟所组成集合具有的代数性质。  相似文献   

5.
给出两个矩阵范畴Mz和MZ[I]中态射满单分解的等价条件,并利用该等价条件讨论了这两个范畴中态射Moore-Penrose逆之间的关系.  相似文献   

6.
以标号迁移系统为工具,探讨了系统行为的等价性问题,构建了模拟及互模拟关系的形式化模型,进而将互模拟的概念推广到了系统的层面,进一步探讨了模拟及互模拟关系的性质,揭示了互模拟概念的本质,为其在形式化分析及验证技术中的应用提供了基础。  相似文献   

7.
定义了范畴中态射集的Baksalary-Hauke序,给出了它的等价刻划,并讨论了它与态射集星形序之间的关系。  相似文献   

8.
目的:研究BCH-代数中P-半单元的性质。方法:通过在BCH-代数中引入P-半单元的概念,利用BCH-代数本身的特点和性质来研究P-半单元的性质.结果:给出了P-半单元的一系列等价条件,证明了由每一个P-半单元可以诱导出一个交换半群,并给出了该交换半群成为交换群的条件.结论:本文将BCH-代数中的P-半单元与交换半群联系了起来,并证明了不同的P-半单元所诱导的交换半群是同构的.  相似文献   

9.
引入了商序映射、商序满(单)射与商序同构的概念,得到了商序映射与商序同构的一些重要性质,给出了商序映射是商序同构的条件,并讨论了商序同构、偏序同构与格同构的关系.  相似文献   

10.
为了探索Kripke模型、非良基集合和知识结构之间的联系,引入了有界互模拟的概念。首先,在Kripke模型上定义了互模拟与有界互模拟,并给出了模态逻辑的非良基模型定义和知识结构模型定义,证明后两类模型分别表达了Kripke模型的互模拟类和有界互模拟类;其次,证明了有界互模拟怎样被无穷模态逻辑的特定部分所刻画和通过Ehrenfeucht游戏来刻画;最后,给出了一些学者在不同的情景下证明的一些结果,使用互模拟和有界互模拟概念证明它们之间的关系。  相似文献   

11.
Using Baire metric, this paper proposes a generalized framework of transition system approximation by developing the notions of approximate reachability and approximate bisimulation equivalences. The proposed framework captures the traditional exact equivalence as a special case. Approximate reachability equivalence is coarser than approximate bisimulation equivalence, just like the hierarchy of the exact ones. Both approximate equivalences satisfy the transitive property, consequently, they can be used in transition system approximation.  相似文献   

12.
模拟和互模拟是分析模态逻辑的表达能力的一个强有力的工具.巴德尔(Baader)率先提出,可以运用描述图之间的模拟关系来分析描述逻辑的包含推理,并证明了在概念定义式循环术语集限制下,描述逻辑EL的包含推理是多项式时间复杂的.本文分析了描述逻辑模拟关系的研究现状和存在的问题,给出一般情形描述逻辑EVL下的模拟关系及其性质.  相似文献   

13.
本文证明分次模态逻辑在有穷传递框架类中的Goldblatt-Thomason定理.一个有穷传递框架类可由分次模态公式集定义当且仅当它在不相交并、生成子框架和分次有界态射像下封闭.该定理的证明使用带根的有穷传递框架的分次Jankov-Fine公式.  相似文献   

14.
As a variant of process algebra, π-calculus can describe the interactions between evolving processes. By modeling activity as a process interacting with other processes through ports, this paper presents a new approach: representing workflow models using π-calculus. As a result, the model can characterize the dynamic behaviors of the workflow process in terms of the LTS (Labeled Transition Semantics) semantics of π-calculus. The main advantage of the workflow model's formal semantic is that it allows for verification of the model's properties, such as deadlock-free and normal termination. Moreover, the equivalence of workflow models can be checked through weak bisimulation theorem in the π-calculus, thus facilitating the optimization of business processes.  相似文献   

15.
为了解决进程接收具体信息的输入所带来的无穷种迁移问题,采用一种称为"符号化"的方法,提出了进程符号环境和符号化和格局标号迁移语义,为Spi演算设计了符号互模拟关系—符号Reded互模拟.结果表明:该符号互模拟关系对传统的互模拟关系是可靠的,符号化的标号转移语义将进程无穷输入导致的迁移限期为有穷种迁移.因此使得基于该关系的安全协议自动验证算法得以实现.  相似文献   

16.
凯撒问题是当代分析哲学中的热门话题,许多学者都尝试为凯撒问题提供解决方案,林奈博给出关于区分范畴种类的元语义学方案、乌兹奎亚纳给出关于区分必然对象和偶然对象的模态方案、库克给出关于区分抽象原则的等价关系和等价类方案。然而,这些方案都不能最终解决凯撒问题。凯撒问题的哲学意义在于解决这个问题的尝试为我们带来了新的研究方法和新的研究方向,从而把分析哲学的研究引向深入。  相似文献   

17.
模糊性是自然语言的本质特征之一。模糊词汇也广泛地存在于法律语言中。综合分析法律英语中的法律术语、普通词汇转化为法律词汇、古语、外来语、缩略语、情态动词等词汇的模糊性及其语用意义,并探索了法律词汇的语意对等、功效对等和模糊消除等的三种翻译策略。  相似文献   

设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号