Modal Reasoning = Metric Reasoning, via Lawvere
分级模态类型、系统和协同效应正在成为处理上下文相关计算的标准形式，其中代码使用起着核心作用。然而，模态语言和协同语言的程序等价理论，如果与这些语言的指称语义和操作语义相比，则相当不发达。这就提出了一个问题，即普通程序等价的理论在多大程度上可以在模态场景中给出。在这项工作中，我们表明，共归纳等价可以扩展到一个模态设置，我们这样做，通过推广阿布拉姆斯基的应用双相似coeffective行为。为了实现这一目标，我们开发了一个通用的理论，三元程序关系的基础上的新概念的comonadic宽松的扩展，在此之上，我们定义了一个模态扩展的Abramsky的应用bisimilarity（我们称之为模态应用bisimilarity）。我们证明这样的关系是一个一致性，这种方式获得一个组合技术推理模态和coeffective行为。但这并不是故事的结束：我们还建立了模态程序关系和程序距离之间的对应关系。这种对应关系表明模态应用双相似性和（适当扩展的）应用双相似性距离一致，这种方式揭示了模态程序等价性和程序距离只是同一枚硬币的两面。
2021-03-05 cs.LO
Minimal modal logics, constructive modal logics and their relations
提出一族对应经典模态逻辑的极小模态逻辑，通过两种独立但等价的方法定义，并揭示其与构造性模态逻辑CK的紧密关系，进而衍生出一族构造性模态逻辑。
2023-09-05 cs.LO
A Linear-logical Reconstruction of Intuitionistic Modal Logic S4
本文提出了一种“模态线性逻辑”，它将直觉模态逻辑S4（IS 4）用线性逻辑来表示，建立了从IS 4到它的Girard翻译的S4-版本。它对模态逻辑的扩展是非-这是微不足道的，因为S4模态和指数模态的简单组合导致两种模态之间的不期望的相互作用。为了解决这个问题，我们引入了一个扩展的直觉乘法指数线性逻辑与模态相结合的S4模态和指数模态，并表明它承认从IS 4的声音翻译。通过Curry-Howard对应，我们进一步得到了Pfenning和Davies为分阶段计算所提出的模态微积分的交互几何机器语义。
2019-04-24 cs.LO
Propositional modal logic with implicit modal quantification
命题项模态逻辑在具有无限多的可达性关系的Kripke结构上解释，因此语法允许变量索引模态和量化。这种逻辑是不可判定的，我们考虑一个变量自由命题的双模态逻辑与隐量化。因此，$[\forall] α$断言所有可及性关系上的必然性，而$[\exists] α$是某些可及性关系上的经典必然性。该逻辑是与一个自然的互模拟模型的关系，我们表明，该逻辑正是一个两个排序的一阶逻辑的互模拟不变片段。该逻辑很容易被看作是可判定的，并且承认有效公式的完全公理化。此外，决策过程自然地延伸到“捆绑片段”的完整术语模态逻辑。
2018-12-29 cs.LO
From Hybrid Modal Logic to Matching Logic and Back
建立在我们以前的工作混合多元模态逻辑，我们确定模态逻辑等价匹配逻辑，程序规范和验证的逻辑。这提供了一种严格的方法来在两种方法之间传输结果，这对两个系统都有好处。
2019-09-04 cs.LO
Undecidability of a Very Simple Modal Logic with Binding
我们展示了什么可以说是最简单的非子布尔模态逻辑的约束力的隐式概念的可满足性问题的不可判定性。这一工作丰富了从混合逻辑到记忆逻辑的关于模态逻辑不可判定性的一系列已有结果。
2015-08-14 cs.LO
A journey in modal proof theory: From minimal normal modal logic to discrete linear temporal logic
扩展和推广了Masini（1992）的2-序列方法，我们给出了经典模态逻辑在K，D，T，S4谱上的计算方法.系统以统一的方式呈现-通过调整单个参数，即对规则的适用性的约束，获得不同的逻辑。割消法只被证明一次，因为证明过程独立于产生不同系统的约束。给出了离散线性时态逻辑ltl的一个代数演算，并证明了其完备性。本文的主旨是模态和一阶量化之间的形式类比。
2020-01-07 cs.LO
Two variable fragment of Term Modal Logic
项模态逻辑（TML）是具有无限多模态的模态逻辑，在模态指数上量化，因此我们可以有$\exists y. \forall x. (\Box_x P(x,y) \supset\Diamond_y P(y,x))$形式的公式。像一阶模态逻辑一样，TML也是“臭名昭著的”不可判定的，在这个意义上，即使是非常简单的片段也是不可判定的。在本文中，我们证明了一个有趣的片段，即两个变量TML的可判定性。这与二变量一阶模态逻辑相反，二变量一阶模态逻辑是不可判定的。
2019-06-27 cs.LO
Intuitionistic modal logic LIK4 is decidable
Faculty of Arts and Sciences Istanbul Aydın University（伊斯坦布尔阿因大学文理学院）；Faculty of Mathematics and Informatics Sofia University St. Kliment Ohridski（索非亚大学克利门特·奥赫里德斯基数学与信息学院）
本文证明了直觉模态逻辑LIK4的可判定性。
2025-12-04 cs.LO
Coalescing: Syntactic Abstraction for Reasoning in First-Order Modal Logics
我们提出了一个句法抽象方法，通过使用标准一阶逻辑和命题模态逻辑的定理证明器来推理一阶模态逻辑。
2014-09-12 cs.LO
Explicit non-normal modal logic
针对道义模态的超内涵性问题，本文提出作为非正规模态逻辑超内涵对应物的新型证成逻辑，证明其可靠性与完全性，并研究实现问题。
2023-08-11 cs.LO
Modal Logics with Composition on Finite Forests: Expressivity and Complexity (Extra Material)
我们研究了有限森林上的两个模态逻辑的表达性和计算复杂性，这些模态逻辑配备了算子来推理子模型。逻辑ML（|）用复合运算符扩展了基本模态逻辑ML|而ML（*）包含来自分离逻辑的分离合取 *。虽然这两个算子都是二阶的性质，我们表明，ML（|）与分级模态逻辑GML（在有限树上）一样具有表达性，而ML（*）严格位于ML和GML之间。此外，我们建立了ML（*）的可满足性问题是塔完全的，而ML（|）是（仅）AExpPol-complete。作为一个副产品，我们解决了几个开放的姐妹逻辑，如静态环境逻辑，模态分离逻辑，有限树上的二阶模态逻辑的问题。
2020-07-16 cs.LO
Intuitionistic modal logics: new and simpler decidability proofs for FIK and LIK
本研究整合模态逻辑终止表方法与直觉主义模态逻辑IK的有穷框架性质，为FIK和LIK给出更简洁的全新可判定性证明。
2025-03-24 cs.LO
Higher Dimensional Modal Logic
高维自动机（HDA）是一种并发模型，可以表示大多数传统的偏序模型，如Mazurkiewicz迹，pomset，事件结构或Petri网。在Kripke结构上解释的模态逻辑是用于推理顺序行为和交叉并发的逻辑。模态逻辑是一阶逻辑的一个良好子集;模态逻辑的许多变体是可判定的。然而，对于更有表现力的HDA模型，没有类似模态的逻辑。在本文中，我们介绍和调查的模态逻辑HDAs，其中包括两个模态推理“期间”和“之后”。我们证明了这种一般的高维模态逻辑（HDML）是可判定的，并为它定义了一个公理系统，同时还说明了当HDA模型被限制为Kripke结构时，HDML的一个语法限制是如何成为标准模态逻辑的。然后，我们隔离类HDAs编码Mazurkiewicz痕迹，并显示如何HDML，与相应的直到运营商的自然定义，可以限制到LTrL（线性时间时序逻辑Mazurkiewicz痕迹）或分支时间ISTL。我们还研究了基本HDML语言wrt的表达能力。并得出结论，HDML捕获分裂互模拟。
2014-05-16 cs.LO
Flat modal fixpoint logics with the converse modality
我们证明了一个通用的完整性结果，一类模态不动点逻辑对应于平面片段的双向μ演算，延长早期的工作Santocanale和Venema。我们观察到，Santocanale和Venema的证明，至少不动点的Lindenbaum-Tarski代数的某些平坦的不动点逻辑是建设性的，使用有限伴随，不再工作时，逆模态介绍。相反，我们的完整性证明直接构建了一个模型的一致性公式，使用归纳规则的方式是类似于标准的完整性证明命题动态逻辑。这种方法结合了焦点的概念，这是以前使用的基于表格的模态不动点逻辑推理。
2017-10-12 cs.LO
Uniform Interpolation for Propositional and Modal Team Logics
在本文中，我们考虑模态组逻辑，经典模态逻辑的推广，它是可能的数据之间的依赖现象描述。我们证明，最有名的片段全模态团队逻辑允许消除所谓的“存在互模拟量词”，其中存在的某个集合是模互模拟。因此，我们证明了这些片段享有一致插值性质。
2018-10-12 cs.LO
Description logics as polyadic modal logics
我们研究标准描述逻辑到多元模态逻辑框架的扩展。我们通过一般关系代数，可以用来定义操作的关系，所有的arities促进一个自然的方法，这样的逻辑。作为一个具体的系统来说明我们的方法，我们调查的多元版本的ALC扩展与关系置换运算符和元组计数。本文的重点是概念性的，而不是技术性的。
2021-08-19 cs.LO
Modal Extensions of Generalised Nelson Logics
Institute of Computer Science, Czech Academy of Sciences（捷克科学院计算机科学研究所）
本文受相关认知逻辑启发，扩展Dunn的二元关系语义以适配RM的模态扩展，并证明所得模态公理与规则可为广义Nelson逻辑族中所有逻辑的模态扩展提供可靠且完备的公理化。
2026-10-08 cs.LO
Graphical Sequent Calculi for Modal Logics
模态图的语法是根据查尔斯·皮尔士（Charles Peirce）在他的存在图的图形逻辑的伽马部分中的符号定义的连续割和断割。正规模态逻辑的图演算是在经典命题逻辑的图演算的基础上发展起来的。这些图形演算具有深层推理的性质。模态逻辑的图演算和图演算之间的关系通过图和模态公式之间的转换来表示。
2017-03-07 cs.LO
Cathoristic logic: A modal logic of incompatible propositions
公理逻辑是一种多模态逻辑，其中否定被一个新的运算符所取代，允许表达不相容的句子。我们提出的语法和语义的逻辑，包括完整的证明规则，并建立了一些结果，如紧凑性，语义特征的基本等价，存在的二次时间决策过程，和随机的不相容语义属性。我们证明了有用的逻辑作为一种语言的知识表示。
2014-11-26 cs.LO
Strong Completeness of Coalgebraic Modal Logics
规范模型在模态逻辑中具有核心重要性，特别是因为它们证明了强完备性和紧性。虽然规范模型的构造对于Kripke语义是很好理解的，但非正规模态逻辑通常存在微妙的困难-直到规范模型可能不存在的程度，例如在大多数概率逻辑中就是这种情况。在这里，我们提出了一个通用的规范模型建设的语义框架的共代数模态逻辑，它精确定位的语法和语义之间的一致性条件，保证强完备性的模态逻辑。我们应用这种方法来重建典型的模型定理，无论是已知的或民间传说，而且实例化我们的方法，以获得新的强完备性结果。特别是，我们证明了强完备性的分次模态逻辑与有限的多重性，模态逻辑的精确概率。
2009-02-12 cs.LO
Local Intuitionistic Modal Logics and Their Calculi
本研究聚焦带局部模态算子的直觉主义模态逻辑，明确基础逻辑LIK与WK、IK的强弱关系，给出其公理化与双嵌套演算，同时提供判定及有穷反模型提取方法。
2024-03-11 cs.LO
Uniform Interpolation in Coalgebraic Modal Logic
一个逻辑有统一的插值，如果它的公式可以向下投影到给定的子签名，保留所有的逻辑后果，不提及删除的符号;较弱的属性（克雷格）插值允许投影公式-插值-是不同的每个逻辑后果的原始公式。这些性质是重要的，例如，逻辑理论的模块化。我们研究插值的上下文中的共代数模态逻辑，即模态逻辑公理化秩1，限制为清晰的情况下，许多模态。这种逻辑的例子包括模态逻辑K和KD，邻域逻辑及其单调变体，有限幺半群加权逻辑和联合逻辑。我们引入了一步（均匀）插值的概念，它只指一个限制逻辑没有嵌套的模态，并证明了一个共代数模态逻辑有均匀插值，如果它有一步插值。此外，我们确定保存有限的满射弱回调作为一个充分的，在单调的情况下，必要的一步插值的条件。因此，我们证明或reprove均匀插值的大多数例子上面列出的。
2022-05-01 cs.LO
A van Benthem Theorem for Fuzzy Modal Logic
我们提出了一个模糊（或定量）版本的范本特姆定理，其特点是命题模态逻辑作为一阶逻辑的互模拟不变片段。具体来说，我们考虑一阶模糊谓词逻辑及其模态片段，并表明，模糊一阶公式是非扩张的w.r.t.互模拟距离的自然概念正好是那些可以通过模糊模态公式来近似的概念。
2018-02-05 cs.LO
A van Benthem Theorem for Quantitative Probabilistic Modal Logic
在概率转换系统中，行为度量提供了比双相似性概念更细粒度和更稳定的系统等价性度量。它们与定量概率逻辑密切相关，事实上，在实数单位区间取值的概率模态逻辑引起的距离与行为距离一致。对于概率系统，概率模态逻辑扮演着类似于Hennessy-Milner逻辑在经典标记转移系统上的角色。在定量背景下，模态逻辑在双相似性下的不变性成为公式求值的非扩展性。行为距离在本文中，我们提供了一个表征的表达能力的概率模态逻辑的基础上，这一观察：我们证明了一个概率模拟的经典范Bentham定理，它指出，模态逻辑正是一阶逻辑的互模拟不变的片段。具体来说，我们表明，定量概率模态逻辑在于密集的双模拟不变片段，在非扩展公式评估的指示意义上，定量概率一阶逻辑;更确切地说，双模拟不变的一阶公式是近似的模态公式的有界秩。有关同一结果的描述逻辑透视图，请参见arXiv：1906.00784。
2019-06-04 cs.LO
Complexity through Translations for Modal Logic with Recursion
本文研究了经典模态逻辑的复杂性及其扩展与不动点算子，使用翻译转移结果跨越逻辑。特别是，我们通过翻译和从μ演算和模态逻辑，这使我们能够转移已知的上限和下限的多智能体逻辑的复杂性结果。我们还使用这些翻译介绍一个终止表系统的逻辑，我们研究的基础上，Kozen的表的μ演算，和一个拟合和Massacci模态逻辑。
2022-09-21 cs.LO
On Modal Logics of Partial Recursive Functions
经典的命题逻辑被认为是健全的和完整的集合语义解释连接词作为集合操作。在上述解释下，本文通过一种新的二元模态扩展了命题语言，该二元模态对应于部分递归函数类型构造器。确定性和非确定性的功能的情况下被认为是语义上完整的模态逻辑描述和这些逻辑的可判定性建立。
2004-07-12 cs.LO
On Transitive modal many-valued logics
本文主要研究由赋值Kripke框架定义的模态逻辑，特别是在某些剩余格上赋值传递Kripke框架的模态逻辑的可计算性和可表示性问题。它表明，一个大家庭的这些逻辑-包括所产生的标准MV和产品代数-产生一个不可判定的后果关系。随后，传递模态Lukasiewicz逻辑的行为进行了比较，它的非传递对应，展示了一些细节有关的可计算性和等价与其他逻辑。最后，我们展示了不可判定性的有效性和局部SAT问题的传递模型时，Delta操作添加到逻辑。
2019-04-02 cs.LO
On Nested Sequents for Constructive Modal Logics
我们提出了各种模态逻辑的演绎系统，这些模态逻辑可以通过添加公理d，t，b，4和5的组合从正常模态逻辑CK的构造性变体中获得。这包括标准模态逻辑K4、S4和S5的构造变体。我们使用我们的演示形式主义的嵌套序列，并给出一个句法证明削减消除。
2015-09-02 cs.LO
Model Checking and Validity in Propositional and Modal Inclusion Logics
命题包含逻辑和模态包含逻辑是属于基于团队语义的逻辑家族的形式主义。本文研究了这些逻辑的模型检验和有效性问题。我们确定这两个问题的复杂性界限，包括宽松和严格的团队语义。通过这样做，我们接近完成该计划，其最终目的是分类的中心推理问题的复杂性模态和命题依赖，独立性和包含逻辑。
2017-04-24 cs.LO
On the Relational Translation Method for Propositional Modal Logics
模态逻辑中定理证明的一种方法是将它们转换为谓词演算，然后使用传统的归结式定理证明器。这种方法在实践中被认为是不合适的，因为得到的公式太长，而且不可能证明模态公式的非定理性。在本文中，我们证明了（关系）翻译方法的实际可行性。使用最先进的一阶谓词逻辑定理证明器，我们证明了模态逻辑文献中的许多基准定理。我们证明了命题模态和时态逻辑公式的无效性，使用模型生成器或可满足性测试的经典逻辑。许多可满足的公式被发现具有非常小的模型。最后，几种不同的方法进行了比较。
2021-12-29 cs.LO
Credulous Acceptability, Poison Games and Modal Logic
毒药游戏是一个双人游戏，在一个图上玩，其中一个玩家可以影响另一个玩家能够穿越的边。它在论证框架中实现了可信容许集的存在性概念，或者用图论术语来说，实现了非平凡半核的存在性。我们开发了一个模态逻辑（毒药模态逻辑，PML）量身定制，以代表在这样的游戏中获胜的位置，从而确定精确的模态推理的基础上的概念，轻信的可接受性在论证。我们研究模型理论和可判定性属性的PML，并将其定位于最近研究的逻辑在十字路口的模态逻辑，论证和图形游戏。
2019-02-19 cs.LO
Bisimulation in Inquisitive Modal Logic
查询模态逻辑InqML是标准Kripke风格模态逻辑的推广。在它的认知化身中，它扩展了标准的认知逻辑，不仅可以捕获代理人拥有的信息，还可以捕获他们感兴趣的问题。从技术上讲，InqML属于基于团队语义的逻辑家族。从模型论的角度来看，它使我们在一元二阶逻辑的方向上迈出了一步，因为好奇的模态算子涉及世界集合上的量化。我们介绍和调查的互模拟等价的设置InqML的自然概念。我们比较了InqML和一阶逻辑的表达能力，并将InqML和一阶逻辑的互模拟不变片段作为一阶逻辑在各种两类关系结构上的互模拟不变片段。这些结果至关重要的是需要非经典的方法在研究互模拟和一阶的表现力在非小学类。
2017-07-27 cs.LO
Complexity of Łukasiewicz Modal Probabilistic Logics
Aix Marseille Univ, CNRS, LIS（艾克斯-马赛大学，法国国家科学研究中心，信息系统实验室）；The Czech Academy of Sciences, Institute of Computer Science（捷克科学院，计算机研究所）
本文研究了扩展的Łukasiewicz模概率逻辑的复杂性，证明了局部后果问题的两个变种具有PSPACE完全性。
2025-11-27 cs.LO
Non-iterative Modal Logics are Coalgebraic
模态逻辑是\emph{non-iterative}，如果它可以由不嵌套模态运算符的公理定义，并且\emph{rank-1}，如果公理中的所有命题变量都在模态运算符的范围内。众所周知，每一个语法定义的秩-1模态逻辑可以配备一个规范的共代数语义，确保可靠性和强完备性。在目前的工作中，我们将这一结果扩展到非迭代模态逻辑，表明每一个非迭代模态逻辑可以配备一个规范的coalgebraic语义定义的copointed函子，再次确保健全性和强完备性，通过一个规范的模型建设。在秩1的情况下，典型的余代数语义等价于具有适当框架条件的邻域语义，因此邻域语义上的非迭代模态逻辑的强完备性是已知的。作为这些结果的一个例子，我们讨论道义逻辑与事实分离，这是捕获的公理是非迭代的，但不是秩~1。
2020-08-02 cs.LO
The Size of Interpolants in Modal Logics
University of Amsterdam（阿姆斯特丹大学）；University of Liverpool（利物浦大学）
研究模态逻辑中Craig插值项、统一插值项和最强蕴含项的规模，发现表型模态逻辑中最强蕴含项可多项式时间转化为经典命题逻辑的统一插值项计算，但非表型逻辑中Craig插值项和最强蕴含项有指数级下界。
2026-05-14 cs.LO
A many-sorted polyadic modal logic
本文提出了一种多分类多元模态逻辑，推广了一些现有的方法。代数语义使我们得到了一个带有算子的布尔代数的多分类推广，为此我们证明了类似于Jónsson-Tarski定理。虽然从单排序逻辑到多排序逻辑的过渡是一个平稳的过程，但我们认为我们的系统是深化模态逻辑和程序验证之间联系的一个步骤，因为我们的系统可以被视为匹配逻辑的命题片段，一阶逻辑用于指定和推理程序。
2018-11-30 cs.LO
Characterizing Crisp Simulations and Crisp Directed Simulations between Fuzzy Labeled Transition Systems by Using Fuzzy Modal Logics
我们制定和证明清晰的模拟和清晰的模糊标记的过渡系统之间的模拟模糊模态逻辑，使用一般的t-范数为基础的语义的逻辑特征。所考虑的逻辑片段的模糊命题动态逻辑与Baaz投影算子。的逻辑刻画关注保存的积极存在（分别为正）模式下的清晰模拟（分别为清晰定向模拟），以及Hennessy-Milner属性的模拟公式。
2021-09-06 cs.LO
Losing Connection:the Modal Logic of Definable Link Deletion
在这篇文章中，我们从一个两人游戏开始，该游戏模拟了日常生活中不利环境下的通信，并从图的模态逻辑的角度研究它，其中可以根据对抗玩家可用的定义在本地删除链接。我们首先介绍一种新的语言，语义，和一些典型的有效性。然后，我们制定了一种新的类型的一阶翻译的模态逻辑，并证明其正确性。然后，提出了一个新的互模拟的概念，导致一个特征定理的逻辑作为一个片段的一阶逻辑，并进一步调查其表达能力对混合模态语言。接下来，我们讨论如何公理化这个逻辑的链接删除，使用动态认知逻辑作为对比。最后，我们证明了新的模态逻辑既缺乏树模型性质，又缺乏有限模型性质，并且它的可满足性问题是不可判定的。
2019-03-05 cs.LO
Complexity of Polyadic Boolean Modal Logics: Model Checking and Satisfiability
研究了可达性关系上的多元模态逻辑的模型检验的计算复杂性和可满足性问题。首先，我们证明了所得到的逻辑的模型检验问题的组合复杂性是PTime完全的。其次，我们证明了可及性关系上的否定扩展的多元模态逻辑的可满足性问题是ExpTime-完全的。最后，我们证明了可达性关系上的置换和布尔运算符的多元模态逻辑的可满足性问题是ExpTime-完全的，在必要的假设下，可以使用的可达性关系的数量是有界的常数。
2022-10-03 cs.LO
Library-Grade Modal Logic
University of Southern Denmark（南丹麦大学）；University of Amsterdam（阿姆斯特丹大学）
本文在Lean中构建库级模态逻辑形式化，通过垂直与水平复用提供通用框架，派生多种逻辑并减少67%代码，应用于数学、编程语言和并发推理。
2026-10-06 cs.LO
Many-Valued Coalgebraic Modal Logic: One-step Completeness and Finite Model Property
本文利用谓词提升方法研究了多值形式的余代数模态逻辑。余代数，被理解为一般的转移系统，可以作为各种模态逻辑的语义结构。在余代数模态逻辑中，一个著名的结果是它的完备性可以在一步水平上确定。利用正则模型的构造方法，我们将结果推广到多值情形。我们证明了基于三种不同多值代数结构的余代数模态逻辑的结果，这三种多值代数结构包括：有限值Rukasiewicz代数，用正则常数和Baaz Delta展开的交换积分Full-Lambek代数（FL $_{ew}$ -代数），以及用赋值运算展开的FL $_{ew}$ -代数.此外，我们还利用过滤技巧证明了多值余代数模态逻辑的有限模型性质。
2022-06-15 cs.LO
Reasoning in Non-normal Modal Description Logics
非正规模态逻辑，解释的邻域模型，概括了通常的关系语义，已发现应用在几个领域，如认识论，道义，和联盟推理。在这里，我们提出了初步的结果推理的模态描述逻辑的一个家庭，通过结合ALC与非正规模态算子。首先，我们提供了一个框架的终止，正确的，和完整的Tableau算法来检查满足性的公式在这样的逻辑与语义的基础上变化的域。然后，我们调查的可满足性问题，这些语言的片段，通过限制应用程序的模态算子的公式，并解释模型与常数域，提供紧密的复杂性结果。
2022-06-30 cs.LO
The Finite Model Property of Quasi-transitive Modal Logic
建立了准传递模态逻辑$\mathsf{K}_2^3=\mathsf{K}\oplus \Box\Box p\rightarrow \Box\Box\Box p$的有限模型性质。这种模态逻辑被保守地扩展到时态逻辑$\mathsf{Kt}_2^3$。本文提出了一个求解$\mathsf{Kt}_2^3$的Gentzen微积分$\mathsf{G}$。该演算$\mathsf{G}$通过有限的句法结构而具有有限代数性质。因此，$\mathsf{Kt}_2^3$和$\mathsf{K}_2^3$具有有限模型性质。
2019-02-22 cs.LO
The Completeness Problem for Modal Logic
我们介绍了模态逻辑的完备性问题，并研究其复杂性。对于公式的完备性定义，给定模态逻辑的一个公式，完备性问题询问该公式对于该逻辑是否完备。我们发现，完整性和有效性具有相同的复杂性-除了某些例外，一般来说，没有完整的公式。为了证明上界，我们提出了一个非确定性的多项式时间的过程与预言PSPACE相结合的表格和互模拟测试，并确定公式是否是完整的。
2017-09-19 cs.LO
A Modal Characterization Theorem for a Probabilistic Fuzzy Description Logic
模糊模态'可能'是解释概率类型空间通过采取预期的真值。概率模糊描述逻辑在概率双相似下是不变的，在信息量上是非扩展的。行为距离的概念。在本文中，我们提供了一个表征的表达能力，这种逻辑的基础上观察：我们证明了一个概率模拟的经典范Bentham定理，它指出，模态逻辑正是一阶逻辑的bisimulation-invariant片段。具体地说，我们证明了概率模糊一阶逻辑中的每一个公式都是非扩张的。行为距离可以通过概率模糊描述逻辑中的有界秩的概念来近似。关于同一结果的模态逻辑透视图，请参见arXiv：1810.04722。
2019-06-04 cs.LO
A Real-Valued Modal Logic
本文提出一种实值多值模态逻辑，结合Kripke语义与实数上的格群运算，通过带标签tableau系统获得coNEXPTIME上界，并建立模态-乘法片段的消割sequent演算及扩展阿贝尔逻辑的完备性。
2018-01-22 cs.LO
Generic Modal Cut Elimination Applied to Conditional Logics
我们开发了一个通用的标准，削减消除命题模态逻辑，这取决于吸收削减，收缩，削弱和反演的纯模态部分的规则系统。我们的标准也适用于正常模态逻辑领域之外的各种逻辑。我们给我们的框架，以各种条件逻辑广泛的例子实例。对于这些，我们得到完全内化的结石，这是大大简单的比那些已知的文献中，随着精简证明削减消除和复杂性。在一种情况下，条件逻辑与肯定前件和条件排中律，削减消除和复杂性明确表示为开放的文献。
2011-03-17 cs.LO
Modal Independence Logic
本文介绍了模态独立逻辑MIL，模态逻辑，可以显式地谈论命题变量之间的独立性。MIL的公式不是在世界中评估的，而是在世界的集合中评估的，所谓的团队。在这种情况下，MIL可以被看作是Väänänen的模态依赖逻辑MDL的变体。我们发现，MIL嵌入MDL，是严格更具表现力。然而，在单例团队中，MIL并不比通常的模态逻辑更具表达力，但MIL是指数更简洁。利用一种新的互模拟形式，我们将这些表达性结果扩展到由各种广义依赖原子扩展的模态逻辑。我们通过给出MIL中用餐密码协议的匿名性要求的规范来证明MIL的表达能力。我们还研究了MIL的复杂性问题，并表明，虽然它更具表达性，但它的可满足性和模型检验问题具有与MDL相同的复杂性。
2014-04-01 cs.LO
Coalgebraic Reasoning with Global Assumptions in Arithmetic Modal Logics
我们建立了一个通用的上限ExpTime的推理与全球的假设（也称为TBoxes）在共代数模态逻辑。与以前的结果不同，这种情况下，我们的界限不需要一个易于处理的一组Tableau规则的实例逻辑，使结果适用于更广泛的类的逻辑。例子是Presburger模态逻辑，它扩展了等级模态逻辑与后继数的线性不等式，以及概率模态逻辑与概率的多项式不等式。我们使用类型消除算法建立理论上界。我们还提供了一个全局缓存算法，潜在地避免了建立整个指数大小的候选状态空间，从而为实际推理提供了基础。该算法仍然涉及频繁的不动点计算，我们展示了如何有效地处理这些问题，在一个具体的算法建模刘和Smolka的线性时间不动点算法。最后，我们证明了上复杂度界是保持下添加名的逻辑，即在共代数混合逻辑。
2021-11-27 cs.LO
The Relative Succinctness and Expressiveness of Modal Logics Can Be Arbitrarily Complex
我们研究了模态逻辑的相对简洁性和表达性，并证明了这些关系可以像任何可数偏序一样复杂。为此，我们使用两个统一的形式主义来定义模态算子，并在这两个设置的简洁性和表现力的结果。我们的证明是基于公式大小的游戏介绍阿德勒和Immerman和互模拟。
2014-10-22 cs.LO
Preservation Theorems for Unravelling-Invariant Classes: A Uniform Approach for Modal Logics and Graph Neural Networks
Queen Mary University of London（伦敦大学玛丽女王学院）；University of Oxford（牛津大学）
本文研究了模态逻辑和图神经网络在解除不变类下的保护定理，揭示了GNN的表达能力与逻辑系统的对应关系。
2026-02-02 cs.LO
Non-Expansive Fuzzy Coalgebraic Logic
Friedrich-Alexander-Universität Erlangen-Nürnberg（埃尔朗根-纽伦堡大学）
本文提出非扩展共代数模糊模态逻辑，提供PSpace中可判定的标准，并为多种定量模态逻辑提供新的PSpace上界。
2026-02-12 cs.LO
Separating the Expressive Power of Propositional Dynamic and Modal Fixpoint Logics
我们调查的表达能力的两种主要类型的程序逻辑复杂的，非常规的程序属性在文献中发现：那些扩展命题动态逻辑（PDL），和那些扩展模态μ演算。这是受到最近发现的一种可判定程序逻辑的启发，这种逻辑被称为具有Chop的可见下推定点逻辑，它将模态μ演算和PDL扩展到可见下推语言上，到目前为止，这构成了可判定程序逻辑的两个支柱。在这里，我们表明这个逻辑不仅比它的两个片段中的任何一个更具表达力，而且事实上比它们的结合更具表达力。因此，程序逻辑之间的可判定性边界已经被适当地推高。我们完成了图片提供的结果分离所有的PDL为基础的和模态不动点逻辑与定期，明显下推和任意上下文无关的建设。
2021-08-24 cs.LO
