Stream Reasoning on Expressive Logics

表达性描述逻辑的实用推理

Practical Reasoning for Expressive Description Logics

描述逻辑是一类知识表示形式化体系，其主要特征是构造器从原子概念和角色构造复杂的概念和角色。表达角色构造器在许多应用中很重要，但在计算上可能存在问题。我们提出了一个算法，决定可满足性的DL ALC扩展的传递和逆角色，角色层次结构，和合格的数量限制。早期的实验表明，该算法是非常适合实现。此外，我们还证明了仅具有传递和逆角色的ALC扩展仍然是PSPACE中的。最后，我们调查这个家庭的DL的可判定性的限制。

表达性描述逻辑中一致内插和遗忘的基础

Foundations for Uniform Interpolation and Forgetting in Expressive Description Logics

研究了描述逻辑ALC中的一致内插和遗忘问题。我们的主要结果是模型理论的一致插值和他们的存在性的bisimula- tions，严格的复杂性界决定一致插值的存在性，一种方法来计算插值时，他们存在，和严格的限制他们的大小。我们使用模型理论和自动机理论的方法，作为一个副产品，还提供了保守扩展的特征和决策程序的混合。

On expressive rule-based logics

We investigate a family of rule-based logics. The focus is on very expressive languages. We provide a range of characterization results for the expressive powers of the logics and relate them with corresponding game systems.

Signature-Based Abduction for Expressive Description Logics -- Technical Report

Signature-based abduction aims at building hypotheses over a specified set of names, the signature, that explain an observation relative to some background knowledge. This type of abduction is useful for tasks such as diagnosis, where the vocabulary used for observed symptoms differs from the vocabulary expected to explain those symptoms. We present the first complete method solving signature-based abduction for observations expressed in the expressive description logic ALC, which can include TBox and ABox axioms, thereby solving the knowledge base abduction problem. The method is guaranteed t…

度量时态逻辑的表达完备性

Expressive Completeness of Metric Temporal Logic

度量时态逻辑（Metric Temporal Logic，MTL）是线性时态逻辑的一种推广，其中Until和Since模态用表示度量约束的间隔来注释。Hirshfeld和Rabinovich的一个开创性的结果表明，在实数上，具有二进制顺序关系<和一元函数+1的一阶逻辑严格地比具有整数常数的MTL更具表达性。事实上，他们证明，没有时间逻辑的模态是由公式定义的有界量词深度可以表达完整的FO（<，+1）。在本文中，我们展示了一个令人惊讶的结果：如果我们在一阶逻辑中允许一元函数+q，（q有理数），并相应地允许MTL中的有理数常数，那么这两个逻辑具有相同的表达能力。这给出了第一个推广的坎普定理的表达完整性的LTL FO（<）的定量设置。这个结果的证明涉及Gabbay的分离概念的推广。

度量时态逻辑何时表达完备？

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）。

Separating the Expressive Power of Propositional Dynamic and Modal Fixpoint Logics

We investigate the expressive power of the two main kinds of program logics for complex, non-regular program properties found in the literature: those extending propositional dynamic logic (PDL), and those extending the modal mu-calculus. This is inspired by the recent discovery of a decidable program logic called Visibly Pushdown Fixpoint Logic with Chop which extends both the modal mu-calculus and PDL over visibly pushdown languages, which, so far, constituted the ends of two pillars of decidable program logics. Here we show that this logic is not only more expressive than either of its two …

基于二维乘积逻辑的时序图神经网络的逻辑表达能力

The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics

该研究首次通过二维乘积逻辑刻画时序GNN的表达能力，证明递归应用静态GNN的时序GNN可表达PTL与K的乘积逻辑的全部性质，而图-时间、全局TGNN仅能表达受限片段。

模态依赖逻辑的表现力

The Expressive Power of Modal Dependence Logic

我们研究了各种模态逻辑与团队语义的表达能力。我们表明，正是向下封闭和封闭下的团队k-互模拟的团队的属性，对于一些有限的k，是可定义的模态逻辑扩展与直觉析取。此外，我们还证明了直觉析取模态逻辑和扩展模态依赖逻辑的表达能力是一致的。最后，我们建立任何翻译从扩展模态依赖逻辑到模态逻辑与直觉析取增加一些公式的大小呈指数级。

Decidability of an Expressive Description Logic with Rational Grading

