Bisimulation Invariant Monadic-Second Order Logic in the Finite
我们考虑在各类有限变迁系统上的互模拟不变一元二阶逻辑。我们提出了几个组合特征时，这个片段的表达能力与模态μ演算相一致。使用这些特征，我们证明了一些简单的过渡系统，这确实是这样的。特别地，我们证明了在Cantor-Bendixson秩不超过k的有限转移系统类上，互模拟不变的MSO与L_mu一致.
2019-05-16 cs.LO
Proof Search Specifications of Bisimulation and Modal Logics for the pi-Calculus
我们指定的操作语义和互模拟关系的有限π演算内的逻辑，其中包含的nabla量词编码通用的判断和定义编码不动点。由于我们只限于有限的情况，逻辑展开不动点的能力使得这个逻辑对于操作语义的归纳性质和互模拟的共归纳性质都是完备的。nabla量词有助于解决π演算表达式中变量范围及其执行（证明）的微妙问题。我们说明了这种逻辑所允许的逻辑规范的几个优点：它们是自然的和说明性的;它们不包含关于变量名的副条件，同时保持对这些变量的完全形式化处理;后期互模拟关系和开放互模拟关系之间的差异来自于熟悉的逻辑区别;三个量词之间的相互作用（对于所有，存在，（nabla）它们的作用域可以解释早期互模拟和晚期互模拟之间的差异以及基于约束输入和输出行为的各种模态算子之间的差异;并且涉及推理规则、统一和回溯的应用的证明搜索可以为模态逻辑中的一步转换、互模拟和满足提供完整的证明系统。我们还说明了如何可以编码的π演算与复制，在一个扩展的逻辑与归纳和共归纳。
2009-02-16 cs.LO
Bisimulation and p-morphism for branching-time logics with indistinguishability relations
在Zanardo，1998年中，分支时间逻辑的皮尔斯语义丰富了经过t的历史之间在时刻t的不可区分性的概念。具有不可分割性关系的树为具有时态和模态运算符的时态语言提供了语义。本文给出了这种语言和语义的p-态射和互模拟的概念，并证明了一些保持性结果。
2013-05-02 cs.LO
Bisimulation-Based Comparisons for Interpretations in Description Logics
我们研究比较描述逻辑的解释方面的“逻辑后果”的形式半积极的概念（如半积极的概念断言）。这种比较的特点是由类似的互模拟的条件。在所考虑的逻辑中最简单的是PDL（命题动态逻辑）的变体。其他的扩展，逻辑与逆角色，名词，量化的数量限制，通用的角色，和/或概念构造器表示的局部自反性的角色。所研究的问题是：关于比较的半正概念的保持，用于比较的Hennessy-Milner性质，以及保持半正概念的解释的最小化。
2013-04-20 cs.LO
Monadic Second-Order Logic and Bisimulation Invariance for Coalgebras
推广标准的一元二阶逻辑的Kripke模型，我们介绍了一元二阶逻辑解释的余代数的任意集函子。一元二阶逻辑树相似的知名结果，我们提供了一个翻译的这种逻辑到一类自动机，相对于类的coalgebras承认一个树状支持Kripke框架。然后，我们考虑公式的行为等价下的不变性，更特别地，我们调查是否coalgebraic μ演算是一元二阶逻辑的bisimulation不变片段。最近的结果的第三作者的基础上，我们表明，为了提供这样一个共代数推广的Janin-Walukiewicz定理，它足以找到我们所谓的一个适当的一致建设的函子。作为这个结果的应用，我们得到了Janin-Walukiewicz定理的部分新证明，以及袋函子（分次模态逻辑）和所有指数多项式函子的互模拟不变性结果。最后，我们考虑了单调邻域函子的一些细节，它为单调模态逻辑提供了共代数语义。事实证明，这个函子没有足够的统一构造，因此互模拟不变性的自动机理论方法不能直接应用。如果我们考虑邻域模型之间的全局互模拟，这个问题可以克服：我们的主要技术结果之一提供了一个表征的单调模态μ演算扩展与全球模态，作为片段的一元二阶逻辑的单调邻域函子是不变的全局互模拟。
2015-01-28 cs.LO
Knowledge, Awareness, and Bisimulation
我们比较不同的认识概念中存在的意识命题变量：逻辑的隐性知识（其中明确的知识是可定义的），明确的知识，和投机性的知识。互模拟的不同概念适用于这些逻辑。我们提供这些逻辑的图像有限模型之间的相互模拟和模态等价的对应关系。推理知识的逻辑与显性知识的逻辑具有同样的表达能力，而隐性知识的逻辑比这两者更具表达能力。我们还提供了公理化的三个逻辑-只有一个投机知识是新颖的。然后，我们通过回忆包含意识的动作模型来研究动态。我们表明，任何可以想象的知识或意识的变化，可以在这种情况下建模，我们给了一个完整的公理化的动态逻辑的隐性知识。令人惊讶的是，所有三种逻辑的动态版本都具有同样的表达能力。
2013-10-23 cs.LO
Graded modal logic and counting bisimulation
本文将互模拟不变片段的刻画定理推广到分级多模态逻辑，证明其在所有及有限点态 Kripke 结构上恰好对应计数互模拟等价下保持的一阶性质。
2023-07-18 cs.LO math.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
Relational Dualities and Bisimulation
University of Bristol（布里斯托大学）
本文探讨了关系对偶性与双射之间的对应关系，通过构建特定的关系扩展，将良好的系统间关系（如双射）与谓词间的关系联系起来。
2026-05-07 cs.LO
Logic-Induced Bisimulations
对于由逻辑连接给出的共代数模态逻辑，我们定义了一个新的逻辑诱导的互模拟概念（称为$ρ$ -互模拟），并研究了它的性质。我们表明，它是结构的意义上说，它是只在定义方面的余代数结构和一步模态语义，而且，可以通过一种形式的关系提升的特点。此外，我们比较$ρ$ -互模拟几个著名的等价概念，我们证明了两个模型之间的互模拟的集合往往形成一个完整的晶格。主要的技术结果是一个Hennessy-Milner型定理，它指出，在某些条件下，逻辑等价意味着$ρ$ -双相似性。特别地，后者不依赖于函子\emph{not}（余代数的类型）和$\mathsf{L}$（给出逻辑）之间的对偶性，也不依赖于逻辑连接$ρ$的属性。
2020-08-21 cs.LO math.LO
Bisimulations and Modal Logics for Higher Dimensional Automata
Norwegian University of Science and Technology（挪威科技大学）；University of Edinburgh（爱丁堡大学）；University of New South Wales（新南威尔士大学）；University of Warsaw（华沙大学）
该研究针对高维自动机，提出介于ST与hhp互模拟间的新中间等价关系，构建了刻画hhp互模拟的模态逻辑，其片段可刻画ST互模拟及中间概念。
2026-08-17 cs.LO
Simulations and Bisimulations For Coalgebraic Modal Logics
我们定义了一个概念的Lambda模拟的共代数模态逻辑，参数的选择Lambda的谓词提升函子T。我们证明了这个概念在几个方面是足够的：i）它保留了正公式的真值，ii）对于Lambda，单调谓词提升的分离集，Lambda-互模拟的相关概念对应于T-行为等价（此外Lambda-n-互模拟对应于T-n-行为等价），以及iii）事实上，对于Lambda-分离和T保持弱回调，双功能Lambda-互模拟是T-互模拟。从本质上讲，我们得到了一个模块化的等价概念，当与一组单独的单调谓词提升一起使用时，与T-行为等价一致，而不管T是否保留弱回调（与T-双相似性的概念不同）。
2013-04-11 cs.LO math.LO
Bisimulations and Logics for Higher-Dimensional Automata
Norwegian University of Science and Technology（挪威科技大学）；University of Warsaw（华沙大学）；EPITA Research Lab（EPITA研究实验室）
本文提出Ipomset模态逻辑，用于刻画HDAs中的路径双向模拟，并定义单元双向模拟及其与标准双向模拟的关系。
2024-11-11 cs.FL cs.LO
Intuitionistic K is a Bisimulation-Invariant Fragment of Intuitionistic First-Order Logic
University of Bern（伯尔尼大学）；Universidade Federal de Santa Catarina（圣卡塔琳娜联邦大学）
定义直觉主义模态逻辑IK的关系语义上的IK-双模拟，证明IK是直觉主义一阶逻辑的IK-双模拟不变片段，并给出内在刻画及Hennessy-Milner型定理，发展直觉主义一阶模型论。
2026-07-01 cs.LO math.LO
Bisimulations Meet PCTL Equivalences for Probabilistic Automata
概率自动机已成功地应用于并发和随机系统的形式化验证。有效的模型检验算法已经被研究，其中最常用的用于表达属性的逻辑是基于概率计算树逻辑（PCTL）及其扩展PCTL^*。提出了各种行为等价物，作为一个强大的工具，抽象和组合最小化的PA。不幸的是，这些等价是众所周知的合理的，但就PCTL或PCTL* 所诱导的逻辑等价而言并不完整。塞加拉在1995年指出了一个既健全又完整的行为等价的愿望，但多年来一直没有定论。在本文中，我们引入了新的概念，强互模拟关系，PCTL和PCTL* 的特点。我们扩展了弱互模拟的特点PCTL和PCTL* 没有下一个运营商，分别。此外，我们还扩展了模拟前序的框架。因此，我们的论文弥合了在这种情况下逻辑和行为等价性和前序之间的差距。
2013-06-21 cs.LO
Bisimulations for intuitionistic temporal logics
我们介绍了互模拟的逻辑$ITL^e$与“下一个”，“直到”和“释放”，一个直观的时态逻辑的基础上配备了一个偏序用于解释直观的含义和一个单调函数用于解释的时间模态的结构。我们的主要结果是，“最终”，这是可定义的“until”，不能定义的“下一个”和“henceforth”，同样的，“henceforth”，可定义的“释放”，不能定义的“下一个”和“until”，即使在较小的类这里和那里的模型。
2018-03-14 cs.LO math.LO
Uniform Interpolation for Propositional and Modal Team Logics
在本文中，我们考虑模态组逻辑，经典模态逻辑的推广，它是可能的数据之间的依赖现象描述。我们证明，最有名的片段全模态团队逻辑允许消除所谓的“存在互模拟量词”，其中存在的某个集合是模互模拟。因此，我们证明了这些片段享有一致插值性质。
2018-10-12 cs.LO
A meta-modal logic for bisimulations
Universidad de Málaga（马拉加大学）；Universidad de Sevilla（塞维利亚大学）
本文提出一种元模态逻辑用于研究仿射关系，通过扩展基本模态语言引入新模态，建立仿射关系的定义，并证明其逻辑的可判定性和PSPACE完全性。
2026-10-27 cs.LO math.LO
A van Benthem Theorem for Fuzzy Modal Logic
我们提出了一个模糊（或定量）版本的范本特姆定理，其特点是命题模态逻辑作为一阶逻辑的互模拟不变片段。具体来说，我们考虑一阶模糊谓词逻辑及其模态片段，并表明，模糊一阶公式是非扩张的w.r.t.互模拟距离的自然概念正好是那些可以通过模糊模态公式来近似的概念。
2018-02-05 cs.LO
Finite Model Property and Bisimulation for LFD
最近，Baltag和van Benthem引入了一种可判定的函数依赖逻辑（LFD），它用原子局部依赖语句扩展了柱面相对化集合代数（CRS）的逻辑。它的语义可以用广义赋值模型或它们的模态对应物给出，因此该逻辑既是一阶逻辑又是模态逻辑。利用Herwig关于扩展部分同构的定理证明了LFD具有有限模型性质（FMP），并证明了LFD作为一阶逻辑片段的互模拟不变性定理。
2021-09-17 cs.LO cs.MA
The Glory of the Past and Geometrical Concurrency
本文有助于对并发的几何模型的一般理解，被命名为高维自动机（HDAs）的普拉特。特别是，我们调查模态逻辑等模型和它们的表达能力方面的互模拟，可以被捕获。并发的几何模型之所以有趣，主要有两个原因：它的通用性和可表达性，以及捕获自动并发和动作细化的自然方式。然而，这种模型的逻辑没有得到很好的研究，其中一个简单的，但足够的，模态逻辑在HDAs只是最近才被引入。由于这种模态逻辑，有两个存在模态，期间和之后，只捕获分裂互模拟，这是相当低的范Glabbeek和Vaandrager的频谱，直接的问题是什么小的扩展，这个逻辑可以捕获更细粒度的遗传历史保持互模拟（hh）？作为回应，本文中的工作提供了几个见解。一个是HDA的几何方面使得可以用于捕获hh互模拟，这是一种不使用事件变量的标准模态逻辑，与我们比较的两种逻辑（在表达性较低的模型上）相反。我们在这里研究的逻辑使用标准的过去模态，并扩展了以前引入的逻辑（称为HDML），只有向前的，动作标记的模态。此外，我们试图通过引入一个相关的模型，我们称之为ST-配置结构，它扩展了van Glabbeek和Plotkin的配置结构，以更好地理解上述问题。我们将这个模型与HDAs联系起来，并根据这个新模型重新定义和证明了以前的结果。这些提供了一个不同的观点，为什么过去的模态和几何并发捕获遗传历史保持互模拟。还获得了其他相关的见解。
2012-06-14 cs.LO
Capturing Bisimulation-Invariant Exponential-Time Complexity Classes
奥托定理将图上的互模拟不变PTIME查询描述为可以在多元μ演算中制定的那些查询，它依赖于Immerman-Vardi定理，Immerman-Vardi定理通过具有最少不动点的一阶逻辑来描述PTIME（有序结构）。这种连接已经通过在谓词上使用函数的polyadic μ演算的扩展到了具有最小不动点的双模拟不变EXPTIME，利用Immerman的二阶逻辑对EXPTIME的表征。在本文中，我们表明，在指数时间层次中的所有类的互模拟不变的版本有逻辑对应的出现作为扩展的polyadic μ演算的高阶函数。这利用了高阶逻辑（k+1阶）对k-EXPTIME的特征化，具有最少的不动点，这是由Freire和Martins提出的。
2022-09-21 cs.CC cs.LO
A van Benthem Theorem for Quantitative Probabilistic Modal Logic
在概率转换系统中，行为度量提供了比双相似性概念更细粒度和更稳定的系统等价性度量。它们与定量概率逻辑密切相关，事实上，在实数单位区间取值的概率模态逻辑引起的距离与行为距离一致。对于概率系统，概率模态逻辑扮演着类似于Hennessy-Milner逻辑在经典标记转移系统上的角色。在定量背景下，模态逻辑在双相似性下的不变性成为公式求值的非扩展性。行为距离在本文中，我们提供了一个表征的表达能力的概率模态逻辑的基础上，这一观察：我们证明了一个概率模拟的经典范Bentham定理，它指出，模态逻辑正是一阶逻辑的互模拟不变的片段。具体来说，我们表明，定量概率模态逻辑在于密集的双模拟不变片段，在非扩展公式评估的指示意义上，定量概率一阶逻辑;更确切地说，双模拟不变的一阶公式是近似的模态公式的有界秩。有关同一结果的描述逻辑透视图，请参见arXiv：1906.00784。
2019-06-04 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
First-Order Modal $ξ$-Calculus: On the Aspects of Application and Bisimulation
本文提出了一阶模态$ξ$ -演算以及系谱Kripke模型。受模态$μ$ -演算的启发，一阶模态$ξ$ -演算采取了非常相似的形式，并将其归纳表达扩展到不同的维度。我们阐述了几个生动的例子，证明了这种逻辑的深刻的效用，特别是描绘家谱的并发计算机进程。互模拟概念的逻辑也得到了彻底的检查。
2023-01-17 cs.LO math.LO
Bisimulation and expressivity for conditional belief, degrees of belief, and safe belief
LORIA, CNRS / Université de Lorraine（洛里亚研究所、法国国家科学研究中心 / 洛林大学）；DTU Compute, Technical University of Denmark（丹麦技术大学计算学院）
可信性模型是Kripke模型，代理人使用它来推理他们自己和彼此的知识和信念。这些模型被用来解释条件信念、信念度和安全信念的概念。条件信念逻辑既包含该模态，也包含知识模态，信念度逻辑和安全信念逻辑也是如此。关于这些逻辑，可扩展性模型可能包含太多信息。需要一个适当的互模拟概念来表征它们。我们定义了互模拟的概念，并证明了所需的特征：类的图像有限和原像有限的模型（相对于可扩展性关系），两个指向Kripke模型是模态等价的三个逻辑中的任何一个，当且仅当它们是双相似的。结果，这种模型的信息内容可以类似地用条件信念逻辑、信念程度逻辑或安全信念逻辑来表示。我们发现了一个惊人的结果。然而，这并不意味着逻辑具有同样的表达性：条件和信念度的逻辑是不可比较的，信念度的逻辑和安全信念的逻辑是不可比较的，而安全信念的逻辑比条件信念的逻辑更具表达性。鉴于互模拟表征的结果，这是一个同样令人惊讶的结果。我们希望我们的见解可能有助于不断增长的社区正式认识论和定性和定量建模之间的关系。
2016-02-25 cs.AI cs.LO
Computation Tree Logic with Deadlock Detection
研究了在没有下一状态模态的计算树逻辑（CTL-X）中满足相同公式的标号迁移系统的状态等价关系。这个关系是由De Nicola & Vaandrager通过将标记转移系统转化为Kripke结构而得到的，同时解除了对后者的总体性限制。他们将其描述为发散敏感分支互模拟等价。我们发现，这种等价未能成为一个交错并行组合的同余。原因是，CTL-X的非总Kripke结构的拟议应用缺乏表现力，以应付死锁属性是重要的，在并行组合的上下文中。我们提出了一个扩展的CTL-X，或替代治疗的非整体，填补这一空白。等价诱导我们的扩展的特点是分支互模拟等价与明确的分歧，这是，此外，示出的粗同余包含在分歧敏感的分支互模拟等价。
2009-12-22 cs.LO
Finite Model Property and Bisimulation for LFD
最近，Baltag和van Benthem arXiv：2103.14946 [cs.LO]引入了一种新的具有局部依赖公式和依赖量词的函数依赖（LFD）可判定逻辑。该语言在依赖模型上进行解释，依赖模型是具有一组可用变量分配的一阶结构对，也称为团队。与依赖模型相关的团队可以被看作是一个标记的转换系统，在这个系统上LFD成为模态逻辑，其中依赖量词成为模态，局部依赖公式被视为特殊原子。在本文中，我们引入适当的互模拟的概念，将LFD（和一些相关的逻辑）表征为一阶逻辑（FOL）的一个片段，并表明它等价于arXiv：2102.10368 [cs.LO]中提出的更标准的互模拟概念，但对于互相似性检查更有效。我们的主要结果是LFD具有有限模型性质（FMP），通过Herwig定理的一个新的应用扩展部分同构。
2021-07-13 cs.LO math.LO
Neighborhood Contingency Logic: A New Perspective
在本文中，我们提出了一个新的邻域语义的权变逻辑，通过引入一个简单的性质，在标准的邻域模型。这简化了（Fan and van Ditmarsch，2015）中给出的邻域语义，但不会改变有效公式的集合。在此基础上，在互模拟的各种概念和Hennessy-Milner定理中，我们证明了$c$ -互模拟等价于文献中的nbh- $Δ$ -互模拟，从而引导我们理解后者概念的本质。这个视角也提供了各种框架可定义性和公理化结果。
2018-02-07 cs.LO math.LO
A Van Benthem Theorem for Modal Team Semantics
著名的van Bentham定理指出模态逻辑恰好对应于在互模拟下不变的一阶逻辑的片段。在这篇文章中，我们证明了一个精确的模拟这个定理的框架中的模态依赖逻辑MDL和团队语义。我们表明，模态团队逻辑MTL，扩展MDL的经典否定，捕捉到的正是FO-可定义的互模拟不变性质的Kripke结构和团队。我们还比较了MTL的表达能力，最近在该地区研究的MDL的大多数变体和扩展。
2015-07-13 cs.LO
Inquisitive bisimulation
本文引入并研究探究性模态逻辑InqML中的互模拟等价，将其刻画为双类型结构上一阶逻辑的互模拟不变片段，并比较其与一阶逻辑的表达能力。
2020-10-29 cs.LO math.LO
Positive Hennessy-Milner Logic for Branching Bisimulation
本文引入了 Hennessy-Milner 定理的有向版本，通过提出仅有限使用否定的正模态逻辑（PHMLU）和有向分支互模拟，证明了状态理论包含与有向互模拟的等价性，并揭示 HMLU 可由 PHMLU 的布尔组合表示。
2025-10-27 cs.FL cs.LO
Neighbourhood semantics for graded modal logic
引入了一类将Kripke框架嵌入邻域框架的分次模态逻辑的邻域框架。这类邻域框架是一阶可定义的，但不是模态可定义的。通过修正单调互模拟的定义，得到了Kripke框架上的分次互模拟的一个新定义。
2021-05-19 cs.LO math.LO
Reasoning About Bounds in Weighted Transition Systems
本文提出一种推理加权转移系统中转移权重界限的方法，引入更粗的互模拟概念，并设计定制模态逻辑，证明其不变性、有限模型性质、完备公理化及可判定性。
2018-11-23 cs.FL cs.LO
Some Remarks on the Model Theory of Epistemic Plausibility Models
经典的知识和信念逻辑通常是在克里普克模型上解释的，对于克里普克模型，数学上发展良好的模型理论是可用的。然而，这种模型不足以捕捉动态现象。因此，引入了认知可解释性模型。因为这些模型的结构比Kripke模型丰富得多，所以它们并不直接继承模态逻辑的模型理论结果。因此，虽然认知可解释性结构非常适合建模的目的，广泛的调查，他们的模型理论一直缺乏到目前为止。本文的目的正是填补这一空白，通过启动一个系统的探索模型理论的认知可解释性模型。与“普通”模态逻辑一样，重点将放在互模拟的概念上。我们定义了各种概念的互模拟（参数化的语言L），并表明L-双相似意味着L-等价。我们证明了一个Hennesy-Milner型结果和两个不可定义性结果。然而，我们的主要观点是一个负面的，即互模拟不能简单地推广到认知可验证性模型，如果考虑到条件信念。我们提出了两种方法来处理这个问题：（i）增加一个模态的语言，和（ii）把额外的限制模型。最后，我们对互模拟和动态模型变化之间的相互作用做了一些评论。
2010-03-14 cs.LO
Modal Logics for Nominal Transition Systems
本文为名义转换系统定义了通用模型及Hennessy-Milner逻辑，证明其充分且表达完备，并系统处理多种互模拟变体，已在Nominal Isabelle中形式化。
2021-01-27 cs.LO
Generating Witness of Non-Bisimilarity for the pi-Calculus
在逻辑编程范式中，很难开发出一个优雅的解决方案来生成证明两个π演算过程之间的开放双相似性失败的区分公式;这是出乎意料的，因为π演算和开放互模拟的语义已经在高阶逻辑编程系统中被优雅地指定。我们使用Haskell的解决方案将公式生成定义为从所有不确定互模拟步骤的森林到一对区分公式的树变换。由于Haskell中的惰性，只生成树转换函数所需的必要路径。我们的工作表明，Haskell和它的库提供了一个有吸引力的平台，象征性地分析等价性标记的过渡系统在环境敏感的设置。
2017-05-31 cs.LO
Monadic second order logic as the model companion of temporal logic
本文的主要重点是互模拟不变的MSO，更具体地说，在模型论中，一个理论的模型伴侣是一类模型的一阶描述，其中所有潜在的可解方程组和非方程组有解决方案。我们发现，双模拟不变的MSO树模型伴侣的一个新的时态逻辑，“公平CTL”，丰富的CTL与当地的公平性约束。为了实现这一点，我们给出了一个完整的证明，逻辑公平CTL相结合的tableaux和石头对偶，和一个公平的CTL编码的自动机的模态μ演算。此外，我们还证明了二叉树上的MSO是二元确定性公平CTL的模型伴侣。
2016-05-03 cs.LO math.LO
Epistemic Logic with Partial Dependency Operator
本文将$\textit{partial}$依赖模态$\mathcal{D}$引入认知逻辑，以推理Kripke模型中的$\textit{partial}$依赖关系。由此产生的依赖认知逻辑具有良好的表现力和美丽的性质。提供了几个有趣的例子，突出了这种逻辑的实际用途。然后讨论了该逻辑的互模拟性，并给出了该逻辑的一个子语言的可靠的强完备公理化。
2019-08-27 cs.LO math.LO
A Modal Characterization Theorem for a Probabilistic Fuzzy Description Logic
模糊模态'可能'是解释概率类型空间通过采取预期的真值。概率模糊描述逻辑在概率双相似下是不变的，在信息量上是非扩展的。行为距离的概念。在本文中，我们提供了一个表征的表达能力，这种逻辑的基础上观察：我们证明了一个概率模拟的经典范Bentham定理，它指出，模态逻辑正是一阶逻辑的bisimulation-invariant片段。具体地说，我们证明了概率模糊一阶逻辑中的每一个公式都是非扩张的。行为距离可以通过概率模糊描述逻辑中的有界秩的概念来近似。关于同一结果的模态逻辑透视图，请参见arXiv：1810.04722。
2019-06-04 cs.LO
On the expressive power of inquisitive epistemic logic
该研究利用InqML框架的互模拟等价概念，将探究性认知逻辑（InqML）的表达能力刻画为一阶逻辑在双排序一阶结构上的互模拟不变片段，需用非经典模型论方法分析其非初等性质。
2025-02-12 cs.LO math.LO
Model Comparison Games for Horn Description Logics
Horn描述逻辑是标准描述逻辑的语法定义的片段，其属于一阶逻辑的Horn片段，并且对于其本体中介的查询应答由于数据复杂度而处于PTime中。它们在模态逻辑中被独立地引入，以捕捉Horn一阶逻辑与模态逻辑的交集。在本文中，我们介绍了基本的Horn描述逻辑hornALC（对应于基本的Horn模态逻辑）的模型比较游戏，并使用它们来获得一个Escherichfeucht-Fraïssé型可定义性结果和van Bentham风格的表达完整性结果的HornALC。我们还建立了后者的有限模型理论版本。Escherichfeucht-Fraïssé类型可定义性结果用于表明，检查模型的hornALC不可定义性是ExpTime-complete的，这与ALC不可定义性形成鲜明对比（即，互模拟等价）在PTime中可检查。此外，我们探讨了更多的表现性描述和模态逻辑的霍恩片段的行为，通过定义一阶逻辑的霍恩守护片段，并引入模型比较游戏。
2019-04-15 cs.LO
Description Logic TBoxes: Model-theoretic Characterizations and Rewritability
我们描述的描述逻辑（DL）TBox的表达能力，无论是表达DL，如ALC和ALCQIO和轻量级DL，如DL-Lite和EL。我们的刻画是相对于一阶逻辑，基于广泛的语义概念，如互模拟，等模拟，不相交的工会，和直接产品。我们首先研究了以下一类新的决策问题：给定一个在DL L中表示的TBox T，决定T是否可以等价地重写为L的片段L'中的TBox。
2011-04-15 cs.LO math.LO
On Free Description Logics with Definite Descriptions
明确描述是“该$x$使得$φ$”形式的短语，用于指代上下文中的单个实体。它们通常比单独的名称对用户更有意义，特别是在通过本体建模或查询数据时。我们研究自由描述逻辑与个人的名字和明确的描述作为语言的条款，同时也占他们可能缺乏外延。我们专注于扩展的$\mathcal{ALC}$和，分别，$\mathcal{EL}$与名词，普遍的作用，和明确的描述。我们表明，在这些扩展中的标准推理并不比原来的语言更难，我们使用一个合适的互模拟概念来描述相对于一阶公式的概念的表达能力。此外，我们奠定了基础，通过研究的复杂性，决定存在的明确的描述下的本体论的个人自动支持确定的描述生成。最后，我们提供了一个多项式时间减少的推理在其他自由描述逻辑语言的基础上的双域语义部分解释的情况下。
2021-06-29 cs.LO
A Characterization Theorem for a Modal Description Logic
模态描述逻辑的特点是模态，它捕获知识对诸如时间、地点或代理的信息状态等参数的依赖性。例如，在一个示例中，逻辑S5-ALC将标准描述逻辑ALC与可以被理解为认知算子或表示（无向）变化的S5模态相结合。该逻辑嵌入到相应的模态一阶逻辑S5-FOL中。我们证明了一个模态特征定理的嵌入，在类比的结果由范Bentham和罗森有关ALC标准的一阶逻辑：我们表明，S5-ALC只有局部角色是，无论是在有限的和无限制的模型，正是互模拟不变片段的S5-FOL，从而给出了一个精确的描述的表达能力的S5-ALC只有局部角色。
2017-05-23 cs.LO math.LO
On the Verification of Logically Decorated Graph Transformations
我们解决的问题，推理图转换功能的行动，如\emph{addition}和\emph{deletion}的节点和边缘，节点\emph{merging}和\emph{cloning}，节点或边缘\emph{labelling}和边缘\emph{redirection}。首先，我们介绍了所考虑的图重写系统参数化的一个给定的逻辑$\mathcal{L}$。利用$\mathcal{L}$的公式对图的节点和边进行标记。在第二步中，我们解决的问题，所考虑的重写系统的形式验证，通过使用霍尔最弱的前提演算。它作用于$\{\texttt{Pre}\}(\texttt{R},\texttt{strategy}) \{\texttt{Post}\}$形式的三元组，其中\texttt{Pre}和\texttt{Post}是在给定逻辑$\mathcal{L}$中指定的条件，\texttt{R}是图形重写系统，而\texttt{strategy}是说明如何执行\texttt{R}中的规则的表达式。我们证明我们介绍的微积分是健全的。此外，我们展示了如何建议的框架可以成功地实例化不同的逻辑。我们调查一阶逻辑和它的几个可判定的片段，特别侧重于不同方言的描述逻辑（DL）。我们还表明，通过使用互模拟关系，一些DL片段不能使用，由于他们缺乏表达能力。
2018-03-07 cs.LO
Model Theoretic Characterisations of Description Logics
本文研究了描述逻辑ALC、ALCI、ALCQ以及ALCO、ALCQO、ALCQIO、EL的模型论性质。TBox的ALC，ALCI和ALCQ的特点是作为片段的FO是不变的全球互模拟和不相交的工会。逻辑ALCO，ALCQO和ALCQIO，其中包括个人，其特征在于w.r.t.将个体解释为单例集的所有解释的类K。ALCO和ALCQO的TBox的特征都要求在某些情况下，在向前生成的子解释下保留一个FO-句子。等同于ALCQIO-TBoxes的FO-句子-由于ALCQIO的反向角色-具有类似的特征，但需要在生成的子解释下保留。作为子布尔DL的EL在概念层面上被表征为在模拟下被保存并且在直接产品下被保存的FO片段。同样有效的是通过在模拟下保留和具有最小模型来表征。对于EL-TBox，模拟的全局版本是不够的，但EL-TBox的FO-语句在全局等价模拟、不相交并和直积下是不变的。对于这些描述逻辑中的每一个，特征概念都被阐明，并且特征化伴随着一个调查，在这个调查下，饱和的概念下，手头的逻辑享有Hennessy-and-Milner性质。作为应用的结果，我们确定了最小的全球双相似同伴w.r.t. ALCQO互模拟，并介绍了TBox的L1到L2可重写性问题，其中L1和L2是（描述）逻辑。后者是决定L1-TBox是否可以等价地表示为L2-TBox的问题。给出了判定ALCI到ALC可重写性和ALC到EL可重写…
2013-05-24 cs.LO math.LO
Categorical Semantics for Model Comparison Games for Description Logics
一个分类的方法来研究模型比较游戏的comonads最近发起的Abramsky等人。在这项工作中，我们分析了游戏，自然出现在描述逻辑的背景下，并补充他们与合适的游戏comonads。更确切地说，我们认为表达的子逻辑ALCSelfIbO，即，逻辑扩展ALC与任何组合的逆，名，安全的布尔角色组合，和自我运营商。我们的结构扩充和修改了Abramsky和Shah的所谓模态comonad。我们采用的方法严重依赖于相对comonads的使用，我们利用它以组合的方式在互模拟游戏中封装额外的功能。
2022-11-11 cs.LO math.CT
Description Logics with Two Types of Definite Descriptions: Complexity, Expressiveness, and Automated Deduction
Queen Mary University of London（伦敦大学玛丽女王学院）
本文提出两种扩展描述逻辑ALC的确定描述变体，分析其复杂性、表达性及自动推理方法，展示ALCι_G在表达性上的优势及实现的有效性。
2025-12-07 cs.LO
A Rational Entailment for Expressive Description Logics via Description Logic Programs
ISTI - CNR（意大利国家研究委员会信息科学与技术研究所）；CAIR - University of Cape Town（开普敦大学CAIR）
Lehmann和Magidor的有理闭包被认为是非单调逻辑领域的一个里程碑，它也在描述逻辑（DL）的背景下被重新表述。我们在这里展示了如何建模的合理形式的蕴涵表达DL，如SROIQ，提供了一种新的推理过程，编译成一个描述逻辑程序（DL程序）的非单调DL知识库。
2021-06-28 cs.AI cs.LO
