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
Unifying Hidden-Variable Problems from Quantum Mechanics by Logics of Dependence and Independence
我们研究隐藏变量模型从量子力学，和他们的抽象在纯粹的概率和关系的框架，通过依赖和独立的逻辑，基于团队语义。我们发现，隐藏变量模型的共同理想的属性可以定义在一个优雅和简洁的方式在依赖和独立逻辑。不同性质之间的关系，以及它们的同时可实现性，因此可以在纯逻辑层面上被公式化和证明，作为逻辑公式的蕴涵和可满足性问题。在依赖和独立逻辑中，概率和关系蕴涵之间的联系使我们能够简化证明。在许多情况下，我们可以通过一个证明建立概率和关系隐变量模型的结果，因为一种情况意味着另一种情况，这取决于纯粹的语法标准。我们还讨论了贝尔和Kochen-Specker的不去定理，并提供了后者的一个纯粹的逻辑变体，引入非上下文选择作为一个团队语义属性。
2022-01-27 cs.LO math.LO
Independence and concurrent separation logic
一个组合的Petri网为基础的语义给出了一个简单的语言，允许指针操作和并行。然后，该模型被应用到给出一个概念的有效性并发分离逻辑，强调在这样的可靠性保证推理的过程-环境的二重性所作出的判断。合理性的并发分离逻辑的规则相对于这个定义的有效性。保留的Petri网模型的独立性信息，然后利用来表征的逻辑执行的并行进程的独立性。这表明允许能够改变原子动作的粒度的细化操作。
2008-03-19 cs.LO cs.PL
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
On Dependence Logic
我们给出了一个概述的依赖和独立逻辑的一些发展。这是一个小的选择，为新人，从一个快速增长的文学主题。进一步讨论了条件独立原子，证明了条件独立逻辑与非条件独立逻辑是等价的。最后，我们简要地讨论了我们的逻辑信念表示的应用。
2013-05-25 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
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
Equivalence and Conditional Independence in Atomic Sheaf Logic
University of Ljubljana（卢布尔雅那大学）；Institute of Mathematics, Physics and Mechanics（数学、物理与力学研究所）
本文提出了一种逻辑语义基础，用于在具有变量等价、变量粗等价和变量条件独立性的设置中进行推理。通过原子sheaf拓扑研究了等价与条件独立性的逻辑，并展示了其在经典逻辑中的应用。
2026-05-15 cs.LO math.CT math.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
Logics of Dependence and Independence: The Local Variants
现代的依赖和独立逻辑是基于团队语义的，这意味着公式的计算不是基于变量的单个赋值，而是基于一组这样的赋值，称为团队。这导致了存在二阶逻辑水平上的高表达能力。作为替代，Baltag和van Benthem提出了依赖逻辑的局部变体，称为函数依赖逻辑（logic of functional dependence，LFD）。虽然它的语义也是基于团队的，但公式只在其中一个分配上进行本地评估，并且团队只是作为评估过程中考虑的可能分配的供应。因此，这种逻辑依赖于广义赋值语义的模态视角，并且可以被看作是一阶逻辑的一个片段。对于不含等式的LFD变体，可满足性问题是可判定的。我们扩展了本地化逻辑的依赖和独立的想法，在一个系统的方式，考虑到本地变量的标准原子依赖属性：除了依赖和独立，还包括，排除和匿名。我们研究模型理论和算法问题的本地化逻辑，并解决了一些问题，已离开开放的巴尔塔格和范Benthem。特别地，我们研究了局部逻辑的可判定性问题，证明了等式可满足的LFD是不可判定的。此外，我们通过适当的互模拟的概念建立特征定理，并研究这些逻辑的模型检验问题的复杂性。
2021-02-20 cs.LO math.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
Dependence and Independence
我们引入一个原子公式直观地说，给定的变量是独立于给定的其他变量，如果第三组变量保持不变。我们将其与依赖逻辑进行对比。我们表明，我们的独立原子产生了一个自然的逻辑能够形式化的基本直觉的独立性和依赖性。
2012-08-27 cs.LO math.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
A Probabilistic Separation Logic
概率独立性是一个有用的概念，用于描述随机抽样的结果-所有概率语言中的基本操作-和用于推理随机变量组。然而，现有的验证方法处理独立性很差，如果有的话。我们提出了一个概率分离逻辑PSL，其中分离模型概率独立性。本文首先给出了一个新的聚束蕴涵逻辑（BI）的概率模型。然后，我们建立了一个程序逻辑的基础上，这些断言，并证明系统的可靠性。我们证明了我们的逻辑验证信息理论的安全性的密码结构的几个众所周知的任务，包括私人信息检索，不经意的传输，安全多方除了，和简单的不经意的RAM。我们的证明纯粹是根据高级属性进行推理的，比如独立性和一致性。
2020-07-17 cs.LO cs.PL
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
A Credal Extension of Independent Choice Logic
我们提出了一个扩展普尔的独立选择逻辑的基础上放松的基本独立性假设。采用了一种涉及可能世界上多个联合概率质量函数的信任语义。这是一种保守的概率逻辑编程方法，通过考虑与概率事实一致的所有质量函数来实现。这允许对一些概率选择之间的独立性不能被假设的任务进行建模，并且不能评估特定的依赖模型。初步测试的对象排名应用程序表明，尽管松散的基本假设，信息推理可以提取。
2018-06-21 cs.LO
Losing Connection:the Modal Logic of Definable Link Deletion
在这篇文章中，我们从一个两人游戏开始，该游戏模拟了日常生活中不利环境下的通信，并从图的模态逻辑的角度研究它，其中可以根据对抗玩家可用的定义在本地删除链接。我们首先介绍一种新的语言，语义，和一些典型的有效性。然后，我们制定了一种新的类型的一阶翻译的模态逻辑，并证明其正确性。然后，提出了一个新的互模拟的概念，导致一个特征定理的逻辑作为一个片段的一阶逻辑，并进一步调查其表达能力对混合模态语言。接下来，我们讨论如何公理化这个逻辑的链接删除，使用动态认知逻辑作为对比。最后，我们证明了新的模态逻辑既缺乏树模型性质，又缺乏有限模型性质，并且它的可满足性问题是不可判定的。
2019-03-05 cs.LO
On existential declarations of independence in IF Logic
我们分析了IF句中的量词前缀中存在量词之间的独立性声明行为，给出了一个句法判据，用以判定是否存在以该前缀开头的句子，使得其真假值的独立性声明的去除可能会影响该句子的真值。我们的结果还扩展到平衡语义值为未定的IF句子。主要定理使我们能够描述各种特定类别的量词前缀的行为，并证明作为一个显着的推论，所有存在的IF句子是等价于一阶句子。作为进一步的结果，我们证明了与知识记忆的IF句子片段只有一阶的表达能力（真理等价）。
2012-05-11 cs.LO math.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