In this paper syntactic objects---concept constructors called part restrictions which realize rational grading are considered in Description Logics (DLs). Being able to convey statements about a rational part of a set of successors, part restrictions essentially enrich the expressive capabilities of DLs. We examine an extension of well-studied DL ALCQIHR+ with part restrictions, and prove that the reasoning in the extended logic is still decidable. The proof uses tableaux technique augmented with indices technique, designed for dealing with part restrictions.

高表达描述逻辑的实用推理

Practical Reasoning for Very Expressive Description Logics

描述逻辑是一类知识表示形式化体系，其主要特征是构造器从原子概念和角色构造复杂的概念和角色。表达角色构造器在许多应用中很重要，但在计算上可能存在问题。我们提出了一个算法，决定可满足性的DL ALC扩展与传递和逆角色和功能限制方面的一般概念包含公理和角色层次结构，早期的实验表明，该算法是非常适合实施。此外，我们还证明了仅具有传递和逆角色的ALC扩展仍然是PSPACE中的。我们调查这个家庭的DL的可判定性的限制，表明放松限制放置在数量限制中使用的各种角色导致所有推理问题的不可判定性。最后，我们描述了一些优化技术，这是至关重要的，在获得实现的决策过程中，尽管最坏情况下的问题的复杂性，表现出良好的性能与现实生活中的问题。

Polynomial Rewritings from Expressive Description Logics with Closed Predicates to Variants of Datalog

In many scenarios, complete and incomplete information coexist. For this reason, the knowledge representation and database communities have long shown interest in simultaneously supporting the closed- and the open-world views when reasoning about logic theories. Here we consider the setting of querying possibly incomplete data using logic theories, formalized as the evaluation of an ontology-mediated query (OMQ) that pairs a query with a theory, sometimes called an ontology, expressing background knowledge. This can be further enriched by specifying a set of closed predicates from the theory t…

具有实数与浮点数的循环图神经网络的逻辑刻画

Logical Characterizations of Recurrent Graph Neural Networks with Reals and Floats

本文在浮点数和实数两种场景下给出了循环图神经网络的精确逻辑刻画，并证明在MSO可定义属性上两者的表达能力等价，同时通过分布式自动机建立了与分布式计算模型的联系。

论模态逻辑子命题片段的表达力

On the Expressive Power of Sub-Propositional Fragments of Modal Logic

模态逻辑是计算机科学中几种有用和适用的形式系统的范式。它通常保留了经典命题逻辑的低复杂性，但在描述、时间和空间逻辑领域存在明显的例外，其中最具表达力的形式主义具有非常高的复杂性，甚至是不可判定的。为了寻找计算上表现良好的片段，时态和描述逻辑的小句形式和其他子命题限制最近被研究。这种对子命题逻辑的新兴趣主要集中在各种片段的复杂性上，这就提出了关于它们的相对表达能力的自然问题，我们试图在这里回答基本的多模态逻辑Kn。我们考虑霍恩和克罗姆限制，以及模态逻辑的组合限制（称为核心片段），以及正交，通过不允许方块或菱形从正文字出现的片段。我们在一个非常一般的环境中研究这个问题，以便于将我们的结果转移到其他有意义的案例中。

具有路径表达式的表达性描述逻辑中的数据复杂性

Data Complexity in Expressive Description Logics With Path Expressions

本文分析 ZOIQ 在拟森林上可满足性的数据复杂性，证明其 NP 完全，并据此重新刻画 OWL2 SR 族及 ZIQ 根查询蕴涵的复杂性界限。

论时间逻辑的表达能力：有界性、非准时性和确定性冻结的比较

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]中是可表达的。

用激光进行表达流推理

Expressive Stream Reasoning with Laser

越来越多的用例需要从语义注释的数据流中及时提取重要知识，特别是在Web和物联网（IoT）上。通常，这种提取需要表达性推理，这在大型流上计算是具有挑战性的。我们提出激光，一个新的推理机，支持一个务实的，非平凡的片段的逻辑LARS扩展回答集编程（ASP）的流。在其核心，激光实现了一种新的评估程序，该程序注释公式，以避免在多个时间点重复计算。这个过程，结合一个明智的实施LARS运营商，是负责显着更好的运行时间比其他国家的最先进的系统，如C-SPARQL和CQELS，或执行LARS上运行的ASP求解器Clingo。这使得基于表达逻辑的推理能够应用于大型流，并为更广泛的流推理用例打开了大门。

