Satisfiability vs. Finite Satisfiability in Elementary Modal Logics
我们研究基本模态逻辑，即模态逻辑考虑一阶可定义类的框架。模态逻辑的经典语义允许无限结构，但实际应用往往要求我们将注意力限制在有限结构上。初等模态逻辑的许多可判定性和不可判定性结果分别在一般可满足性和有限可满足性下得到了证明[11，12，16，17]。在本文中，我们表明，有一个原因，我们必须分别处理这两种可满足性-我们证明，有一个通用的一阶公式，定义了一个基本模态逻辑与可判定的（整体）可满足性问题，但不可判定的有限可满足性问题，反之亦然，存在一个普适公式，它定义了一个具有可判定的有限可满足性问题但具有不可判定的一般可满足性问题的初等模态逻辑。
2012-10-09 cs.CC cs.LO
On the Complexity of Elementary Modal Logics
模态逻辑在计算机科学中有着广泛的应用。自20世纪70年代以来，模态可满足性问题的复杂性一直在研究，通常是在逐个案例的基础上证明结果。我们证明了一个非常普遍的分类广泛的一类相关的逻辑：模态逻辑的许多重要的子类可以通过限制允许的模型与一阶霍恩公式。我们证明了这些逻辑的可满足性问题是NP完全的或PSPACE困难的，并展示了一个简单的分类标准。此外，我们证明了许多PSPACE硬逻辑匹配的PSPACE上界。
2008-02-13 cs.CC cs.LO
Symmetries in Modal Logics
FaMAF Universidad Nacional de Córdoba（科尔多瓦国立大学FaMAF）；CONICET（国家科学技术研究委员会）
我们将合取范式中命题公式的对称性概念推广到模态公式。我们的框架使用共归纳模型，因此，结果适用于广泛的一类模态逻辑，包括，例如，混合逻辑。我们的主要结果表明，模态公式的对称性保持蕴涵。
2013-03-29 cs.AI cs.LO
Solving Quantified Modal Logic Problems by Translation to Classical Logics
本文评估了自动定理证明系统在QMLTP库中的表现，通过将问题翻译为类型一阶和高阶逻辑并使用一阶或高阶逻辑ATP系统求解，发现嵌入方法在使用先进系统时可靠，且在反驳猜想时优于原生模态逻辑系统。
2024-04-29 cs.AI cs.LO
PSPACE Bounds for Rank-1 Modal Logics
由于缺乏适用于各种逻辑的通用算法方法，为给定的模态逻辑建立复杂性界限通常是一项艰巨的任务。目前的工作是一个一般理论的复杂性模态逻辑的一步。我们的主要结果是，所有秩1逻辑享有浅模型属性，因此，在温和的假设下，其axiomatisation格式，在PSPACE。这导致了一个统一的推导紧PSPACE边界的一些逻辑，包括K，KD，联盟逻辑，分级模态逻辑，多数逻辑和概率模态逻辑。此外，我们的通用算法发现，见证愉快的证明理论的性质，包括一个弱子公式属性的Tableau证明。这种普遍性是由一个coalgebraic语义，方便地抽象的细节，一个给定的模型类，从而允许覆盖范围广泛的逻辑在一个统一的方式。
2007-06-27 cs.CC cs.LO
PVS Embeddings of Propositional and Quantified Modal Logic
SRI International（斯坦福国际研究院）
模态逻辑允许推理各种模式的真理：例如，它意味着什么的东西可能是真的，或者知道的东西是真的，而不是仅仅相信it.This报告描述了嵌入的命题和量化模态逻辑的PVS验证系统。PVS的资源允许以一种有吸引力的方式来完成这一点，该方式支持模态逻辑的大部分标准语法，同时提供有效的自动化。该报告介绍并正式指定和验证了模态逻辑中的几个标准主题，例如标准模态公理和可达性关系的属性之间的关系，以及Barcan公式的属性及其在常数和变化域中的逆。
2022-05-12 cs.AI cs.LO
Minimal modal logics, constructive modal logics and their relations
提出一族对应经典模态逻辑的极小模态逻辑，通过两种独立但等价的方法定义，并揭示其与构造性模态逻辑CK的紧密关系，进而衍生出一族构造性模态逻辑。
2023-09-05 cs.LO
On Modal Logics for Qualitative Possibility in a Fuzzy Setting
Spanish Council for Scientific Research (CSIC)（西班牙国家研究委员会）
在不确定性建模的可能性方法中，本文提出了一种模态逻辑系统来推理模糊命题的可能性（和必要性）的定性（比较）陈述。我们把这种定性模态逻辑与著名的知识和信念模态逻辑S5和KD 45的多值类似物MVS5和MVKD 45分别联系起来。完整性结果得到这样的逻辑，因此，他们扩展了以前现有的结果定性可能性逻辑在经典的非模糊设置。
2013-02-27 cs.AI cs.LO
Complexity of validity for propositional dependence logics
研究了命题依赖逻辑、模态依赖逻辑和扩展模态依赖逻辑的有效性问题。我们证明了命题依赖逻辑的有效性问题是NEXPTIME-完全的。此外，我们建立了相应的问题的模态依赖逻辑和扩展的模态依赖逻辑是NEXPTIME困难的，在NEXPTIME^NP。
2014-08-26 cs.CC 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
Undecidability of the unification and admissibility problems for modal and description logics
我们表明，统一问题`是否有一个替代实例的一个给定的公式，是证明在一个给定的逻辑？对于用泛模态扩充的基本模态逻辑K和K_4，因此，推理规则的容许性问题对于这些逻辑也是不可判定的。这些是标准可判定模态逻辑的第一个例子，其中统一和容许问题是不可判定的。我们还证明了不可判定性的统一和容许问题的K和K4至少有两个模态算子和名（而不是通用模态），从而表明这些问题是不可判定的基本混合逻辑。最近，统一已被引入作为一个重要的推理服务的描述逻辑。带名项的K的不可判定性证明可以用来证明带名项的布尔描述逻辑（如ALCO和SHIQO）的统一的不可判定性。对于具有泛模态的K的不可判定性证明可以用来表明，对于具有传递角色、反向角色和角色层次（如SHI和SHIQ）的布尔描述逻辑，与角色盒相关的统一问题是不可判定的。
2006-09-11 cs.AI cs.LO
Weakly Aggregative Modal Logic: Characterization and Interpolation (new version)
Peking University（北京大学）；UC Berkeley（加州大学伯克利分校）
弱聚合模态逻辑（WAML）是一组伪装的多元模态逻辑，它们的参数都是相同的。WAML在认知逻辑和博弈逻辑中有着有趣的应用，因此本文研究了WAML的一些基本模型理论问题。具体地说，我们基于互模拟的直观概念给出了WAML的vanBenthem-Rosen特征定理，并证明了每个基本WAML系统K_n都缺少Craig插值。
2019-05-30 cs.AI cs.LO math.LO
Propositional modal logic with implicit modal quantification
命题项模态逻辑在具有无限多的可达性关系的Kripke结构上解释，因此语法允许变量索引模态和量化。这种逻辑是不可判定的，我们考虑一个变量自由命题的双模态逻辑与隐量化。因此，$[\forall] α$断言所有可及性关系上的必然性，而$[\exists] α$是某些可及性关系上的经典必然性。该逻辑是与一个自然的互模拟模型的关系，我们表明，该逻辑正是一个两个排序的一阶逻辑的互模拟不变片段。该逻辑很容易被看作是可判定的，并且承认有效公式的完全公理化。此外，决策过程自然地延伸到“捆绑片段”的完整术语模态逻辑。
2018-12-29 cs.LO
Modal Logics for Topological Spaces
在这篇论文中，我们将提出两个逻辑系统，MP和MP，用于推理知识和努力。这些逻辑系统将在空间背景下进行解释，因此，知识和努力的抽象概念将由具体的数学概念来定义。
2000-07-26 cs.AI cs.LO
Systematic Verification of the Modal Logic Cube in Isabelle/HOL
Freie Universität Berlin（柏林自由大学）；Cambridge University（剑桥大学）
我们提出了一个著名的模态逻辑立方体在Isabelle/HOL的自动验证，在其中我们证明了立方体的逻辑之间的包含关系，使用自动推理工具。先前的工作解决了这个问题，但不限于模态逻辑立方体，并使用一阶逻辑中的编码与一阶自动定理证明器相结合。相比之下，我们的解决方案更优雅，透明和有效。它采用了嵌入的量化模态逻辑在经典的高阶逻辑。自动推理工具，如大锤与LEO-II，Satallax和CVC 4，Metis和Nitpick，实现完全自动化。虽然成功，实验也激励一些技术改进的Isabelle/HOL工具。
2015-07-31 cs.AI cs.LO
From Hybrid Modal Logic to Matching Logic and Back
建立在我们以前的工作混合多元模态逻辑，我们确定模态逻辑等价匹配逻辑，程序规范和验证的逻辑。这提供了一种严格的方法来在两种方法之间传输结果，这对两个系统都有好处。
2019-09-04 cs.LO
Non-normal modalities in variants of Linear Logic
ISTC-CNR（意大利国家研究委员会认知科学与技术研究所）；Université Paris-Est（巴黎东部大学）
本文介绍了资源意识逻辑的模态版本。我们专注于扩展的变种线性逻辑与一个最小的非正常模态。在早期的工作中，我们研究了多智能体系统中的代理，我们已经证明了结果可以扩展到具有多个非最小模态的逻辑。在这里，我们从没有加性析取的命题直觉线性逻辑的语言开始，我们添加了一个模态。我们提供了一个解释这种语言的一类Kripke资源模型扩展的邻域函数：模态Kripke资源模型。我们提出了一个希尔伯特式的公理化和根森式的微积分。我们证明理论是健全的和完整的一类模态Kripke资源模型。我们表明，微积分承认削减消除和证明搜索是在PSPACE。然后，我们将展示如何扩展的结果时，非交换连接词添加到语言。最后，我们通过将其实例化为代理逻辑来使用逻辑框架。特别是，我们提出了一个逻辑的原因资源敏感的使用文物，并说明它与各种例子。
2015-09-04 cs.AI cs.LO
Modal definability in Euclidean modal logics
本文研究欧几里得模态逻辑框架类中模态可定义性问题的可计算性，刻画了哪些欧几里得模态逻辑会导致该问题不可判定。
2025-08-14 cs.LO math.LO
"Knowing value" logic as a normal modal logic
Peking University（北京大学）
近年来，人们对“知道是否”、“知道什么”、“知道如何”等非标准认知逻辑的兴趣越来越大。这些逻辑通常是非正规的，即，模态逻辑的标准公理和推理规则可能是无效的。本文证明了Wang和Fan \cite{WF13}提出的条件“知值”逻辑可以被看作是一种伪装的正常模态逻辑，方法是把Kv算子的否定看作一种特殊的菱形。在这种观点下，原来的一阶Kripke语义可以通过在标准Kripke模型中引入三元关系$R_i^c$来大大简化，该三元关系将一个世界与两个$i$可访问的世界相关联，这两个世界在常量$c$的值上不一致。在直觉约束下，基于这种Kripke模型的模态逻辑正是Wang和Fan（2013，2014）所研究的模态逻辑。此外，有一个非常自然的二进制推广的“知道值”钻石，这令人惊讶的是，并没有增加逻辑的表达能力。由此得到的二进制菱形逻辑具有透明的正规模态系统，这加深了我们对“知值”逻辑的理解，并简化了一些以前难以解决的问题。
2016-11-21 cs.AI cs.LO
Undecidability and non-axiomatizability of modal many-valued logics
在这项工作中，我们研究了一类全球模态逻辑所产生的Kripke框架评估某些剩余格，在文献中称为模态多值逻辑的可判定性。我们展示了一个大的家庭，这些模态逻辑是不可判定的，与经典的模态逻辑和命题逻辑定义在同一类代数。这个家族包括了在标准Lukasiewicz代数和乘积代数上计算的Kripke框架所产生的全局模态逻辑。我们改进了前面的结果，证明了全局模态Lukasiewicz和乘积逻辑甚至不能递归可公理化。我们的结论是否定地解决了开放的问题，即每个全局模态逻辑是否与它的局部模态逻辑在无限制必然规则下是封闭的。
2022-04-15 cs.LO math.LO
Intuitionistic modal logics: a minimal setting
本文提出一种严格包含于IK的直觉主义模态逻辑，作为最小正规直觉主义模态逻辑的候选，并探讨其设定。
2025-02-26 cs.LO math.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
The Expressive Power of Modal Dependence Logic
我们研究了各种模态逻辑与团队语义的表达能力。我们表明，正是向下封闭和封闭下的团队k-互模拟的团队的属性，对于一些有限的k，是可定义的模态逻辑扩展与直觉析取。此外，我们还证明了直觉析取模态逻辑和扩展模态依赖逻辑的表达能力是一致的。最后，我们建立任何翻译从扩展模态依赖逻辑到模态逻辑与直觉析取增加一些公式的大小呈指数级。
2014-06-24 cs.LO math.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
Transfinite Modal Logic: a Semi-quantitative Explanation for Bayesian Reasoning
Japan Advanced Institute of Science and Technology（日本北陆先端科学技术大学院大学）
贝叶斯推理在人类理性和机器学习中起着重要的作用。本文介绍了超限模态逻辑，它将模态逻辑与序数运算相结合，半定量地形式化贝叶斯推理。在技术上，我们首先研究了序数算术的一些非平凡性质，然后使我们能够自然和优雅地扩展正常模态逻辑的语义到新的超限模态逻辑上，同时仍然保持Kripke模型的普通定义完全不变。尽管所有的超限数学定义，我们认为，在实践中，这种逻辑实际上可以适应一个完全有限的解释。我们认为，超限模态逻辑以一种相当简单明了的形式抓住了贝叶斯推理的本质，特别是它为福尔摩斯的名言“当你排除了不可能，剩下的无论多么不可能，都一定是真理”提供了一个完美的解释。“我们还证明了我们的逻辑的有限模型性质定理的对应。
2022-04-02 cs.AI cs.LO math.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
Goldblatt-Thomason Theorems for Modal Intuitionistic Logics
证明了双代数直觉主义逻辑的Goldblatt-Schlason定理，并将其实例化为文献中各种模态直觉主义逻辑的Goldblatt-Schlason定理.
2022-06-01 cs.LO math.LO
Description logics as polyadic modal logics
我们研究标准描述逻辑到多元模态逻辑框架的扩展。我们通过一般关系代数，可以用来定义操作的关系，所有的arities促进一个自然的方法，这样的逻辑。作为一个具体的系统来说明我们的方法，我们调查的多元版本的ALC扩展与关系置换运算符和元组计数。本文的重点是概念性的，而不是技术性的。
2021-08-19 cs.LO
Deterministic modal Bayesian Logic: derive the Bayesian inference within the modal logic T
本文定义并研究了条件逻辑。这种条件逻辑DmBL被构造为贝叶斯条件的确定性对应物。逻辑是不受限制的，因此允许任何逻辑运算。逻辑独立性的概念也在逻辑本身中定义。这种逻辑被证明是非平凡的，并没有减少到经典命题。建立了逻辑模型。证明了结果的完备性。它表明，任何无条件概率可以扩展到整个逻辑DmBL。然后从概率DmBL中恢复贝叶斯条件。最后，说明了DmBL为什么符合Lewis的平凡性.
2007-01-28 cs.LO math.LO math.PR
Modality for Free: Notes on Adding the Tarskian Möglichkeit to Substructural Logics
我们简要地研究了模态公式，可以得出乘法加法线性逻辑（MALL）和一些扩展，通过使用Tarksi的扩展模态算子。我们还将它与模态逻辑K的一个子结构形式作了简单的比较。
2011-05-08 cs.LO math.LO
First-Order Modal Logic via Logical Categories
本文将逻辑范畴框架扩展至一阶模态逻辑，证明Joyal风格表示定理并引入模态预拓扑os概念，最后展示如何从一阶模态理论构建语法范畴。
2025-04-03 cs.LO math.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
Quantum modal logic
Oita College National Institute of Technology（大分科学技术大学）
本文形式化了最简形式的基于量子逻辑的模态逻辑，给出其关系语义与矢列演算并证明二者间的可靠性和完全性定理，为构建量子逻辑上的各类模态逻辑提供基础框架。
2025-11-13 cs.LO math.LO
A van Benthem Theorem for Fuzzy Modal Logic
我们提出了一个模糊（或定量）版本的范本特姆定理，其特点是命题模态逻辑作为一阶逻辑的互模拟不变片段。具体来说，我们考虑一阶模糊谓词逻辑及其模态片段，并表明，模糊一阶公式是非扩张的w.r.t.互模拟距离的自然概念正好是那些可以通过模糊模态公式来近似的概念。
2018-02-05 cs.LO
Topological Modal Logics with Difference Modality
我们考虑带有两个模态算子$\Box$和$\D$的命题模态逻辑。在拓扑语义中，$\Box$被解释为内部算子，而$\D$被解释为差。我们表明，一些重要的拓扑性质是在这种语言中表达。此外，我们提出了一些逻辑和证明f.m.p.和完备性定理。
2010-11-25 cs.LO math.LO
A van Benthem Theorem for Quantitative Probabilistic Modal Logic
在概率转换系统中，行为度量提供了比双相似性概念更细粒度和更稳定的系统等价性度量。它们与定量概率逻辑密切相关，事实上，在实数单位区间取值的概率模态逻辑引起的距离与行为距离一致。对于概率系统，概率模态逻辑扮演着类似于Hennessy-Milner逻辑在经典标记转移系统上的角色。在定量背景下，模态逻辑在双相似性下的不变性成为公式求值的非扩展性。行为距离在本文中，我们提供了一个表征的表达能力的概率模态逻辑的基础上，这一观察：我们证明了一个概率模拟的经典范Bentham定理，它指出，模态逻辑正是一阶逻辑的互模拟不变的片段。具体来说，我们表明，定量概率模态逻辑在于密集的双模拟不变片段，在非扩展公式评估的指示意义上，定量概率一阶逻辑;更确切地说，双模拟不变的一阶公式是近似的模态公式的有界秩。有关同一结果的描述逻辑透视图，请参见arXiv：1906.00784。
2019-06-04 cs.LO
Justification Logic for Intuitionistic Modal Logic (Extended Technical Report)
本文为Fischer Servi的直觉主义模态逻辑IK及其扩展提供证明逻辑对应物，通过扩展证明项语法、公理化和无切嵌套序列系统实现语法实现。
2025-07-12 cs.LO math.LO
The expressive power of modal logic with inclusion atoms
模态包含逻辑是基本模态逻辑的包含原子扩展，其语义定义在Kripke模型上。Kripke模型的团队只是其域的一个子集。本文给出了模态包含逻辑表达能力的一个完整刻画：一类带队的Kripke模型在模态包含逻辑中是可定义的当且仅当它在k-互模拟下是闭的，对于某个整数k，它在并下是闭的，并且它具有空队性质.我们还证明了同样的表达能力，可以通过添加一个单一的一元非空算子模态逻辑。此外，我们建立了一个指数下界的大小从模态包含逻辑到模态逻辑与非空算子的翻译。
2015-09-24 cs.LO math.LO
Complexity through Translations for Modal Logic with Recursion
本文研究了经典模态逻辑的复杂性及其扩展与不动点算子，使用翻译转移结果跨越逻辑。特别是，我们通过翻译和从μ演算和模态逻辑，这使我们能够转移已知的上限和下限的多智能体逻辑的复杂性结果。我们还使用这些翻译介绍一个终止表系统的逻辑，我们研究的基础上，Kozen的表的μ演算，和一个拟合和Massacci模态逻辑。
2022-09-21 cs.LO
Sahlqvist Correspondence Theory for Sabotage Modal Logic
破坏模态逻辑是一种动态逻辑。它扩展了静态模态逻辑，增加了一个动态模态，该模态被解释为“在框架中删除一个箭头后，公式为真”。本文旨在解决一个公开问题，即给出破坏模态逻辑的Sahlqvist型对应定理。本文定义了破坏Sahlqvist公式，并给出了计算破坏Sahlqvist公式的一阶对应项的算法。最后，我们给出了一些评论和未来的发展方向。
2021-07-02 cs.LO math.LO
On Modal Logics of Partial Recursive Functions
经典的命题逻辑被认为是健全的和完整的集合语义解释连接词作为集合操作。在上述解释下，本文通过一种新的二元模态扩展了命题语言，该二元模态对应于部分递归函数类型构造器。确定性和非确定性的功能的情况下被认为是语义上完整的模态逻辑描述和这些逻辑的可判定性建立。
2004-07-12 cs.LO
