该论文证明二维 Weisfeiler-Leman 算法在 n 顶点图上稳定所需迭代次数为 O(n^2/log(n))，改进了平凡上界，并由此导出 C3 与 L3 逻辑中量词深度的对应上界。
摘要：
我们证明，在具有 n 个顶点的图上，二维 Weisfeiler-Leman 算法达到稳定所需的迭代次数至多为 O(n^2/log(n))。这特别表明，先前最佳的平凡上界 O(n^2) 在渐近意义上并不紧。在逻辑设定中，这转化为如下陈述：如果两个大小为 n 的图可以通过带计数的一阶逻辑公式（即 C3 逻辑）区分，那么它们也可以通过一个量词深度至多为 O(n^2/log(n)) 的 C3 公式区分。为了证明该结果，我们定义了一个双人博弈，它使我们能够解耦算法多次迭代中同时发生的过程之间的因果依赖关系。这允许我们分别处理大的颜色类和小的颜色类。作为证明的一部分，我们表明对于颜色类大小有界的图，达到稳定所需的迭代次数至多与顶点数成线性关系。这也产生了带计数的一阶逻辑中的相应陈述。类似的结果也可以在没有计数量词的相应逻辑（即 L3 逻辑）中获得。
英文摘要：
We show that on graphs with n vertices, the 2-dimensional Weisfeiler-Leman algorithm requires at most O(n^2/log(n)) iterations to reach stabilization. This in particular shows that the previously best, trivial upper bound of O(n^2) is asymptotically not tight. In the logic setting, this translates to the statement that if two graphs of size n can be distinguished by a formula in first-order logic with counting with 3 variables (i.e., in C3), then they can also be distinguished by a C3-formula that has quantifier depth at most O(n^2/log(n)).
To prove the result we define a game between two players that enables us to decouple the causal dependencies between the processes happening simultaneously over several iterations of the algorithm. This allows us to treat large color classes and small color classes separately. As part of our proof we show that for graphs with bounded color class size, the number of iterations until stabilization is at most linear in the number of vertices. This also yields a corresponding statement in first-order logic with counting.
Similar results can be obtained for the respective logic without counting quantifiers, i.e., for the logic L3.
Algebraic logic studies algebraic theories related to proposition and first-order logic. A new algebraic approach to first-order logic is sketched in this paper. We introduce the notion of a quantifier theory, which is a functor from the category of a monad of sets to the category of Boolean algebras, together with a uniquely determined system of quantifiers. A striking feature of this approach is that Cayley's Completeness Theorem and Godel's Completeness Theorem can be stated and proved in a much simpler fashion for quantifier theories. Both theorems are due to Halmos for polyadic algebras. …
The satisfiability problem of the branching time logic CTL is studied in terms of computational complexity. Tight upper and lower bounds are provided for each temporal operator fragment. In parallel, the minimal model size is studied with a suitable notion of minimality. Thirdly, flat CTL is investigated, i.e., formulas with very low temporal operator nesting depth. A sharp dichotomy is shown in terms of complexity and minimal models: Temporal depth one has low expressive power, while temporal depth two is equivalent to full CTL.
We study the extension of dependence logic D by a majority quantifier M over finite structures. We show that the resulting logic is equi-expressive with the extension of second-order logic by second-order majority quantifiers of all arities. Our results imply that, from the point of view of descriptive complexity theory, D(M) captures the complexity class counting hierarchy.
We study a natural hierarchy in first-order logic, namely the quantifier structure hierarchy, which gives a systematic classification of first-order formulas based on structural quantifier resource. We define a variant of Ehrenfeucht-Fraisse games that characterizes quantifier classes and use it to prove that this hierarchy is strict over finite structures, using strategy compositions. Moreover, we prove that this hierarchy is strict even over ordered finite structures, which is interesting in the context of descriptive complexity.
This paper explores the computational complexity of various natural one-variable fragments of first-order modal logics with the addition of counting quantifiers, over both constant and varying domains. The addition of counting quantifiers provides us a rich language with which to succinctly express statements about the quantity of objects satisfying a given first-order property, using a single variable. Optimal NExpTime upper-bounds are provided for the satisfiability problems of the one-variable fragment of the minimal first-order modal logic QK, over both constant and expanding/decreasing do…
We prove two completeness results, one for the extension of dependence logic by a monotone generalized quantifier Q with weak interpretation, weak in the meaning that the interpretation of Q varies with the structures. The second result considers the extension of dependence logic where Q is interpreted as "there exists uncountable many." Both of the axiomatizations are shown to be sound and complete for FO(Q) consequences.
Constraint LTL, a generalisation of LTL over Presburger constraints, is often used as a formal language to specify the behavior of operational models with constraints. The freeze quantifier can be part of the language, as in some real-time logics, but this variable-binding mechanism is quite general and ubiquitous in many logical languages (first-order temporal logics, hybrid logics, logics for sequence diagrams, navigation logics, logics with lambda-abstraction etc.). We show that Constraint LTL over the simple domain (N,=) augmented with the freeze quantifier is undecidable which is a surpri…
We prove that the theory of Monadic Second-Order logic (MSO) of the infinite binary tree extended with qualitative path-measure quantifier is undecidable. This quantifier says that the set of infinite paths in the tree that satisfies some formula has Lebesgue-measure one. To do this we prove that the emptiness problem of qualitative universal parity tree automata is undecidable. Qualitative means that a run of a tree automaton is accepting if the set of paths in the run that satisfy the acceptance condition has Lebesgue-measure one.
Classical logic is embedded into constructive logic, through a definition of the classical connectives and quantifiers in terms of the constructive ones.
A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data words, linear temporal logic is extended by the freeze quantifier, which stores the element at the current word position into a register, for equality comparisons deeper in the formula. By translations from the logic to alternating automata with registers and then to faulty counter automata whose counters may erroneously increase at any time, and from faulty and error-free counter automata to the logic, we obtain a c…
We present alternative definitions of the first-order stable model semantics and its extension to incorporate generalized quantifiers by referring to the familiar notion of a reduct instead of referring to the SM operator in the original definitions. Also, we extend the FLP stable model semantics to allow generalized quantifiers by referring to an operator that is similar to the $\sm$ operator. For a reasonable syntactic class of logic programs, we show that the two stable model semantics of generalized quantifiers are interchangeable.
We study logics defined in terms of second-order monadic monoidal and groupoidal quantifiers. These are generalized quantifiers defined by monoid and groupoid word-problems, equivalently, by regular and context-free languages. We give a computational classification of the expressive power of these logics over strings with varying built-in predicates. In particular, we show that ATIME(n) can be logically characterized in terms of second-order monadic monoidal quantifiers.
The list segment predicate ls used in separation logic for verifying programs with pointers is well-suited to express properties on singly-linked lists. We study the effects of adding ls to the full quantifier-free separation logic with the separating conjunction and implication, which is motivated by the recent design of new fragments in which all these ingredients are used indifferently and verification tools start to handle the magic wand connective. This is a very natural extension that has not been studied so far. We show that the restriction without the separating implication can be solv…
We consider the quantifier alternation hierarchy within two-variable first-order logic FO^2[<,suc] over finite words with linear order and binary successor predicate. We give a single identity of omega-terms for each level of this hierarchy. This shows that it is decidable for a given regular language and a non-negative integer m, whether the language is definable by a formula in FO^2[<,suc] which has at most m quantifier alternations. We also consider the alternation hierarchy of unary temporal logic TL[X,F,Y,P] defined by the maximal number of nested negations. This hierarchy coincides with …
This paper presents a way of formalising definite descriptions with a binary quantifier $ι$, where $ιx[F, G]$ is read as `The $F$ is $G$'. Introduction and elimination rules for $ι$ in a system of intuitionist negative free logic are formulated. Procedures for removing maximal formulas of the form $ιx[F, G]$ are given, and it is shown that deductions in the system can be brought into normal form.
This paper gives a thorough overview of what is known about first-order logic with counting quantifiers and with arithmetic predicates. As a main theorem we show that Presburger arithmetic is closed under unary counting quantifiers. Precisely, this means that for every first-order formula phi(y,z_1,...,z_k) over the signature {<,+} there is a first-order formula psi(x,z_1,...,z_k) which expresses over the structure <Nat,<,+> (respectively, over initial segments of this structure) that the variable x is interpreted exactly by the number of possible interpretations of the variable y for which th…
We prove near-optimal trade-offs for quantifier depth versus number of variables in first-order logic by exhibiting pairs of $n$-element structures that can be distinguished by a $k$-variable first-order sentence but where every such sentence requires quantifier depth at least $n^{Ω(k/\log k)}$. Our trade-offs also apply to first-order counting logic, and by the known connection to the $k$-dimensional Weisfeiler--Leman algorithm imply near-optimal lower bounds on the number of refinement iterations. A key component in our proof is the hardness condensation technique recently introduced by [Raz…
We establish the strictness of several set quantifier alternation hierarchies that are based on modal logic, evaluated on various classes of finite graphs. This extends to the modal setting a celebrated result of Matz, Schweikardt and Thomas (2002), which states that the analogous hierarchy of monadic second-order logic is strict. Thereby, the present paper settles a question raised by van Benthem (1983), revived by ten Cate (2006), and partially answered by Kuusisto (2008, 2015).
The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting q…
We study tree languages that can be defined in Δ_2 . These are tree languages definable by a first-order formula whose quantifier prefix is forall exists, and simultaneously by a first-order formula whose quantifier prefix is . For the quantifier free part we consider two signatures, either the descendant relation alone or together with the lexicographical order relation on nodes. We provide an effective characterization of tree and forest languages definable in Δ_2 . This characterization is in terms of algebraic equations. Over words, the class of word languages definable in Δ_2 forms a robu…
A new class of languages of infinite words is introduced, called the max-regular languages, extending the class of $ω$-regular languages. The class has two equivalent descriptions: in terms of automata (a type of deterministic counter automaton), and in terms of logic (weak monadic second-order logic with a bounding quantifier). Effective translations between the logic and automata are given.
We identify and highlight certain landmark results in Samson Abramsky's work which we believe are fundamental to current developments and future trends. In particular, we focus on the use of (i) topological duality methods to solve problems in logic and computer science; (ii) category theory and, more particularly, free (and co-free) constructions; (iii) these tools to unify the `power' and `structure' strands in computer science.
We discuss the definability of finite graphs in first-order logic with two relation symbols for adjacency and equality of vertices. The logical depth $D(G)$ of a graph $G$ is equal to the minimum quantifier depth of a sentence defining $G$ up to isomorphism. The logical width $W(G)$ is the minimum number of variables occurring in such a sentence. The logical length $L(G)$ is the length of a shortest defining sentence. We survey known estimates for these graph parameters and discuss their relations to other topics (such as the efficiency of the Weisfeiler-Lehman algorithm in isomorphism testing…
During the last decades, a lot of effort was put into identifying decidable fragments of first-order logic. Such efforts gave birth, among the others, to the two-variable fragment and the guarded fragment, depending on the type of restriction imposed on formulae from the language. Despite the success of the mentioned logics in areas like formal verification and knowledge representation, such first-order fragments are too weak to express even the simplest statistical constraints, required for modelling of influence networks or in statistical reasoning. In this work we investigate the extensions…
We define a semantics for first-order logic with generalized quantifiers based on double teams. We also define and investigate a notion of a generalized atom. Such atoms can be used in order to define extensions of first-order logic with a team-based semantics. We also define a game semantics and compare it with the double team semantics.
Given two structures $G$ and $H$ distinguishable in $\fo k$ (first-order logic with $k$ variables), let $A^k(G,H)$ denote the minimum alternation depth of a $\fo k$ formula distinguishing $G$ from $H$. Let $A^k(n)$ be the maximum value of $A^k(G,H)$ over $n$-element structures. We prove the strictness of the quantifier alternation hierarchy of $\fo 2$ in a strong quantitative form, namely $A^2(n)\ge n/8-2$, which is tight up to a constant factor. For each $k\ge2$, it holds that $A^k(n)>\log_{k+1}n-2$ even over colored trees, which is also tight up to a constant factor if $k\ge3$. For $k\ge 3$ …
Nominal logic is a variant of first-order logic that provides support for reasoning about bound names in abstract syntax. A key feature of nominal logic is the new-quantifier, which quantifies over fresh names (names not appearing in any values considered so far). Previous attempts have been made to develop convenient rules for reasoning with the new-quantifier, but we argue that none of these attempts is completely satisfactory. In this article we develop a new sequent calculus for nominal logic in which the rules for the new- quantifier are much simpler than in previous attempts. We also pro…
For relational monadic formulas (the Löwenheim class) second-order quantifier elimination, which is closely related to computation of uniform interpolants, projection and forgetting - operations that currently receive much attention in knowledge processing - always succeeds. The decidability proof for this class by Heinrich Behmann from 1922 explicitly proceeds by elimination with equivalence preserving formula rewriting. Here we reconstruct the results from Behmann's publication in detail and discuss related issues that are relevant in the context of modern approaches to second-order quantifi…
We contribute to the refined understanding of the language-logic-algebra interplay in the context of first-order properties of countable words. We establish decidable algebraic characterizations of one variable fragment of FO as well as boolean closure of existential fragment of FO via a strengthening of Simon's theorem about piecewise testable languages. We propose a new extension of FO which admits infinitary quantifiers to reason about the inherent infinitary properties of countable words. We provide a very natural and hierarchical block-product based characterization of the new extension. …
For every $q\in \mathbb N$ let $\textrm{FO}_q$ denote the class of sentences of first-order logic FO of quantifier rank at most $q$. If a graph property can be defined in $\textrm{FO}_q$, then it can be decided in time $O(n^q)$. Thus, minimizing $q$ has favorable algorithmic consequences. Many graph properties amount to the existence of a certain set of vertices of size $k$. Usually this can only be expressed by a sentence of quantifier rank at least $k$. We use the color-coding method to demonstrate that some (hyper)graph problems can be defined in $\textrm{FO}_q$ where $q$ is independent of …
This paper explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a de Morgan dual pair of nominal quantifiers. These nominal quantifiers called `new' and `wen' are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkeeping enables private names to be modelled in processes embedded as formulae in MAV1. Th…
We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically equivalent quantifier-free formula. The algorithm we formalize is a hybrid mixture of Tarski's original QE algorithm and the Ben-Or, Kozen, and Reif algorithm, and it is the first complete multivariate QE algorithm formalized in Isabelle/HOL.
Adding modular predicates yields a generalization of first-order logic FO over words. The expressive power of FO[<,MOD] with order comparison $x<y$ and predicates for $x \equiv i \mod n$ has been investigated by Barrington, Compton, Straubing and Therien. The study of FO[<,MOD]-fragments was initiated by Chaubard, Pin and Straubing. More recently, Dartois and Paperman showed that definability in the two-variable fragment FO2[<,MOD] is decidable. In this paper we continue this line of work. We give an effective algebraic characterization of the word languages in Sigma2[<,MOD]. The fragment Sigm…
This paper establishes model-theoretic properties of $\mathrm{FOE}^{\infty}$, a variation of monadic first-order logic that features the generalised quantifier $\exists^\infty$ (`there are infinitely many'). We provide syntactically defined fragments of $\mathrm{FOE}^{\infty}$ characterising four different semantic properties of $\mathrm{FOE}^{\infty}$-sentences: (1) being monotone and (2) (Scott) continuous in a given set of monadic predicates; (3) having truth preserved under taking submodels or (4) invariant under taking quotients. In each case, we produce an effectively defined map that tr…
We study the logic obtained by endowing the language of first-order arithmetic with second-order measure quantifiers. This new kind of quantification allows us to express that the argument formula is true in a certain portion of all possible interpretations of the quantified variable. We show that first-order arithmetic with measure quantifiers is capable of formalizing simple results from probability theory and, most importantly, of representing every recursive random function. Moreover, we introduce a realizability interpretation of this logic in which programs have access to an oracle from …
Metric Temporal Logic (MTL) and Timed Propositional Temporal Logic (TPTL) are prominent real-time extensions of Linear Temporal Logic (LTL). In general, the satisfiability checking problem for these extensions is undecidable when both the future U and the past S modalities are used. In a classical result, the satisfiability checking for MITL[U,S], a non punctual fragment of MTL[U,S], is shown to be decidable with EXPSPACE complete complexity. Given that this notion of non punctuality does not recover decidability in the case of TPTL[U,S], we propose a generalization of non punctuality called \…
We study the expressive power of fragments of inclusion logic under the so-called lax team semantics. The fragments are defined either by restricting the number of universal quantifiers or the arity of inclusion atoms in formulae. In case of universal quantifiers, the corresponding hierarchy collapses at the first level. Arity hierarchy is shown to be strict by relating the question to the study of arity hierarchies in fixed point logics.
It is well known that dependence logic captures the complexity class NP, and it has recently been shown that inclusion logic captures P on ordered models. These results demonstrate that team semantics offers interesting new possibilities for descriptive complexity theory. In order to properly understand the connection between team semantics and descriptive complexity, we introduce an extension D* of dependence logic that can define exactly all recursively enumerable classes of finite models. Thus D* provides an approach to computation alternative to Turing machines. The essential novel feature…
This paper studies a first-order expansion of a combination C+J of intuitionistic and classical propositional logic, which was studied by Humberstone (1979) and del Cerro and Herzig (1996), from a proof-theoretic viewpoint. While C+J has both classical and intuitionistic implications, our first-order expansion adds classical and intuitionistic universal quantifiers and one existential quantifier to C+J. This paper provides a multi-succedent sequent calculus G(FOC+J) for our combination of the first-order intuitionistic and classical logic. Our sequent calculus G(FOC+J) restricts contexts of th…
There are logics where necessity is defined by means of a given identity connective: $\squareφ:= φ\equiv\top$ ($\top$ is a tautology). On the other hand, in many standard modal logics the concept of propositional identity (PI) $φ\equivψ$ can be defined by strict equivalence (SE) $\square(φ\leftrightarrowψ)$. All these approaches to modality involve a principle that we call the Collapse Axiom (CA): "There is only one necessary proposition." In this paper, we consider a notion of PI which relies on the identity axioms of Suszko's non-Fregean logic $\mathit{SCI}$. Then $S3$ proves to be the small…
Separation Logic (SL) is a well-known assertion language used in Hoare-style modular proof systems for programs with dynamically allocated data structures. In this paper we investigate the fragment of first-order SL restricted to the Bernays-Schoenfinkel-Ramsey quantifier prefix $\exists^*\forall^*$, where the quantified variables range over the set of memory locations. When this set is uninterpreted (has no associated theory) the fragment is PSPACE-complete, which matches the complexity of the quantifier-free fragment. However, SL becomes undecidable when the quantifier prefix belongs to $\ex…