On the Expressive Power of TeamLTL and First-Order Team Logic over Hyperproperties

In this article we study linear temporal logics with team semantics (TeamLTL) that are novel logics for defining hyperproperties. We define Kamp-type translations of these logics into fragments of first-order team logic and second-order logic. We also characterize the expressive power and the complexity of model-checking and satisfiability of team logic and second-order logic by relating them to second- and third-order arithmetic. Our results set in a larger context the recent results of Lück showing that the extension of TeamLTL by the Boolean negation is highly undecidable under the so-calle…

包含原子模态逻辑的表达能力

The expressive power of modal logic with inclusion atoms

模态包含逻辑是基本模态逻辑的包含原子扩展，其语义定义在Kripke模型上。Kripke模型的团队只是其域的一个子集。本文给出了模态包含逻辑表达能力的一个完整刻画：一类带队的Kripke模型在模态包含逻辑中是可定义的当且仅当它在k-互模拟下是闭的，对于某个整数k，它在并下是闭的，并且它具有空队性质.我们还证明了同样的表达能力，可以通过添加一个单一的一元非空算子模态逻辑。此外，我们建立了一个指数下界的大小从模态包含逻辑到模态逻辑与非空算子的翻译。

探究团队逻辑和探究一阶逻辑的表达能力

On the Expressive Power of Inquisitive Team Logic and Inquisitive First-Order Logic

本文证明探究团队逻辑中开放公式的表达能力严格超越一阶逻辑，并扩展至探究一阶逻辑，解决了一个开放问题。

Understanding the Expressive Power of Unhygienic Substitution in Metaprogramming via Combinatory Logic

Recent work on combinatory logic demonstrates a compositional translation from lambda calculus that gives meaning to open terms. As the meaning of open terms is a key difficulty in the study of metaprogramming, we investigate whether this idea can be extended to metaprogramming systems with hygienic and unhygienic substitution, specifically $λ_{e}^{\rightarrow \Box}$ and $λ_{\mathcal{S}}$. We conclude that there is quantitative evidence to support the claim that metaprogramming with unhygienic substitution is more powerful than metaprogramming with hygienic substitution.

经典次指数逻辑和直觉次指数逻辑具有相同的表达性

Classical and Intuitionistic Subexponential Logics are Equally Expressive

经典逻辑的直觉限制被标准地看作是增加了逻辑的表达性，因为经典逻辑可以通过双重否定在直觉逻辑中得到充分的表示，而另一个方向没有真值保持的命题编码。在这里，我们表明，次指数逻辑，这是一个家庭的子结构的经典逻辑，每个参数在一个前序的次指数连接词的改进，不遭受这种不对称性，如果前序是系统修改的编码的一部分。准确地说，我们显示了合成（即，聚焦的）对给定编码取模的部分双导数。我们的编码特定的次指数前序的特殊情况下，产生了已知的和新的充分性定理的子结构逻辑。

关于线性序表达能力的一个注记

A note on the expressive power of linear orders

本文证明了存在两个特殊的线性序，使得具有这两个线性序的一阶逻辑与具有位谓词FO（Bit）的一阶逻辑具有相同的表达能力。作为推论，我们得到：也存在一个内置置换，使得一阶逻辑具有线性序，并且这个置换与FO（Bit）一样具有表达性。

论表达力与类不变性

On expressive power and class invariance

在计算机科学中，定义了各种逻辑语言来分析系统的属性。找出这些逻辑之间的本质区别的一种方法是比较它们在区分能力和表达能力方面的表达能力。在本文中，我们研究这两个概念，把后者的概念作为前者提升到类的模型。我们展示了一些一般性的结果，提升模型的不变性关系的一类模型，这样，当前者对应于一个逻辑的区分能力，后者对应于它的表达能力，给出一定的紧凑性要求。特别是，我们引入类互模拟的概念来捕捉模态逻辑的表达能力。我们展示了我们的研究结果的应用，通过重新审视模态可定义性与我们的新见解。

关于带有表达性局部Presburger约束的二变量守卫片段逻辑

On two-variable guarded fragment logic with expressive local Presburger constraints

本文研究二变量守卫片段逻辑扩展局部Presburger量词后的可满足性问题，证明其为EXP完全，并提出一种新的简单确定性图算法给出上界。

