We study the problem of deciding satisfiability of first order logic queries over views, our aim being to delimit the boundary between the decidable and the undecidable fragments of this language. Views currently occupy a central place in database research, due to their role in applications such as information integration and data warehousing. Our main result is the identification of a decidable class of first order queries over unary conjunctive views that generalises the decidability of the classical class of first order sentences over unary relations, known as the Lowenheim class. We then demonstrate how various extensions of this class lead to undecidability and also provide some expressivity results. Besides its theoretical interest, our new decidable class is potentially interesting for use in applications such as deciding implication of complex dependencies, analysis of a restricted class of active database rules, and ontology reasoning.
Hyperproperties are properties of systems that relate different executions traces, with many applications from security to symmetry, consistency models of concurrency, etc. In recent years, different linear-time logics for specifying asynchronous hyperproperties have been investigated. Though model checking of these logics is undecidable, useful decidable fragments have been identified with applications e.g. for asynchronous security analysis. In this paper, we address expressiveness and decidability issues of temporal logics for asynchronous hyperproperties. We compare the expressiveness of t…
We consider first-order logic over the subword ordering on finite words, where each word is available as a constant. Our first result is that the $Σ_1$ theory is undecidable (already over two letters). We investigate the decidability border by considering fragments where all but a certain number of variables are alternation bounded, meaning that the variable must always be quantified over languages with a bounded number of letter alternations. We prove that when at most two variables are not alternation bounded, the $Σ_1$ fragment is decidable, and that it becomes undecidable when three variab…
Analyzing relational languages by their logical expressiveness is well understood. Something not well understood or even formalized is the vague concept of relational query patterns. What are query patterns? And how can we reason about query patterns across different relational languages, irrespective of their syntax and their procedural or declarative nature? In this paper, we formalize the concept of query patterns with a variant of pattern-preserving mappings between the relational atoms of queries. This formalism allows us to analyze the relative pattern expressiveness of relational query …
We consider dynamic versions of epistemic logic as formulated in Baltag and Moss "Logics for epistemic programs" (2004). That paper proposed a logical language (actually families of languages parameterized by action signatures) for dynamic epistemic logic. It had been shown that validity in the language is Pi-1-1-complete, so there are no recursively axiomatized complete logical systems for it. In contrast, this paper proves a weak completeness result for the fragment without action iteration, and a strong completeness result for the fragment without action iteration and common knowledge. Our …
Metric Temporal Logic, $\mtlfull$ is amongst the most studied real-time logics. It exhibits considerable diversity in expressiveness and decidability properties based on the permitted set of modalities and the nature of time interval constraints $I$. \oomit{The classical results of Alur and Henzinger showed that $\mtlfull$ is undecidable where as $\mitl$ which uses only non-singular intervals $NS$ is decidable. In a surprizing result, Ouaknine and Worrell showed that the satisfiability of $\mtl$ is decidable over finite pointwise models, albeit with NPR decision complexity, whereas it remains …
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（卡塞尔大学）
Hyperproperties, which generalize trace properties by relating multiple traces, are widely studied in information-flow security. Recently, a number of logics for hyperproperties have been proposed, and there is a need to understand their decidability and relative expressiveness. The new logics have been obtained from standard logics with two principal extensions: temporal logics, like LTL and CTL$^*$, have been generalized to hyperproperties by adding variables for traces or paths. First-order and second-order logics, like monadic first-order logic of order and MSO, have been extended with the…
We compare the model-theoretic expressiveness of the existential fragment of Separation Logic over unrestricted relational signatures (SLR) -- with only separating conjunction as logical connective and higher-order inductive definitions, traditionally known as the symbolic heap fragment -- with the expressiveness of (Monadic) Second Order Logic ((M)SO). While SLR and MSO are incomparable on structures of unbounded treewidth, it turns out that SLR can be embedded in SO, in general, and that MSO becomes a strict subset of SLR, when the treewidth of the models is bounded by a parameter given as i…
The stable model semantics had been recently generalized to non-Herbrand structures by several works, which provides a unified framework and solid logical foundations for answer set programming. This paper focuses on the expressiveness of normal and disjunctive programs under the general stable model semantics. A translation from disjunctive programs to normal programs is proposed for infinite structures. Over finite structures, some disjunctive programs are proved to be intranslatable to normal programs if the arities of auxiliary predicates and functions are bounded in a certain way. The equ…
Institute of Mathematical Sciences, Homi Bhabha National Institute（数学科学研究所，霍米·巴巴国家研究所）；Peking University（北京大学）
Quantified modal logic provides a natural logical language for reasoning about modal attitudes even while retaining the richness of quantification for referring to predicates over domains. But then most fragments of the logic are undecidable, over many model classes. Over the years, only a few fragments (such as the monodic) have been shown to be decidable. In this paper, we study fragments that bundle quantifiers and modalities together, inspired by earlier work on epistemic logics of know-how/why/what. As always with quantified modal logics, it makes a significant difference whether the doma…
Complexity and decidability of logics is a major research area involving a huge range of different logical systems. This calls for a unified and systematic approach for the field. We introduce a research program based on an algebraic approach to complexity classifications of fragments of first-order logic (FO) and beyond. Our base system GRA, or general relation algebra, is equiexpressive with FO. It resembles cylindric algebra but employs a finite signature with only seven different operators. We provide a comprehensive classification of the decidability and complexity of the systems obtained…
Saarland University（萨尔兰大学）；Université de Lorraine（洛林大学）；CNRS（法国国家科学研究中心）；LORIA（洛林计算机科学及其应用实验室）
We study finite first-order satisfiability (FSAT) in the constructive setting of dependent type theory. Employing synthetic accounts of enumerability and decidability, we give a full classification of FSAT depending on the first-order signature of non-logical symbols. On the one hand, our development focuses on Trakhtenbrot's theorem, stating that FSAT is undecidable as soon as the signature contains an at least binary relation symbol. Our proof proceeds by a many-one reduction chain starting from the Post correspondence problem. On the other hand, we establish the decidability of FSAT for mon…
The logical technique of focusing can be applied to the $λ$-calculus; in a simple type system with atomic types and negative type formers (functions, products, the unit type), its normal forms coincide with $βη$-normal forms. Introducing a saturation phase gives a notion of quasi-normal forms in presence of positive types (sum types and the empty type). This rich structure let us prove the decidability of $βη$-equivalence in presence of the empty type, the fact that it coincides with contextual equivalence, and a finite model property.
A Logical View of GNN-Style Computation and the Role of Activation Functions
Institute for Mathematical and Computational Engineering（数学与计算工程研究所）；Pontifical Catholic University of Chile（天主教智利大学）；IMFD；CENIA；Department of Computer Science, University of Antwerp（安特卫普大学计算机科学系）；Institute for Logic and Computation, TU Wien（逻辑与计算研究所，维也纳技术大学）；Data Science Institute, Universiteit Hasselt（数据科学研究所，哈塞尔特大学）
The classical decision problem, as it is understood today, is the quest for a delineation between the decidable and the undecidable parts of first-order logic based on elegant syntactic criteria. In this paper, we treat the concept of separateness of variables and explore its applicability to the classical decision problem. Two disjoint sets of first-order variables are separated in a given formula if variables from the two sets never co-occur in any atom of that formula. This simple notion facilitates extending many well-known decidable first-order fragments significantly and in a way that pr…
