Signature-Based Abduction for Expressive Description Logics -- Technical Report
Technische Universität Dresden（德累斯顿工业大学）；The University of Manchester（曼彻斯特大学）；Max Planck Institut für Informatik（马克斯·普朗克计算机科学研究所）
基于特征的溯因推理旨在对一组特定的名字（特征）建立假设，这些假设解释了与某些背景知识相关的观察。这种类型的外展对于诊断等任务很有用，其中用于观察症状的词汇与预期解释这些症状的词汇不同。我们提出了第一个完整的方法解决基于签名的溯因表达的描述逻辑ALC中表示的意见，其中可以包括TBox和ABox公理，从而解决知识库溯因问题。该方法是保证计算一个有限的和完整的假设集，并在一组现实的知识库进行评估。
2020-07-08 cs.AI cs.LO
Practical Reasoning for Very Expressive Description Logics
描述逻辑是一类知识表示形式化体系，其主要特征是构造器从原子概念和角色构造复杂的概念和角色。表达角色构造器在许多应用中很重要，但在计算上可能存在问题。我们提出了一个算法，决定可满足性的DL ALC扩展与传递和逆角色和功能限制方面的一般概念包含公理和角色层次结构，早期的实验表明，该算法是非常适合实施。此外，我们还证明了仅具有传递和逆角色的ALC扩展仍然是PSPACE中的。我们调查这个家庭的DL的可判定性的限制，表明放松限制放置在数量限制中使用的各种角色导致所有推理问题的不可判定性。最后，我们描述了一些优化技术，这是至关重要的，在获得实现的决策过程中，尽管最坏情况下的问题的复杂性，表现出良好的性能与现实生活中的问题。
2000-05-09 cs.AI cs.LO
Polynomial Rewritings from Expressive Description Logics with Closed Predicates to Variants of Datalog
TU Wien（维也纳技术大学）
在许多情况下，完整和不完整的信息并存。出于这个原因，知识表示和数据库社区长期以来一直对在推理逻辑理论时同时支持封闭世界和开放世界的观点感兴趣。在这里，我们考虑使用逻辑理论查询可能不完整的数据的设置，形式化的本体介导的查询（OMQ），对查询与理论，有时称为本体，表达背景知识的评价。这可以通过从理论中指定一组封闭谓词来进一步丰富，这些谓词将在封闭世界假设下解释，而其余的则用开放世界观点来解释。通过这种方式，我们可以利用数据的部分完整性来检索更精确的查询答案。本文的中心目标是理解OMQ语言的相对表达能力，其中本体是用表达性描述逻辑（DL）ALCHOI编写的，并且包括一组封闭谓词。我们考虑一类有限的合取查询。我们的主要结果是表明，这种非单调查询语言中的每一个查询都可以在多项式时间内被翻译成稳定模型语义下的带否定的数据库。为了克服挑战，数据库没有直接的手段来表达存在的量化ALCHOI，我们定义了一个两个玩家的游戏，其特征在于本体的满意度，并设计了一个数据库查询，可以决定存在的获胜策略的游戏。如果没有封闭的谓词，也就是在查询一个普通的ALCHOI知识库的情况下，我们的翻译产生一个多项式大小的正析取数据库程序。据我们所知，不像以前的翻译相关片段表达（非霍恩）DL，这些是第一个多项式时间翻译。
2019-12-16 cs.AI cs.LO
Data Complexity in Expressive Description Logics With Path Expressions
TU Dresden（德累斯顿工业大学）；University of Wrocław（弗罗茨瓦夫大学）
本文分析 ZOIQ 在拟森林上可满足性的数据复杂性，证明其 NP 完全，并据此重新刻画 OWL2 SR 族及 ZIQ 根查询蕴涵的复杂性界限。
2024-06-11 cs.AI cs.CC cs.LO
Bounded Fitting for Expressive Description Logics
Leipzig University and ScaDS.AI Center Dresden/Leipzig（莱比锡大学和ScaDS.AI中心德累斯顿/莱比锡）；TU Dortmund University（德累斯顿理工大学）；Center for Trustworthy Data Science and Security, University Alliance Ruhr（可信数据科学与安全中心，鲁尔大学联盟）
本文研究了在扩展ALC的表达式描述逻辑中，受限适配方法的理论性质和实现，通过SAT求解器实现，并与现有概念学习器比较，展示了其在复杂概念学习中的实用性。
2026-05-08 cs.AI
Extending SROIQ with Constraint Networks and Grounded Circumscription
Indian Institute of Technology, Mandi（曼迪印度理工学院）；SCHOOL OF COMPUTING AND ELECTRICAL ENGINEERING（计算与电气工程学院）
语义网技术的发展促进了不同领域知识的本体编码。然而，许多实际领域的建模需要比标准描述逻辑（最突出的SROIQ）支持更多的表现力。在本文中，我们扩展了表达的DL SROIQ与约束网络（导致在逻辑SROIQc）和接地限制（导致在逻辑GC-SROIQ）。约束建模的应用包括嵌入具有时间或空间信息的本体，而接地限制的应用包括可撤销推理和封闭世界推理。我们描述的语法和语义的逻辑形成，包括约束建模结构在SROIQ，并提供了一个健全的，完整的和终止tableau算法，我们进一步提供了一个直观的算法，在SROIQc的接地外切，它坚持接地外切的一般框架，并可以应用到整个范围的表达逻辑，目前还没有这样的具体算法存在。
2015-08-01 cs.AI cs.LO
A Decidable Very Expressive Description Logic for Databases (Extended Version)
KRDB Research Centre, Free University of Bozen-Bolzano（博岑-博尔扎诺自由大学 KRDB 研究中心）
我们介绍$\mathcal{DLR}^+$，扩展的n元命题封闭的描述逻辑$\mathcal{DLR}$处理属性标记的元组（概括的位置符号），关系的投影，以及全球和本地的关系对象化，能够表示包含，功能，关键，和外部的唯一性依赖。该逻辑配备了TBox和ABox公理。我们展示了如何一个简单的语法限制共享共同属性的投影在$\mathcal{DLR}^+$知识库的外观，使推理的语言决定与$\mathcal{DLR}$相同的计算复杂性。所得到的$\mathcal{DLR}^\pm$ n元描述逻辑能够更彻底地编码概念数据模型，如EER，UML和ORM。
2017-07-25 cs.AI
Disjunctive Logic Programs versus Normal Logic Programs
University of Western Sydney（西悉尼大学）
本文主要研究在有限、无限或任意结构上的稳定模型语义下，析取和常规逻辑程序的表达能力。本文提出了一种从析取逻辑程序到普通逻辑程序的转换，并证明了这种转换在无限结构上是合理的。证明了两类逻辑程序对任意结构的表达能力的等价性与对有限结构的表达能力的等价性是一致的，并且与NP在补下是否闭的等价性是一致的。在有限结构上，证明了在辅助谓词和辅助函数的性质有界的条件下，从析取逻辑程序到正常逻辑程序的不可译性。
2013-04-02 cs.AI
The Complexity of Reasoning with Cardinality Restrictions and Nominals in Expressive Description Logics
我们研究的复杂性相结合的描述逻辑ALCQ和ALCQI的术语形式主义的基础上基数限制的概念。这些组合可以自然地嵌入到C^2中，C^2是谓词逻辑的两个变量片段，具有计数量词，这在NExpTime中产生了可判定性。我们表明，这种方法导致ALCQI的最佳解决方案，因为具有基数限制的ALCQI具有与C^2（NExpTime-complete）相同的复杂性。相反，我们表明，对于ALCQ，问题可以在ExpTime中解决。这一结果是通过减少基数限制推理推理与（一般较弱）术语形式主义的一般公理ALCQ扩展与名词。使用相同的减少，我们表明，对于ALCQI与名义的扩展，推理与一般公理是一个NExpTime完全的问题。最后，我们锐化这一结果，并表明纯概念的ALCQI与名词可满足性是NExpTime-complete。如果没有名词，这个问题被认为是PSpace完全的。
2011-06-01 cs.AI
GC-SROIQ(C) : Expressive Constraint Modelling and Grounded Circumscription for SROIQ
语义网技术的发展促进了不同领域知识的本体编码。然而，许多实际领域的建模需要更多的表达比标准描述逻辑（DL）支持的表示方案。我们扩展了DL SROIQ与约束网络和接地限制。约束建模的应用包括嵌入具有时间或空间信息的本体，而接地限制允许可撤销推理和封闭世界推理。本文克服了现有的约束建模方法的限制，通过引入表达结构。接地限制允许概念和角色最小化，并可决定DL。我们提供了一个通用的和直观的算法的框架，可以适用于整个范围的逻辑接地限制。我们提出了由此产生的逻辑：GC-SROIQ（C），并描述了它的tableau决策过程。
2017-04-03 cs.AI
Finite Query Answering in Expressive Description Logics with Transitive Roles
University of Warsaw（华沙大学）；TU Wien（维也纳工业大学）
我们研究有限本体介导的查询回答（FOMQA）的问题，OMQA的变种，其中所代表的世界被假定为有限的，因此只考虑有限的本体模型。我们采用最典型的设置与工会的合取查询和本体表示的描述逻辑（DL）。FOMQA的研究与非可控环境相关。这不仅适用于没有有限模型属性的DL，而且适用于那些允许传递角色声明的DL。当传递角色被允许时，评估查询是具有挑战性的：FOMQA对于SHOIF是不可判定的，并且只知道对于ALCIF的Horn片段是可判定的。我们展示了FOMQA对SOIF的三个适当片段：SOI，SOF和SIF的可判定性。我们的方法是建立相关的模型来决定有限的查询蕴涵。依赖于这些模型的一定规律性，我们开发了基于自动机的决策程序与最佳复杂性的界限。
2018-08-09 cs.AI
On the Configuration of More and Less Expressive Logic Programs
University of Calabria（卡拉布里亚大学）；University of Genoa（热那亚大学）；University of Huddersfield（哈德斯菲尔德大学）
特定问题的表示之间的解耦，即，其知识模型和推理方面是基于模型的人工智能的主要优点之一。这允许例如通过在整个求解过程中具有优势来专注于改进推理方面。此外，众所周知，许多求解器甚至对输入中的语法变化都非常敏感。在本文中，我们专注于提高推理方面，利用这种敏感性。我们考虑两个著名的基于模型的人工智能方法，SAT和ASP，定义了一些语法功能，可能会干扰他们的输入，并使用自动配置工具来重新制定的输入公式或程序。广泛的实验分析，涉及SAT和ASP域，从各自的竞争，结果表明，可以通过使用输入重新制定和配置获得不同的优势。逻辑程序设计理论与实践（TPLP）
2022-03-02 cs.AI
Reasoning with Very Expressive Fuzzy Description Logics
National and Technical University of Athens（雅典国立技术大学）；The University of Aberdeen（阿伯丁大学）；The University of Manchester（曼彻斯特大学）
今天人们普遍认识到，对不精确性和精确性的管理将产生更智能和更现实的基于知识的应用程序。描述逻辑是一种知识表示语言，由于其可判定性和推理算法的高性能，在过去的十年中得到了广泛的关注。本文将著名的模糊ALCDL推广到模糊SHINDL，它将模糊ALCDL推广为传递性角色公理（S）、逆角色公理（I）、角色层次（H）和数量限制（N）。我们说明了为什么传递性的角色公理是难以处理的模糊解释的存在，以及如何正确地处理它们。然后，我们通过添加角色层次结构和数量限制来扩展这些结果。本文的主要贡献是模糊DL语言fuzzy-SI和fuzzy-SHIN的可判定性证明，以及fuzzy-SI和fuzzy-SHIN的知识库可满足性问题的判定过程。
2011-10-31 cs.AI
DeepProbLog: Neural Probabilistic Logic Programming
KU Leuven（鲁汶大学）；Cardiff University（卡迪夫大学）；Ghent University - imec（根特大学-校际微电子中心）
我们介绍DeepProbLog，这是一种概率逻辑程序设计语言，通过神经谓词结合了深度学习。我们展示了如何现有的推理和学习技术可以适应新的语言。我们的实验表明，DeepProbLog支持符号和子符号表示和推理，1）程序归纳，2）概率（逻辑）编程，3）从示例中进行（深度）学习。据我们所知，这项工作是第一个提出一个框架，其中通用神经网络和表达概率逻辑建模和推理集成的方式，利用充分的表现力和两个世界的优势，可以训练端到端的基础上的例子。
2018-12-12 cs.AI
Relative Expressiveness of Defeasible Logics II
University of New South Wales（新南威尔士大学）
本研究基于Maher 2012提出的两种相对表达能力概念，证明DL框架下的可废止逻辑在第一种定义下表达能力等价，第二种定义下个体击败与团队击败的逻辑表达能力等价，仅歧义处理方式会造成表达能力差异，完善了DL相对表达能力的研究。
2021-02-21 cs.AI cs.LO
An Expressive Probabilistic Temporal Logic
本文认为，概率，时间和行动的综合治疗是必不可少的概率的概念的适当的逻辑帐户，并根据这种直觉，描述了一个表达概率的时间逻辑推理的行动与不确定的结果。该逻辑是模态的和高阶的：由动作注释的模态用于表达由动作产生的下一状态中的命题的可能性和必要性，并且需要高阶函数来表达概率算子。所提出的逻辑被证明是经典数学概率论的一个适当的扩展，并通过Monty Hall问题的形式化来说明其表达能力。
2017-10-08 cs.AI cs.LO
Expressive Power of Graph Transformers via Logic
Tampere University（塔尔皮奥大学）；Leipzig University（莱比锡大学）
本文研究了图变换器和GPS网络在不同注意力机制下的表达能力，发现其在不同逻辑框架下的等价性。
2026-02-18 cs.AI cs.LO
Stream Reasoning on Expressive Logics
Işık University（伊什克大学）
数据流广泛存在于各种现实应用中。目前对流数据的研究主要集中在对流数据的数据管理、查询评价和优化等方面，而对流知识库在断言和术语两个层次上的推理过程的研究非常有限。通常，大型知识库上的推理服务非常昂贵，并且当数据作为流接收时需要连续应用。因此，需要新的技术来优化这个连续的过程，以开发高效的流数据推理机。在本文中，我们综述了相关的研究表达逻辑推理，可以应用于这一设置，并指出在这一领域的进一步研究方向。
2018-08-15 cs.AI cs.LO
On expressive rule-based logics
我们研究一个家庭的规则为基础的逻辑。重点是非常有表现力的语言。我们提供了一系列的表征结果的表达能力的逻辑，并将它们与相应的游戏系统。
2022-02-07 cs.LO
Expressive Completeness of Metric Temporal Logic
度量时态逻辑（Metric Temporal Logic，MTL）是线性时态逻辑的一种推广，其中Until和Since模态用表示度量约束的间隔来注释。Hirshfeld和Rabinovich的一个开创性的结果表明，在实数上，具有二进制顺序关系<和一元函数+1的一阶逻辑严格地比具有整数常数的MTL更具表达性。事实上，他们证明，没有时间逻辑的模态是由公式定义的有界量词深度可以表达完整的FO（<，+1）。在本文中，我们展示了一个令人惊讶的结果：如果我们在一阶逻辑中允许一元函数+q，（q有理数），并相应地允许MTL中的有理数常数，那么这两个逻辑具有相同的表达能力。这给出了第一个推广的坎普定理的表达完整性的LTL FO（<）的定量设置。这个结果的证明涉及Gabbay的分离概念的推广。
2013-02-16 cs.LO
When is Metric Temporal Logic Expressively Complete?
Kamp的一个开创性的结果是，在实数上，线性时态逻辑（LTL）具有与具有二元顺序关系<和一元谓词的一阶逻辑相同的表达能力。一个关键的问题是是否存在一个类似的度量时态逻辑（MTL）的坎普定理-一个推广的LTL中，直到和因为模态注释的区间表示度量约束。Hirshfeld和Rabinovich给出了否定的回答，证明了具有二元序关系<和一元函数+1的一阶逻辑严格地比具有整数常数的MTL更有表达性。然而，Hunter，Ouaknine和Worrell最近的一个结果表明，在合理的定时常数下，MTL具有与一阶逻辑相同的表达能力，给出了肯定的答案。在本文中，我们推广了这些结果，给出了一个精确的表征，MTL和一阶逻辑具有相同的表达能力的常数集。我们还表明，完整的一阶表达可以恢复与计数方式，强烈支持的断言Hirshfeld和Rabinovich的Q2 MLO是最具表达性的可判定的片段FO（<，+1）。
2013-02-16 cs.LO
Separating the Expressive Power of Propositional Dynamic and Modal Fixpoint Logics
我们调查的表达能力的两种主要类型的程序逻辑复杂的，非常规的程序属性在文献中发现：那些扩展命题动态逻辑（PDL），和那些扩展模态μ演算。这是受到最近发现的一种可判定程序逻辑的启发，这种逻辑被称为具有Chop的可见下推定点逻辑，它将模态μ演算和PDL扩展到可见下推语言上，到目前为止，这构成了可判定程序逻辑的两个支柱。在这里，我们表明这个逻辑不仅比它的两个片段中的任何一个更具表达力，而且事实上比它们的结合更具表达力。因此，程序逻辑之间的可判定性边界已经被适当地推高。我们完成了图片提供的结果分离所有的PDL为基础的和模态不动点逻辑与定期，明显下推和任意上下文无关的建设。
2021-08-24 cs.LO
The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics
RPTU Kaiserslautern-Landau（亚琛工业大学凯撒斯劳滕-兰道分校）；Queen Mary University of London（伦敦女王大学）；University of Łódź（卢宾大学）；Theoretical Computer Science / Formal Methods（理论计算机科学/形式方法）；University of Kassel（卡塞尔大学）
该研究首次通过二维乘积逻辑刻画时序GNN的表达能力，证明递归应用静态GNN的时序GNN可表达PTL与K的乘积逻辑的全部性质，而图-时间、全局TGNN仅能表达受限片段。
2025-10-28 cs.AI cs.LG cs.LO
The Expressive Power of Modal Dependence Logic
我们研究了各种模态逻辑与团队语义的表达能力。我们表明，正是向下封闭和封闭下的团队k-互模拟的团队的属性，对于一些有限的k，是可定义的模态逻辑扩展与直觉析取。此外，我们还证明了直觉析取模态逻辑和扩展模态依赖逻辑的表达能力是一致的。最后，我们建立任何翻译从扩展模态依赖逻辑到模态逻辑与直觉析取增加一些公式的大小呈指数级。
2014-06-24 cs.LO math.LO
Decidability of an Expressive Description Logic with Rational Grading
本文考虑了描述逻辑中实现理性分级的句法对象-概念构造子，即部分限制。部分限制能够表达关于后继集合的合理部分的语句，从本质上丰富了DL的表达能力。我们研究了一个扩展的研究DL ALCQIHR+部分限制，并证明了在扩展逻辑的推理仍然是可判定的。证明使用表格技术与指数技术，旨在处理部分限制。
2019-05-24 cs.LO
Logical Characterizations of Recurrent Graph Neural Networks with Reals and Floats
Tampere University（塔尔库大学）；Leipzig University（莱比锡大学）
本文在浮点数和实数两种场景下给出了循环图神经网络的精确逻辑刻画，并证明在MSO可定义属性上两者的表达能力等价，同时通过分布式自动机建立了与分布式计算模型的联系。
2025-05-02 cs.AI cs.LO
On the Expressive Power of Sub-Propositional Fragments of Modal Logic
模态逻辑是计算机科学中几种有用和适用的形式系统的范式。它通常保留了经典命题逻辑的低复杂性，但在描述、时间和空间逻辑领域存在明显的例外，其中最具表达力的形式主义具有非常高的复杂性，甚至是不可判定的。为了寻找计算上表现良好的片段，时态和描述逻辑的小句形式和其他子命题限制最近被研究。这种对子命题逻辑的新兴趣主要集中在各种片段的复杂性上，这就提出了关于它们的相对表达能力的自然问题，我们试图在这里回答基本的多模态逻辑Kn。我们考虑霍恩和克罗姆限制，以及模态逻辑的组合限制（称为核心片段），以及正交，通过不允许方块或菱形从正文字出现的片段。我们在一个非常一般的环境中研究这个问题，以便于将我们的结果转移到其他有意义的案例中。
2016-09-14 cs.LO
On Expressive Powers of Timed Logics: Comparing Boundedness, Non-punctuality and Deterministic Freezing
时间时态逻辑表现出令人困惑的多样性的运营商和由此产生的可判定性和表达性属性也有很大的不同。我们研究了时间逻辑TPTL[U，S]和MTL[U，S]以及它们的几个片段的表达能力。扩展Etessami和Wilke的LTL EF游戏，我们定义了MTL Escherichfeucht-Fraisse游戏上的一对定时词。利用相关的EF定理，我们证明了时间逻辑BoundedMTL[U，S]，MTL[F，P]和MITL[U，S]（分别包含有界性，一元模态和非准时性的限制）都是两两不可比的.作为我们的第一个主要结果，我们证明了MTL[U，S]严格包含在冻结逻辑TPTL[U，S]中，从而推广了Bouyer等人的结果，并完成了1990年Baur和Henziger猜想的证明.我们还涉及到最近提出的确定性冻结逻辑TTL[X，Y]（NP完全可满足性）MTL的表现力。作为我们的第二个主要结果，我们通过一个显式的约简证明了TTL[X，Y]严格地位于一元非准时逻辑MITL[F，P]内。这表明，具有准时性的确定性冻结在非准时MITL[F，P]中是可表达的。
2011-06-10 cs.LO
On the Expressive Power of TeamLTL and First-Order Team Logic over Hyperproperties
在这篇文章中，我们研究线性时态逻辑与团队语义（TeamLTL），是新的逻辑定义超属性。我们将这些逻辑的坎普型翻译定义为一阶团队逻辑和二阶逻辑的片段。我们还描述了团队逻辑和二阶逻辑的模型检查和可满足性的表达能力和复杂性，将它们与二阶和三阶算术联系起来。我们的结果集在一个更大的背景下，最近的结果Lück表明，扩展TeamLTL的布尔否定是高度不可判定的下，所谓的同步语义。我们还研究了TeamLTL扩展的口吃不变片段。
2021-10-21 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
On the Expressive Power of Inquisitive Team Logic and Inquisitive First-Order Logic
University of Helsinki（赫尔辛基大学）；University of Padua（帕多瓦大学）
本文证明探究团队逻辑中开放公式的表达能力严格超越一阶逻辑，并扩展至探究一阶逻辑，解决了一个开放问题。
2026-07-01 cs.LO math.LO
Understanding the Expressive Power of Unhygienic Substitution in Metaprogramming via Combinatory Logic
最近的工作组合逻辑演示了一个组合翻译从λ演算，使意义开放的条款。由于开放术语的含义是元编程研究中的一个关键难点，我们研究这种想法是否可以扩展到元编程系统与卫生和不卫生的替代，特别是$λ_{e}^{\rightarrow \Box}$和$λ_{\mathcal{S}}$。我们的结论是，有定量的证据来支持索赔，元编程与不卫生的替代是更强大的元编程与卫生的替代。
2019-10-08 cs.LO
Classical and Intuitionistic Subexponential Logics are Equally Expressive
经典逻辑的直觉限制被标准地看作是增加了逻辑的表达性，因为经典逻辑可以通过双重否定在直觉逻辑中得到充分的表示，而另一个方向没有真值保持的命题编码。在这里，我们表明，次指数逻辑，这是一个家庭的子结构的经典逻辑，每个参数在一个前序的次指数连接词的改进，不遭受这种不对称性，如果前序是系统修改的编码的一部分。准确地说，我们显示了合成（即，聚焦的）对给定编码取模的部分双导数。我们的编码特定的次指数前序的特殊情况下，产生了已知的和新的充分性定理的子结构逻辑。
2010-06-16 cs.LO
A note on the expressive power of linear orders
本文证明了存在两个特殊的线性序，使得具有这两个线性序的一阶逻辑与具有位谓词FO（Bit）的一阶逻辑具有相同的表达能力。作为推论，我们得到：也存在一个内置置换，使得一阶逻辑具有线性序，并且这个置换与FO（Bit）一样具有表达性。
2011-12-12 cs.LO
On expressive power and class invariance
在计算机科学中，定义了各种逻辑语言来分析系统的属性。找出这些逻辑之间的本质区别的一种方法是比较它们在区分能力和表达能力方面的表达能力。在本文中，我们研究这两个概念，把后者的概念作为前者提升到类的模型。我们展示了一些一般性的结果，提升模型的不变性关系的一类模型，这样，当前者对应于一个逻辑的区分能力，后者对应于它的表达能力，给出一定的紧凑性要求。特别是，我们引入类互模拟的概念来捕捉模态逻辑的表达能力。我们展示了我们的研究结果的应用，通过重新审视模态可定义性与我们的新见解。
2009-05-27 cs.LO
On two-variable guarded fragment logic with expressive local Presburger constraints
本文研究二变量守卫片段逻辑扩展局部Presburger量词后的可满足性问题，证明其为EXP完全，并提出一种新的简单确定性图算法给出上界。
2024-08-26 cs.LO
Revisiting the expressiveness of metric temporal logic : A tale of "Je t'aime, moi non plus."
IRIF, Université Paris Cité, France（IRIF，巴黎西岱大学）
本文通过比较区间语义和逐点语义，证明在标准有限或非芝诺无限时间执行模型下两者不可比较，并提出一种嵌入两者的混合语义。
2026-05-29 cs.LO
Expressive Logics for Coinductive Predicates
本文在余代数一般框架下研究逻辑对余归纳谓词的完全表征，提出充分性与表现性条件，并应用于相似性、发散性及自动机行为度量等实例。
2021-12-14 cs.LO
On the Expressiveness and Monitoring of Metric Temporal Logic
本文提出度量时序逻辑（MTL）的扩展，使其在有界及无界时间域上达到与FO[<, +1]相同的表达能力，并据此设计了首个与迹长度无关的稠密实时监控程序。
2019-05-09 cs.LO
The Expressive Power of k-ary Exclusion Logic
本文研究了用k元排它原子扩充一阶逻辑得到的k元排它逻辑EXC[k]的表达能力。排除逻辑与依赖逻辑是等价的，没有元界。通过观察翻译，我们发现EXC[k]的表达能力介于k元依赖逻辑和（k+1）元依赖逻辑之间。我们将证明，至少在k=1的情况下，这两个包含是适当的。在作者最近的工作中，证明了k元包含-排除逻辑与k元存在二阶逻辑ESO[k]是等价的。我们将证明，在句子的层次上，可以用排斥原子来模拟包含原子，并且这种方式只使用k元排斥原子来表达ESO[k]-句子。对于这种转换，我们还需要引入一种新的方法来“统一”团队中某些变量的值。因此，EXC[k]在句子级别上捕获ESO[k]，并且我们得到了排除逻辑的严格arity层次。它也遵循k元包含逻辑严格弱于EXC[k]。最后，我们将使用类似的技术来制定从ESO[k]到具有严格语义的k元包含逻辑的转换。因此，对于包含逻辑的任何arity片段，严格语义比宽松语义更具表达性。
2019-06-20 cs.LO math.LO
Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free (full version)
线性时序逻辑（LTL）是反应式系统的标准规约语言，并成功地应用于工业环境。然而，许多缺点LTL已被确定在文献中，其中有限的表达，缺乏定量特征，无法表达鲁棒性。有克服这些缺点的工作，但其中每一个通常是孤立地解决。这对于所有缺点同时显现的应用是不够的。在这里，我们通过引入解决多个缺点的逻辑来解决这个问题。为此，我们结合逻辑线性动态逻辑，LTL，和强大的LTL，每个解决一个方面，新的逻辑。对于两个方面的所有组合，所得到的逻辑具有与普通LTL相同的期望算法属性。特别是，为LTL开发的高效算法后端也适用于这些新逻辑。最后，我们讨论如何同时解决这三个方面。
2021-04-29 cs.FL 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
On the Expressiveness of State Space Models via Temporal Logics
University of Kassel（卡塞尔大学）
本文探讨了状态空间模型在不同门控机制下的表达能力，通过时序逻辑分析其与变换器架构的表达力差异。
2026-01-27 cs.FL cs.LG cs.LO
An Extensible Logic Embedding Tool for Lightweight Non-Classical Reasoning
University of Greifswald（格赖夫斯瓦尔德大学）
逻辑嵌入工具为非经典推理问题到经典高阶逻辑提供了一个过程编码。它是可扩展的，可以支持越来越多的不同的非经典逻辑推理的目标。当用作高阶定理证明器的预处理器或库时，该工具允许逻辑的现成自动化，否则目前很少有证明器可用。
2022-03-23 cs.AI cs.LO
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 logic with temporally accessible iteration
一阶逻辑在表达能力上的不足导致了不动点算子对一阶逻辑的大量扩展，如最小不动点（LFP）、膨胀不动点（IFP）、部分不动点（PFP）等。这些逻辑在有限模型论、数据库论、描述复杂性等方面得到了广泛的研究。本文介绍了一种统一的框架--带迭代算子的逻辑，在这种框架中，迭代步骤可以用时态逻辑公式来表示。我们表明，建议的逻辑FO+TAI包含所有提到的不动点扩展以及许多其他不动点逻辑的自然片段。另一方面，我们表明，在有限的结构FO+TAI是没有更多的表达比FO+PFP。此外，我们表明，增加相同的机器的逻辑单调归纳（FO+LFP）并没有增加其表达能力。
2008-06-17 cs.LO
Extending Two-Variable Logic on Trees
最近证明了在树上解释的一阶逻辑的两个变量片段的有限可满足性问题是ExpSpace完备的。我们考虑这个逻辑的两个扩展。我们发现，添加额外的二进制符号或计数量词的逻辑不影响有限可满足性问题的复杂性。然而，结合两个扩展并添加二进制符号和计数量词会导致这种复杂性的爆炸。我们还比较了两个变量的片段的表达能力，其扩展与计数量词的树木。事实证明，这两种逻辑具有同样的表达能力，尽管在无序树的限制情况下，计数量词确实增加了表达能力。
2016-11-24 cs.LO
Finite Model Reasoning in Expressive Fragments of First-Order Logic
在过去的二十年里，一阶逻辑的几个片段已经被识别出来，并显示出具有良好的计算和算法特性，在很大程度上是由于适当地描述了模态逻辑到一阶逻辑的标准翻译的图像。这尤其适用于受保护的片段，其中量词被原子适当地相对化，并且片段通过将变量的数量限制为两个来定义。这次谈话的目的是回顾最近的工作，这些片段和他们的流行扩展。当提出的材料特别注意的是有限的可满足性问题的决策程序，因为许多讨论的片段包含无穷公理。我们强调在这种情况下使用的最有效的技术，它们的优点和局限性。我们还提到了一些开放的研究方向。
2017-03-07 cs.LO
Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free
线性时序逻辑（LTL）是反应式系统的标准规约语言，并成功地应用于工业环境。然而，许多缺点LTL已被确定在文献中，其中有限的表达，缺乏定量特征，无法表达鲁棒性。有克服这些缺点的工作，但其中每一个通常是孤立地解决。这对于所有缺点同时显现的应用是不够的。在这里，我们通过引入解决多个缺点的逻辑来解决这个问题。为此，我们结合逻辑线性动态逻辑，LTL，和强大的LTL，每个解决一个方面，新的逻辑。对于两个方面的所有组合，所得到的逻辑具有与普通LTL相同的期望算法属性。特别是，为LTL开发的高效算法后端也适用于这些新逻辑。最后，我们讨论如何同时解决这三个方面。
2019-09-17 cs.FL cs.LO
Analytic Tableaux Calculi for KLM Logics of Nonmonotonic Reasoning
我们提出了一些逻辑的非单调推理，由克劳斯，莱曼和Magidor定义的表演算。我们给出了所有KLM逻辑，即优先，循环累积，累积和理性逻辑的一个Tableau证明过程。我们的演算是通过引入合适的模态来解释条件断言而获得的。我们提供了一个决策程序的逻辑考虑，我们研究它们的复杂性。
2006-11-10 cs.AI cs.LO
Characterizing and Reasoning about Probabilistic and Non-Probabilistic Expectation
期望是概率论的核心概念。期望的概念也适用于其他不确定性的概念。我们引入了一个命题逻辑推理的期望，语义取决于潜在的表示的不确定性。在基本表示是（a）概率，（b）概率测度集，（c）置信函数和（d）可能性测度的情况下，我们给出了该逻辑的合理而完整的公理化.我们表明，这种逻辑是更有表现力的比相应的逻辑推理的可能性的情况下的概率措施集，但同等表现力的情况下，概率，信念，和可能性。最后，我们证明了这些逻辑的可满足性是NP-完全的，并不比命题逻辑的可满足性难。
2007-04-20 cs.AI cs.LO
Extended Computation Tree Logic
我们介绍了一个通用的扩展流行的分支时间逻辑CTL细化的时间，直到和释放操作符与形式语言。例如，语言可以确定沿着路径的时刻，直到属性可以被满足。我们考虑几类语言导致逻辑具有不同的表达能力和复杂性，其重要性是出于他们的使用模型检验，合成，抽象解释等，我们表明，即使上下文无关的语言，直到操作逻辑仍然允许多项式时间模型检查，尽管显着增加的表达能力。这使得该逻辑在验证中的应用成为一个有希望的候选者。此外，我们分析了可满足性的复杂性，并比较了这些逻辑的表达能力CTL* 和PDL的扩展。
2010-06-18 cs.LO
On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic
本文研究了$\exists^*\forall^*$语言中带有量词前缀的前向公式的分离合取和蕴涵无限制嵌套的分离逻辑在可能位置论域为可数无限或有限的情况下的可满足性问题.与带有未解释谓词和等式的一阶逻辑类似，我们称这个片段为伯奈斯-舍恩芬克尔-拉姆齐分离逻辑[BSR（SLk）]。我们表明，不同于在一阶逻辑中，（在）有限可满足性问题是不可判定的BSR（SLk），我们定义了两个非平凡的子集，这是可判定的有限和无限的可满足性，分别通过控制的范围内的普遍量化变量的出现分离的影响，以及后者的出现的极性。可判定性结果是通过分离连接词的受控消除获得的，描述为（i）将前束形式分离逻辑公式有效地翻译成少量\emph{test formulae}的组合，仅使用一阶连接词，随后（ii）将后者翻译成可均衡满足的一阶公式。
2018-02-16 cs.LO
Modal Logics of Topological Relations
空间区域间关系推理的逻辑形式在地理信息系统、空间和约束数据库以及人工智能中的空间推理中起着重要作用。在类比Halpern和Shoham的模态逻辑的时间间隔的基础上的艾伦关系，我们介绍了一个家庭的模态逻辑配备了八个模态运营商，解释的Egenhofer-Franzosa（或RCC 8）的关系区域之间的拓扑空间，如真正的平面。我们调查的表达能力和计算复杂性的逻辑得到这种方式。事实证明，我们的模态逻辑具有与一阶逻辑的双变量片段相同的表达能力，但简洁性呈指数级下降。其复杂性范围从（不可判定和）递归可判定到高度不可判定，其中递归可判定逻辑是通过考虑拓扑空间诱导结构的子结构得到的.由于我们的不可判定性结果也捕获了基于实数线的逻辑，它们改进了Halpern和Shoham的区间时间逻辑的不可判定性结果。我们还分析了基于五个RCC 5关系的模态逻辑，关于表达能力的结果类似，但关于复杂性的结果较弱。
2006-06-22 cs.AI cs.CC cs.LO