重温度量时态逻辑的表达能力：一个“我爱你，我也不爱你”的故事。

Revisiting the expressiveness of metric temporal logic : A tale of "Je t'aime, moi non plus."

本文通过比较区间语义和逐点语义，证明在标准有限或非芝诺无限时间执行模型下两者不可比较，并提出一种嵌入两者的混合语义。

余归纳谓词的表现性逻辑

Expressive Logics for Coinductive Predicates

本文在余代数一般框架下研究逻辑对余归纳谓词的完全表征，提出充分性与表现性条件，并应用于相似性、发散性及自动机行为度量等实例。

度量时序逻辑的表达能力与监控

On the Expressiveness and Monitoring of Metric Temporal Logic

本文提出度量时序逻辑（MTL）的扩展，使其在有界及无界时间域上达到与FO[<, +1]相同的表达能力，并据此设计了首个与迹长度无关的稠密实时监控程序。

The Expressive Power of k-ary Exclusion Logic

In this paper we study the expressive power of k-ary exclusion logic, EXC[k], that is obtained by extending first order logic with k-ary exclusion atoms. It is known that without arity bounds exclusion logic is equivalent with dependence logic. By observing the translations, we see that the expressive power of EXC[k] lies in between k-ary and (k+1)-ary dependence logics. We will show that, at least in the case of k=1, the both of these inclusions are proper. In a recent work by the author it was shown that k-ary inclusion-exclusion logic is equivalent with k-ary existential second order logic,…

Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free (full version)

Linear Temporal Logic (LTL) is the standard specification language for reactive systems and is successfully applied in industrial settings. However, many shortcomings of LTL have been identified in the literature, among them the limited expressiveness, the lack of quantitative features, and the inability to express robustness. There is work on overcoming these shortcomings, but each of these is typically addressed in isolation. This is insufficient for applications where all shortcomings manifest themselves simultaneously. Here, we tackle this issue by introducing logics that address more than…

模态独立逻辑

Modal Independence Logic

本文介绍了模态独立逻辑MIL，模态逻辑，可以显式地谈论命题变量之间的独立性。MIL的公式不是在世界中评估的，而是在世界的集合中评估的，所谓的团队。在这种情况下，MIL可以被看作是Väänänen的模态依赖逻辑MDL的变体。我们发现，MIL嵌入MDL，是严格更具表现力。然而，在单例团队中，MIL并不比通常的模态逻辑更具表达力，但MIL是指数更简洁。利用一种新的互模拟形式，我们将这些表达性结果扩展到由各种广义依赖原子扩展的模态逻辑。我们通过给出MIL中用餐密码协议的匿名性要求的规范来证明MIL的表达能力。我们还研究了MIL的复杂性问题，并表明，虽然它更具表达性，但它的可满足性和模型检验问题具有与MDL相同的复杂性。

通过时序逻辑探讨状态空间模型的表达能力

On the Expressiveness of State Space Models via Temporal Logics

本文探讨了状态空间模型在不同门控机制下的表达能力，通过时序逻辑分析其与变换器架构的表达力差异。

具有时间可达迭代的逻辑

A logic with temporally accessible iteration

一阶逻辑在表达能力上的不足导致了不动点算子对一阶逻辑的大量扩展，如最小不动点（LFP）、膨胀不动点（IFP）、部分不动点（PFP）等。这些逻辑在有限模型论、数据库论、描述复杂性等方面得到了广泛的研究。本文介绍了一种统一的框架--带迭代算子的逻辑，在这种框架中，迭代步骤可以用时态逻辑公式来表示。我们表明，建议的逻辑FO+TAI包含所有提到的不动点扩展以及许多其他不动点逻辑的自然片段。另一方面，我们表明，在有限的结构FO+TAI是没有更多的表达比FO+PFP。此外，我们表明，增加相同的机器的逻辑单调归纳（FO+LFP）并没有增加其表达能力。

二元逻辑在树上的扩展

Extending Two-Variable Logic on Trees

