Logical Characterizations of Fuzzy Bisimulations in Fuzzy Modal Logics over Residuated Lattices
描述逻辑中的模糊自动机、模糊标号转移系统、模糊Kripke模型和模糊解释等模糊结构之间存在清晰和模糊两种互模拟。完全剩余格上的模糊自动机之间的模糊互模拟已经在2012年由Kririć等人引入。扇入在2015年（分别是Nguyen等人在2020年）提供了剩余格[0，1]上具有Gödel t-范数的模糊Kripke模型（分别是描述逻辑中的模糊解释）之间模糊互模拟的逻辑刻画。一般剩余格上的模糊图结构之间的模糊互模拟缺乏逻辑刻画，剩余格[0，1]上的模糊图结构之间的模糊互模拟也缺乏逻辑刻画.本文给出并证明了剩余格上模糊模态逻辑中模糊互模拟的逻辑刻画。所考虑的逻辑是模糊命题动态逻辑及其片段。我们的逻辑刻画涉及模糊互模拟下公式的不变性和模糊互模拟的Hennessy-Milner性质。它们可以重新表述为其他模糊结构，如模糊标签转换系统和描述逻辑中的模糊解释。
2021-06-15 cs.LO
Bisimulation-Based Comparisons for Interpretations in Description Logics
我们研究比较描述逻辑的解释方面的“逻辑后果”的形式半积极的概念（如半积极的概念断言）。这种比较的特点是由类似的互模拟的条件。在所考虑的逻辑中最简单的是PDL（命题动态逻辑）的变体。其他的扩展，逻辑与逆角色，名词，量化的数量限制，通用的角色，和/或概念构造器表示的局部自反性的角色。所研究的问题是：关于比较的半正概念的保持，用于比较的Hennessy-Milner性质，以及保持半正概念的解释的最小化。
2013-04-20 cs.LO
Cyclic Datatypes modulo Bisimulation based on Second-Order Algebraic Theories
循环数据结构，如循环列表，在函数式编程中由于其循环性而难以处理。本文研究了循环数据集的范畴、代数和计算基础。我们的循环数据库框架是基于Fiore等人的二阶代数理论，其给出了用于描述和推理循环数据集的语法、类型和计算规则的统一设置。我们从Bloom和Esik的迭代范畴的范畴语义中提取“折叠”计算规则。因此，规则通过构造是正确的。我们证明了强规范化使用一般模式标准的二阶计算规则。而不是不动点定律，我们特别选择Bekic定律进行计算，这是获得强归一化的关键。我们还证明了计算规则的“Church-Rosser模互模拟”性质。综合这些结果，我们得到了循环资料方程理论与褶曲的显著判别结果。
2017-11-14 cs.LO
On Bisimulations for Description Logics
我们研究互模拟有用的描述逻辑。所考虑的逻辑中最简单的是$\mathcal{ALC}_{reg}$（PDL的变体）。其他的扩展，逻辑与逆角色，名词，量化的数量限制，通用的角色，和/或概念构造器表示的局部自反性的角色。它们也允许角色公理。我们给出的结果不变性的概念，TBox和ABoxes，保持RBoxes和知识库，和Hennessy-Milner性质w.r.t.在所考虑的描述逻辑的互模拟。使用不变性的结果，我们比较所考虑的描述逻辑w.r.t.概念、TBox和ABoxes。我们关于分离描述逻辑的表达性的结果自然地扩展到当我们有扩展$\mathcal{ALC}$的$\mathcal{ALC}_{reg}$的任何子逻辑而不是$\mathcal{ALC}_{reg}$的情况。我们还提供了最大的自互模拟和商的解释w.r.t.的结果。这种等价关系。这些结果对于描述逻辑中的最小化解释和概念学习是有用的。为了处理最小化解释的情况下，所考虑的逻辑允许量化的数量限制和/或构造函数的局部自反性的作用，我们引入了一个新的概念，称为QS-解释，这是需要获得预期的结果。通过采用Hopcroft的自动机极小化算法和Paige-Tarjan算法，我们给出了计算有限解释最大自互模拟所对应的划分的有效算法。
2015-02-19 cs.LO
The temporal logic of coalitional goal assignments in concurrent multi-player games
我们介绍和研究交替时间时序逻辑ATL的自然扩展，称为联盟目标的时序逻辑（TLCGA）。它的特点是只有一个，但很有表现力，联盟战略运营商，即联盟目标分配运营商，这是基于映射分配给游戏中的每组球员的联盟目标，形式化的TLCGA语言的路径公式，即一个公式前缀与时间运营商X，U，或G，代表相应的联盟的时间目标，描述满足该目标的策略的属性。建立了TLCGA的μ-演算扩展中时间目标分配的不动点刻画，讨论了它的表达性并举例说明，证明了它相对于适当定义的互模拟概念的互模拟不变性和Hennessy-Milner性质，构造了TLCGA的一个完善的公理系统，并通过有限模型性质得到了它的可判定性.
2022-02-22 cs.GT cs.LO cs.MA
Uniform Interpolation for Propositional and Modal Team Logics
在本文中，我们考虑模态组逻辑，经典模态逻辑的推广，它是可能的数据之间的依赖现象描述。我们证明，最有名的片段全模态团队逻辑允许消除所谓的“存在互模拟量词”，其中存在的某个集合是模互模拟。因此，我们证明了这些片段享有一致插值性质。
2018-10-12 cs.LO
Bisimulation and bisimilarity for fuzzy description logics under the Gödel semantics
描述逻辑（DL）是一个合适的形式主义表示领域的知识，其中对象描述不仅由属性，但也由对象之间的二元关系。模糊扩展的DL可以用于这样的领域时，他们的数据和知识是模糊和不精确的。在这样的领域中指定对象类的可能方法之一是使用模糊DL中的概念。由于DL是模态逻辑的变体，DL中的不相容性的特征在于双相似性。解释的双相似关系是该解释的最大自互模拟。在DL及其模糊扩展中，这种等价关系可以用于概念学习。本文定义并研究了Gödel语义下模糊逻辑的模糊互模拟和双相似性，以及扩展了对合否定的模糊逻辑的清晰互模拟和强双相似性。所考虑的逻辑是模糊扩展的DL $\mathcal{ALC}_{reg}$（PDL的一个变种）与其他功能之间的逆角色，名词，（合格或不合格）的数量限制，普遍的作用，局部自反的作用和对合否定。我们制定和证明结果不变性的概念下模糊（分别）。清晰）互模拟，条件不变性的模糊TBoxex/ABoxes下的双相似性（分别）。强双相似性），和模糊的Hennessy-Milner性质（分别为）。清晰）互模拟的模糊DL没有（分别）。Gödel语义学下的对合否定。除了这些基本的结果，我们还提供了使用模糊互模拟分离模糊DL的表达能力，以及使用强双相似性，以尽量减少模糊解释的结果。
2020-08-06 cs.LO
Neighborhood Contingency Logic: A New Perspective
在本文中，我们提出了一个新的邻域语义的权变逻辑，通过引入一个简单的性质，在标准的邻域模型。这简化了（Fan and van Ditmarsch，2015）中给出的邻域语义，但不会改变有效公式的集合。在此基础上，在互模拟的各种概念和Hennessy-Milner定理中，我们证明了$c$ -互模拟等价于文献中的nbh- $Δ$ -互模拟，从而引导我们理解后者概念的本质。这个视角也提供了各种框架可定义性和公理化结果。
2018-02-07 cs.LO math.LO
Reasoning About Bounds in Weighted Transition Systems
本文提出一种推理加权转移系统中转移权重界限的方法，引入更粗的互模拟概念，并设计定制模态逻辑，证明其不变性、有限模型性质、完备公理化及可判定性。
2018-11-23 cs.FL cs.LO
Towards a Model Theory of Ordered Logics: Expressivity and Interpolation (Extended version)
我们考虑家庭的保护和无保护有序逻辑，构成一个最近重新发现的家庭的可判定的片段的一阶逻辑（FO），其中的顺序量化的变量一致的顺序，这些变量出现作为参数的谓词。虽然他们的可满足性问题的复杂性现在已经很好地建立起来，但是他们的模型理论却知之甚少。本文的目的是提供一些见解。我们首先提供了合适的概念，有序逻辑的互模拟。接下来，我们采用互模拟来比较有序逻辑的相对表达能力，并将我们的逻辑描述为FO a la van Bentham的互模拟不变片段。然后研究了Craig插值性质~（CIP）。我们驳斥了另一个说法，从臭名昭著的工作珀迪，通过显示，长笛和向前的碎片不享受CIP。我们补充这一结果表明，有序片段和保护有序逻辑享有CIP。这些积极的结果依赖于新的和相当复杂的模型结构，充分利用了我们的逻辑的“forwardness”。
2022-06-23 cs.LO
Uniform Interpolation in Distributed Knowledge Modal Logics
Jinan University（暨南大学）
本文研究了分布式知识模态逻辑中的统一插值性质，通过扩展经典公式和字面消除框架，引入集体p-仿射概念，证明了六种分布式知识模态逻辑的统一插值性质。
2026-03-30 cs.LO
Querying the Guarded Fragment
针对一个受保护的一阶理论F评估一个布尔合取查询Q等价于检查“F而不是Q”是否不可满足。这个问题与数据库理论和描述逻辑领域有关。由于Q可能不是被保护的，关于保护片段的可判定性、复杂性和有限模型性质的已知结果在保护理论上并不明显地延续到合取查询应答，并且通常是开放的。通过研究超图和关系结构的有限保护双相似覆盖，并通过大量推广罗萨蒂的有限追逐，我们证明了保护理论F和（工会）合取查询Q，（i）Q是真的，在每个模型的F当且仅当Q是真的，在每个有限模型的F和（ii）确定F是否意味着Q是2 EXPTIME-完全的。我们进一步证明了以下结果：（iii）任意超图的多项式大小共形覆盖的存在性;（iv）最优保护片段的有限模型性质的一个新证明;（v）具有最优界的保护片段的小模型性质;（vi）规范化问题模保护互模拟的多项式时间解，其产生（vii）保护互模拟不变PTIME的捕获结果。
2014-05-20 cs.DB cs.LO
Uniform Interpolation of Basic Tense Logic
Faculty of Humanities and Human Sciences, Hokkaido University（北海道大学人文学部人类科学学院）
本文通过扩展Visser的语义论证，证明了基本时态逻辑（双向模态逻辑）具有一致插值性质。
2026-07-01 cs.LO
Losing Connection:the Modal Logic of Definable Link Deletion
在这篇文章中，我们从一个两人游戏开始，该游戏模拟了日常生活中不利环境下的通信，并从图的模态逻辑的角度研究它，其中可以根据对抗玩家可用的定义在本地删除链接。我们首先介绍一种新的语言，语义，和一些典型的有效性。然后，我们制定了一种新的类型的一阶翻译的模态逻辑，并证明其正确性。然后，提出了一个新的互模拟的概念，导致一个特征定理的逻辑作为一个片段的一阶逻辑，并进一步调查其表达能力对混合模态语言。接下来，我们讨论如何公理化这个逻辑的链接删除，使用动态认知逻辑作为对比。最后，我们证明了新的模态逻辑既缺乏树模型性质，又缺乏有限模型性质，并且它的可满足性问题是不可判定的。
2019-03-05 cs.LO
Extensions of K5: Proof Theory and Uniform Lyndon Interpolation
本文提出 K5 及其多种扩张的分层矢列式演算，得到复杂度最优判定程序，并首次以构造性句法方法证明 K5 具有一致 Lyndon 插值性质。
2023-07-21 cs.LO math.LO
Intuitionistic Linear Temporal Logics
Toulouse University（图卢兹大学）；ENIB（法国国立布雷斯特工程师学院）；Ghent University（根特大学）
我们认为直观的线性时序逻辑的变种与“下一个”，“直到”和“释放”的基础上扩大偏序集：偏序配备了保序过渡函数。这类结构产生了一个逻辑，我们表示为$\iltl$，并通过施加额外的约束，我们得到的逻辑$\itlb$持久偏序集和$\itlht$这里和那里的时间逻辑，这两个都已被认为是在文献中。我们证明了$\iltl$具有有效的有限模型性质，因而是可判定的，而$\itlb$不具有有限模型性质.我们还介绍了这些逻辑的有界互模拟的概念，并使用它们来表明，“直到”和“释放”运营商是不可定义的，即使在类的持久偏序集。
2019-12-30 cs.AI cs.LO cs.SC
A Lindström Theorem for Fitting's Modal Logic over a Finite Heyting Algebra
Department of Mathematics, Mahishadal Raj College（马希沙达尔学院数学系）
该研究针对Maruyama提出的带精确真值测试的Fitting有限Heyting值模态逻辑，建立Lindström极大性定理，证明满足紧致性、Tarski并性质及互模拟强不变的抽象扩展与原逻辑表达等价，且扩展公式的精确值纤维可被定义。
2026-08-18 cs.LO
The expressive power of modal logic with inclusion atoms
模态包含逻辑是基本模态逻辑的包含原子扩展，其语义定义在Kripke模型上。Kripke模型的团队只是其域的一个子集。本文给出了模态包含逻辑表达能力的一个完整刻画：一类带队的Kripke模型在模态包含逻辑中是可定义的当且仅当它在k-互模拟下是闭的，对于某个整数k，它在并下是闭的，并且它具有空队性质.我们还证明了同样的表达能力，可以通过添加一个单一的一元非空算子模态逻辑。此外，我们建立了一个指数下界的大小从模态包含逻辑到模态逻辑与非空算子的翻译。
2015-09-24 cs.LO math.LO
Lindstrom theorems for fragments of first-order logic
林斯特伦定理用模型论的条件来描述逻辑，如紧性和Löwenheim-Skolem性质。大多数现有的这类刻画关注一阶逻辑的扩展。但另一方面，与计算机科学相关的许多逻辑是一阶逻辑的片段或片段的扩展，例如，k变量逻辑和各种模态逻辑。寻找这些语言的Lindström定理可能具有挑战性，因为大多数已知的技术依赖于编码参数，这些参数似乎需要一阶逻辑的全部表达能力。本文给出了一阶逻辑的几个片段的Lindström定理，包括k>2的k-变量片段，Tarski关系代数，分次模态逻辑和二元保护片段。我们使用两种不同的证明技术。一个是对原始林斯特龙证明的修改。另一个涉及互模拟，树解开，有限深度的模态概念。我们的研究结果也暗示语义保持定理。
2009-08-04 cs.LO
A non-uniform view of Craig interpolation in modal logics with linear frames
King's College London（伦敦国王学院）；University of Liverpool（利物浦大学）；Birkbeck, University of London（伦敦大学伯贝克学院）
针对线性传递框架上的模态逻辑缺乏 Craig 插值性质的问题，提出非均匀方法研究插值存在性判定问题，证明对包含 K4.3 的有限公理化逻辑该问题可判定且为 coNP-完全。
2026-06-18 cs.LO math.LO
Modal Logic with Relations over Paths: a Theoretical Development through Comonadic Semantics
本研究提出路径谓词模态逻辑PPML，通过共单子语义建立其模型论性质，关联DataGL等数据感知逻辑与基本模态逻辑，实现多项式时间归约。
2024-08-14 cs.LO
A Common Ancestor of PDL, Conjunctive Queries, and Unary Negation First-order Logic
Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR5800（波尔多大学）；Universidad de Buenos Aires, FCEN, DC & CONICET-UBA, ICC（布宜诺斯艾利斯大学）
本文研究了UCPDL+逻辑，其包含PDL扩展、连接查询和单目否定一阶逻辑，探讨了其表达能力、可满足性和模型检查问题。
2026-10-20 cs.DB cs.LO
Term Graph Representations for Cyclic Lambda-Terms
我们研究了各种表示为循环的高阶或一阶项图。我们专注于“高次项图”（高次项图），这是一阶项图赋予了一个良好的范围功能，和他们的表示为“高次项图”，这是普通的一阶项图与范围顶点，满足一定的范围要求。具体来说，我们解决的问题：哪一类的一阶项图承认一个忠实的嵌入？在这个意义上，（i）的同态为基础的共享顺序的？我们系统地研究是否有一些类的ESTA项图有这个属性，我们发现一个特定的类ESTA项图，满足这一标准。该类的术语图由应用程序、抽象、变量和作用域顶点构建，并且具有后两种顶点具有到相应抽象的反向链接的特征。这一结果在理论上和算法上处理了高阶项图的子项共享的概念：我们获得了一个容易实现的方法来获得最大共享形式的高阶项图。此外，我们打开了可能性，拉回性能从一阶项图到双线性项图，性能，如完整的晶格结构的互模拟等价类的共享顺序。
2013-02-26 cs.LO cs.PL