最近证明了在树上解释的一阶逻辑的两个变量片段的有限可满足性问题是ExpSpace完备的。我们考虑这个逻辑的两个扩展。我们发现，添加额外的二进制符号或计数量词的逻辑不影响有限可满足性问题的复杂性。然而，结合两个扩展并添加二进制符号和计数量词会导致这种复杂性的爆炸。我们还比较了两个变量的片段的表达能力，其扩展与计数量词的树木。事实证明，这两种逻辑具有同样的表达能力，尽管在无序树的限制情况下，计数量词确实增加了表达能力。

一阶逻辑表达片段中的有限模型推理

Finite Model Reasoning in Expressive Fragments of First-Order Logic

在过去的二十年里，一阶逻辑的几个片段已经被识别出来，并显示出具有良好的计算和算法特性，在很大程度上是由于适当地描述了模态逻辑到一阶逻辑的标准翻译的图像。这尤其适用于受保护的片段，其中量词被原子适当地相对化，并且片段通过将变量的数量限制为两个来定义。这次谈话的目的是回顾最近的工作，这些片段和他们的流行扩展。当提出的材料特别注意的是有限的可满足性问题的决策程序，因为许多讨论的片段包含无穷公理。我们强调在这种情况下使用的最有效的技术，它们的优点和局限性。我们还提到了一些开放的研究方向。

Robust, Expressive, and Quantitative Linear Temporal Logics: Pick any Two for Free

Linear Temporal Logic (LTL) is the standard specification language for reactive systems and is successfully applied in industrial settings. However, many shortcomings of LTL have been identified in the literature, among them the limited expressiveness, the lack of quantitative features, and the inability to express robustness. There is work on overcoming these shortcomings, but each of these is typically addressed in isolation. This is insufficient for applications where all shortcomings manifest themselves simultaneously. Here, we tackle this issue by introducing logics that address more than…

概率期望与非概率期望的表征与推理

Characterizing and Reasoning about Probabilistic and Non-Probabilistic Expectation

期望是概率论的核心概念。期望的概念也适用于其他不确定性的概念。我们引入了一个命题逻辑推理的期望，语义取决于潜在的表示的不确定性。在基本表示是（a）概率，（b）概率测度集，（c）置信函数和（d）可能性测度的情况下，我们给出了该逻辑的合理而完整的公理化.我们表明，这种逻辑是更有表现力的比相应的逻辑推理的可能性的情况下的概率措施集，但同等表现力的情况下，概率，信念，和可能性。最后，我们证明了这些逻辑的可满足性是NP-完全的，并不比命题逻辑的可满足性难。

扩展计算树逻辑

Extended Computation Tree Logic

我们介绍了一个通用的扩展流行的分支时间逻辑CTL细化的时间，直到和释放操作符与形式语言。例如，语言可以确定沿着路径的时刻，直到属性可以被满足。我们考虑几类语言导致逻辑具有不同的表达能力和复杂性，其重要性是出于他们的使用模型检验，合成，抽象解释等，我们表明，即使上下文无关的语言，直到操作逻辑仍然允许多项式时间模型检查，尽管显着增加的表达能力。这使得该逻辑在验证中的应用成为一个有希望的候选者。此外，我们分析了可满足性的复杂性，并比较了这些逻辑的表达能力CTL* 和PDL的扩展。

On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic

This paper investigates the satisfiability problem for Separation Logic, with unrestricted nesting of separating conjunctions and implications, for prenex formulae with quantifier prefix in the language $\exists^*\forall^*$, in the cases where the universe of possible locations is either countably infinite or finite. In analogy with first-order logic with uninterpreted predicates and equality, we call this fragment Bernays-Schönfinkel-Ramsey Separation Logic [BSR(SLk)]. We show that, unlike in first-order logic, the (in)finite satisfiability problem is undecidable for BSR(SLk) and we define tw…

拓扑关系的模态逻辑

Modal Logics of Topological Relations

空间区域间关系推理的逻辑形式在地理信息系统、空间和约束数据库以及人工智能中的空间推理中起着重要作用。在类比Halpern和Shoham的模态逻辑的时间间隔的基础上的艾伦关系，我们介绍了一个家庭的模态逻辑配备了八个模态运营商，解释的Egenhofer-Franzosa（或RCC 8）的关系区域之间的拓扑空间，如真正的平面。我们调查的表达能力和计算复杂性的逻辑得到这种方式。事实证明，我们的模态逻辑具有与一阶逻辑的双变量片段相同的表达能力，但简洁性呈指数级下降。其复杂性范围从（不可判定和）递归可判定到高度不可判定，其中递归可判定逻辑是通过考虑拓扑空间诱导结构的子结构得到的.由于我们的不可判定性结果也捕获了基于实数线的逻辑，它们改进了Halpern和Shoham的区间时间逻辑的不可判定性结果。我们还分析了基于五个RCC 5关系的模态逻辑，关于表达能力的结果类似，但关于复杂性的结果较弱。

布尔依赖逻辑与偏序连接词

Boolean Dependence Logic and Partially-Ordered Connectives

我们介绍了一种新的依赖逻辑称为布尔依赖逻辑。在布尔依赖逻辑中，依赖原子的类型为=（x_1，...，x_n，α），其中α是布尔变量。直觉上，布尔依赖原子可以表示关系的量化，而标准依赖原子表示函数的量化。我们比较布尔依赖逻辑的表达能力依赖逻辑和一阶逻辑丰富的偏序连接词。我们证明了布尔依赖逻辑和依赖逻辑的表达能力是一致的。我们定义了自然的布尔依赖逻辑的语法片段，并表明，他们符合相应的片段的一阶逻辑丰富的偏序连接词的表达能力。然后，我们表明，片段形成一个严格的层次结构。

一种用于递归程序的可表达迹逻辑

An Expressive Trace Logic for Recursive Programs

本文提出一种基于迹公式的可表达逻辑，为递归程序提供组合式指称语义和证明演算，并建立程序与公式间的 Galois 连接，揭示程序构造与逻辑连接词的对应关系。

关于TPTL和MTL在ω-数据字上的表示

On the Expressiveness of TPTL and MTL over ω-Data Words

度量时态逻辑（MTL）和时间命题时态逻辑（TPTL）是线性时态逻辑的突出扩展，用于指定数据语言的属性。本文研究了自然数上的非单调数据词的数据语言类。我们证明，在这种情况下，TPTL是严格的表达比MTL。为此，我们介绍Escherichfeucht-Fraisse（EF）游戏MTL。使用EF游戏的MTL，我们还证明了MTL可定义性决策问题（“给定一个TPTL公式，这个公式定义的语言在MTL中可定义吗？“）是不可判定的。我们还定义了EF游戏的TPTL，我们表现出的MTL和TPTL的表现力的各种句法限制的效果。

用于共代数的表达性Quantale值逻辑：一种基于伴随的方法

Expressive Quantale-valued Logics for Coalgebras: an Adjunction-based Approach

该研究基于伴随框架，从刻画行为一致性的模态逻辑推导不动点方程，将其实例化到共代数场景，还得到线性时间下简洁的逻辑与不动点方程，并在分支、线性时间场景中验证了理论。

探究性认知逻辑的表达能力

On the expressive power of inquisitive epistemic logic

该研究利用InqML框架的互模拟等价概念，将探究性认知逻辑（InqML）的表达能力刻画为一阶逻辑在双排序一阶结构上的互模拟不变片段，需用非经典模型论方法分析其非初等性质。

序不变逻辑在深度有界结构上的简洁性

Succinctness of Order-Invariant Logics on Depth-Bounded Structures

研究了一阶逻辑和一元二阶逻辑的序不变句在有界树深结构上的表达能力和简洁性。一般来说，顺序不变是不可判定的，因此，人们努力寻找具有与顺序不变句子相同的表达能力的可判定语法的逻辑。我们表明，在有界树深度的结构，顺序不变的FO具有相同的表达能力FO。我们的证明技术允许对这种翻译的简洁性进行细粒度的分析。我们证明了，对于每一个顺序不变的FO句子存在一个FO句子，其大小是小学的原始句子的大小，其数量的交替是线性的树深度。我们得到类似的结果MSO。MSO和FO的表达能力在有界树深结构上是一致的。我们提供了一个翻译MSO FO，我们表明，这种翻译基本上是最佳的公式大小。作为进一步的结果，我们表明，顺序不变的MSO具有相同的表达能力，FO与有界树深度结构上的模计数量词。

数量限制下角色合成的表达描述逻辑的可判定性

On Decidability of Expressive Description Logics with Composition of Roles in Number Restrictions

描述逻辑是一种知识表示的形式化方法，在广泛的应用领域中得到了广泛的应用。由于其吸引人的表现力，我们认为在本文中扩展的著名的概念语言ALC允许复杂的角色表达式的数量限制。这些语言首先由Baader和Sattler作为ALCN（M）语言引入，采用了{o，-，And，Or}的角色构造函数M子集。特别是，他们在1999年证明，虽然ALCN（o）是可判定的，但添加其他算子可能很容易导致不可判定性：事实上，ALCN（o，And）和ALCN（o，-，Or）被证明是不可判定的。在这项工作中，我们进一步研究的计算性能的ALCN家庭，旨在缩小可判定性的差距留下开放的Baader和Sattler的结果。特别是，我们将证明ALCN（o）扩展与逆角色在数量和价值的限制变得不可判定，而它可以安全地扩展与合格的数量限制，而不会失去可判定性。

DL-Lite的表现力

The Expressive Power of DL-Lite

描述逻辑是知识表示的形式主义，它提供了语义网的形式基础，特别是$\text{OWL}$本体Web语言。本文研究了逻辑$\text{DL-Lite}_{R,\sqcap}$的表达能力及其计算性质。我们依靠模拟来表征$\text{DL-Lite}_{R,\sqcap}$作为概念语言的绝对表达能力，并表明析取是不可表达的。我们还表明，没有模拟为基础的封闭属性存在$\text{DL-Lite}_{R,\sqcap}$断言。最后，我们证明了联合查询的查询应答是$\text{NP-complete}$。

用于细胞自动机的表达性余代数模态逻辑

An Expressive Coalgebraic Modal Logic for Cellular Automata

本文提出了一种用于细胞自动机的余代数模态逻辑，通过行为等价性推断其行为，并证明了Hennessy-Milner定理。

有界度类上的后继不变一阶逻辑

Successor-Invariant First-Order Logic on Classes of Bounded Degree

本文研究后继不变一阶逻辑的表达能力，证明在有界度类上其表达能力不高于普通一阶逻辑。

知识、意识和互模拟

Knowledge, Awareness, and Bisimulation

我们比较不同的认识概念中存在的意识命题变量：逻辑的隐性知识（其中明确的知识是可定义的），明确的知识，和投机性的知识。互模拟的不同概念适用于这些逻辑。我们提供这些逻辑的图像有限模型之间的相互模拟和模态等价的对应关系。推理知识的逻辑与显性知识的逻辑具有同样的表达能力，而隐性知识的逻辑比这两者更具表达能力。我们还提供了公理化的三个逻辑-只有一个投机知识是新颖的。然后，我们通过回忆包含意识的动作模型来研究动态。我们表明，任何可以想象的知识或意识的变化，可以在这种情况下建模，我们给了一个完整的公理化的动态逻辑的隐性知识。令人惊讶的是，所有三种逻辑的动态版本都具有同样的表达能力。

定时模态μ演算的表达性结果

Expressiveness Results for Timed Modal Mu-Calculi

本文证明了定时模态μ演算$L^{rel}_{ν,μ}$严格强于其他μ演算及TCTL，而其他μ演算与TCTL在一般定时自动机上不可比较。

On the Expressive Power of the Normal Form for Branching-Time Temporal Logics

With the emerging applications that involve complex distributed systems branching-time specifications are specifically important as they reflect dynamic and non-deterministic nature of such applications. We describe the expressive power of a simple yet powerful branching-time specification framework -- branching-time normal form (BNF), which has been developed as part of clausal resolution for branching-time temporal logics. We show the encoding of Buchi Tree Automata in the language of the normal form, thus representing, syntactically, tree automata in a high-level way. Thus we can treat BNF …

论角色逻辑

On Role Logic

我们提出的角色逻辑，一个符号的关系结构的形状分析，数据库和知识库中描述的属性。我们使用de Bruijn的λ演算符号的思想来构造角色逻辑，在λ演算中编码一阶逻辑，以及一元和二元谓词的隐式参数的简单规则。角色逻辑的无限制版本具有传递闭包的一阶逻辑的表达能力。通过对角色逻辑公式的句法限制，我们识别出角色逻辑的一个自然片段RL ^2。我们证明了RL^2片段与计数C^2的二元逻辑具有相同的表达能力，因此是可判定的。我们提出了一个翻译的命令式语言到可判定的片段RL ^[2]，它允许组合验证的程序，操纵关系结构。此外，我们展示了RL^2如何编码布尔形状分析约束和一个富有表现力的描述逻辑。