Abstract Inquisitive modal logic, InqML, is a generalisation of standard Kripke-style modal logic. In its epistemic incarnation, it extends standard epistemic logic to capture not just the information that agents have, but also the questions that they are interested in. Technically, InqML fits within the family of logics based on team semantics. From a model-theoretic perspective, it takes us a step in the direction of monadic second-order logic, as inquisitive modal operators involve quantification over sets of worlds. We introduce and investigate the natural notion of bisimulation equivalence in the setting of InqML. We compare the expressiveness of InqML and first-order logic in the context of relational structures with two sorts, one for worlds and one for information states, and characterise inquisitive modal logic as the bisimulation invariant fragment of first-order logic over various natural classes of two-sorted structures.

Team semantics admits reasoning about large sets of data, modelled by sets of assignments (called teams), with first-order syntax. This leads to high expressive power and complexity, particularly in the presence of atomic dependency properties for such data sets. It is therefore interesting to explore fragments and variants of logic with team semantics that permit model-theoretic tools and algorithmic methods to control this explosion in expressive power and complexity. We combine here the study of team semantics with the notion of guarded logics, which are well-understood in the case of classical Tarski semantics, and known to strike a good balance between expressive power and algorithmic manageability. In fact there are two strains of guardedness for teams. Horizontal guardedness requires the individual assignments of the team to be guarded in the usual sense of guarded logics. Vertical guardedness, on the other hand, posits an additional (or definable) hypergraph structure on relational structures in order to interpret a constraint on the component-wise variability of assignments within teams. In this paper we investigate the horizontally guarded case. We study horizontally guarded logics for teams and appropriate notions of guarded team bisimulation. In particular, we establish characterisation theorems that relate invariance under guarded team bisimulation with guarded team logics, but also with logics under classical Tarski semantics.

We investigate multi-agent epistemic modal logic with common knowledge modalities for groups of agents and obtain van Benthem style model-theoretic characterisations, in terms of bisimulation invariance of classical first-order logic over the non-elementary classes of (finite or arbitrary) common knowledge Kripke frames. The fixpoint character of common knowledge modalities and the rôle that reachability and transitive closures play for the derived accessibility relations take our analysis beyond classical model-theoretic terrain and technically pose a novel challenge to the analysis of model-theoretic games. Over and above the more familiar locality-based techniques we exploit a specific structure theory for specially adapted Cayley groups: through the association of agents with sets of generators, all epistemic frames can be represented up to bisimilarity by suitable Cayley groups with specific acyclicity properties; these support a locality analysis at different levels of granularity as induced by distance measures w.r.t. various coalitions of agents.

Abstract We give a new, simplified and detailed account of the correspondence between levels of the Sherali–Adams relaxation of graph isomorphism and levels of pebble-game equivalence with counting (higher-dimensional Weisfeiler–Lehman colour refinement). The correspondence between basic colour refinement and fractional isomorphism, due to Tinhofer [22; 23] and Ramana, Scheinerman and Ullman [17], is re-interpreted as the base level of Sherali–Adams and generalised to higher levels in this sense by Atserias and Maneva [1] and Malkin [14], who prove that the two resulting hierarchies interleave. In carrying this analysis further, we here give (a) a precise characterisation of the level k Sherali–Adams relaxation in terms of a modified counting pebble game; (b) a variant of the Sherali–Adams levels that precisely match the k-pebble counting game; (c) a proof that the interleaving between these two hierarchies is strict. We also investigate the variation based on boolean arithmetic instead of real/rational arithmetic and obtain analogous correspondences and separations for plain k-pebble equivalence (without counting). Our results are driven by considerably simplified accounts of the underlying combinatorics and linear algebra.

We propose a novel construction of finite hypergraphs and relational structures that is based on reduced products with Cayley graphs of groupoids. The universal algebraic and combinatorial properties of groupoids are abstracted form the composition behaviour of partial injections and support a very natural approach to the construction of certain highly symmetric finite instances of hypergraphs and relational structures. The typical task of this kind asks for regular realisations of a locally specified overlap pattern between pieces (hyperedges, guarded substructures). We show that reduced products with groupoids provide a generic and versatile tool towards such constructions; they are explored in applications to the construction of finite hypergraph coverings, to finite model constructions for the guarded fragment, and to extension properties for partial isomorphisms of relational structures (in the sense of Hrushovski, Herwig, Lascar). To this end we construct groupoids whose Cayley graphs have large girth not just in the usual sense, but with respect to a discounted distance measure that contracts edges from the same sub-groupoid (colour) and only counts transitions between cosets (different colours), and show that their acyclicity properties guarantee corresponding degrees of acyclicity in reduced products.

We construct finite groups whose Cayley graphs have large girth even with respect to a discounted distance measure that contracts arbitrarily long sequences of edges from the same color class (subgroup), and only counts transitions between color classes (cosets). These groups are shown to be useful in the construction of finite bisimilar hypergraph covers that avoid any small cyclic configurations. We present two applications to the finite model theory of the guarded fragment: a strengthening of the known finite model property for GF and the characterization of GF as the guarded bisimulation invariant fragment of first-order logic in the sense of finite model theory.

Abstract We study first-order logic with two variables FO2 and establish a small substructure property. Similar to the small model property for FO2 we obtain an exponential size bound on embedded substructures, relative to a fixed surrounding structure that may be infinite. We apply this technique to analyse the satisfiability problem for FO2 under constraints that require several binary relations to be interpreted as equivalence relations. With a single equivalence relation, FO2 has the finite model property and is complete for non-deterministic exponential time, just as for plain FO2. With two equivalence relations, FO2 does not have the finite model property, but is shown to be decidable via a construction of regular models that admit finite descriptions even though they may necessarily be infinite. For three or more equivalence relations, FO2 is undecidable.

A well-established and fundamental insight in database theory is that negation (also known as complementation) tends to make queries difficult to process and difficult to reason about. Many basic problems are decidable and admit practical algorithms in the case of unions of conjunctive queries, but become difficult or even undecidable when queries are allowed to contain negation. Inspired by recent results in finite model theory, we consider a restricted form of negation, guarded negation . We introduce a fragment of SQL, called GN-SQL, as well as a fragment of Datalog with stratified negation, called GN-Datalog, that allow only guarded negation, and we show that these query languages are computationally well behaved, in terms of testing query containment, query evaluation, open-world query answering, and boundedness. GN-SQL and GN-Datalog subsume a number of well known query languages and constraint languages, such as unions of conjunctive queries, monadic Datalog, and frontier-guarded tgds. In addition, an analysis of standard benchmark workloads shows that many uses of negation in SQL in practice are guarded.

Evaluating a boolean conjunctive query q over a guarded first-order theory T is equivalent to checking whether (T \& not q) is unsatisfiable. This problem is relevant to the areas of database theory and description logic. Since q may not be guarded, well known results about the decidability, complexity, and finite-model property of the guarded fragment do not obviously carry over to conjunctive query answering over guarded theories, and had been left open in general. By investigating finite guarded bisimilar covers of hypergraphs and relational structures, and by substantially generalising Rosati's finite chase, we prove for guarded theories T and (unions of) conjunctive queries q that (i) T implies q iff T implies q over finite models, that is, iff q is true in each finite model of T and (ii) determining whether T implies q is {2EXPTIME}-complete. We further show the following results: (iii) the existence of polynomial-size conformal covers of arbitrary hypergraphs; (iv) a new proof of the finite model property of the clique-guarded fragment; (v) the small model property of the guarded fragment with optimal bounds; (vi) a polynomial-time solution to the canonisation problem modulo guarded bisimulation, which yields (vii) a capturing result for guarded-bisimulation-invariant PTIME.

We construct finite groups whose Cayley graphs have large girth even w.r.t. a discounted distance measure that contracts arbitrarily long sequences of edges from the same colour class, and only counts transitions between colour classes. These groups are shown to be useful in the construction of finite bisimilar hypergraph covers that avoid any small cyclic configurations. We present two applications to the finite model theory of the guarded fragment: a strengthening of the known finite model property for GF and the characterisation of GF as the guarded bisimulation invariant fragment of FO in the sense of finite model theory.

We consider the monadic boundedness problem for least fixed points over FO formulae as a decision problem: Given a formula phi(X, x), positive in X, decide whether there is a uniform finite bound on the least fixed point recursion based on phi. Few fragments of FO are known to have a decidable boundedness problem; boundedness is known to be undecidable for many fragments. We here show that monadic boundedness is decidable for purely universal FO formulae without equality in which each non-recursive predicate occurs in just one polarity (e.g., only negatively). The restrictions are shown to be essential: waving either the polarity constraint or allowing positive occurrences of equality, the monadic boundedness problem for universal formulae becomes undecidable. The main result is based on a model theoretic analysis involving ideas from modal and guarded logics and a reduction to the monadic second-order theory of trees

We investigate model theoretic characterisations of the expressive power of modal logics in terms of bisimulation invariance. The paradigmatic result of this kind is van Benthem's theorem, which says that a first-order formula is invariant under bisimulation if and only if it is equivalent to a formula of basic modal logic. The present investigation primarily concerns ramifications for specific classes of structures. We study in particular model classes defined through conditions on the underlying frames, with a focus on frame classes that play a major role in modal correspondence theory and often correspond to typical application domains of modal logics. Classical model theoretic arguments do not apply to many of the most interesting classes -for instance, rooted connected frames, well-founded frames, finite rooted connected frames, finite transitive frames, finite equivalence frames - as these are not elementary. Instead we develop and extend the game-based analysis (first-order Ehrenfeucht-Fraisse versus bisimulation games) over such classes and provide bisimulation preserving model constructions within these classes.

We study first-order logic with two variables FO/sup 2/ and establish a small substructure property. Similar to the small model property for FO/sup 2/ we obtain an exponential size bound on embedded substructures, relative to a fixed surrounding structure that may be infinite. We apply this technique to analyse the satisfiability problem for FO/sup 2/ under constraints that require several binary relations to be interpreted as equivalence relations. With a single equivalence relation, FO/sup 2/ has the finite model property and is complete for non-deterministic exponential time, just as for plain FO/sup 2/. With two equivalence relations, FO/sup 2/ does not have the finite model property, but is shown to be decidable via a construction of regular models that admit finite descriptions even though they may necessarily be infinite. For three or more equivalence relations, FO/sup 2/ is undecidable.

Characterisation theorems for modal and guarded fragments of first-order logic are explored over finite transition systems. We show that the classical characterisations in terms of semantic invariance under the appropriate forms of bisimulation equivalence can be recovered at the level of finite model theory. The new, more constructive proofs naturally extend to alternative proofs of the classical variants. The finite model theory version of van Benthem's characterisation of basic modal logic is due to E. Rosen. That proof is simplified and the result slightly strengthened in terms of quantitative bounds. The main theme, however is a uniform treatment that extends to incorporate universal and inverse modalities and guarded quantification over transition systems. Technically, the present treatment exploits first-order locality in the context of a new finitary construction of locally acyclic bisimilar covers. These serve as graded finite analogues of tree unravellings, giving local control over first-order logic infinite bisimilar companion structures.

Guarded fixed-point logic μGF extends the guarded fragment by means of least and greatest fixed points, and thus plays the same role within the domain of guarded logics as the modal μ-calculus plays within the modal domain. We provide a semantic characterization of μGF within an appropriate fragment of second-order logic, in terms of invariance under guarded bisimulation. The corresponding characterization of the modal μ-calculus, due to Janin and Walukiewicz, is lifted from the modal to the guarded domain by means of model theoretic translations. Guarded second-order logic, the fragment of second-order logic which is introduced in the context of our characterization theorem, captures a natural and robust level of expressiveness with several equivalent characterizations. For a wide range of issues in guarded logics it may take up a role similar to that of monadic second-order in relation to modal logics. At the more general methodological level, the translations between the guarded and modal domains make the intuitive analogy between guarded and modal logics available as a tool in the further analysis of the model theory of guarded logics.

Abstract The satisfiability problem for the two-variable fragment of first-order logic is investigated over finite and infinite linearly ordered, respectively wellordered domains, as well as over finite and infinite domains in which one or several designated binary predicates are interpreted as arbitrary wellfounded relations. It is shown that FO2 over ordered, respectively wellordered. domains or in the presence of one well-founded relation, is decidable for satisfiability as well as for finite satisfiability. Actually the complexity of these decision problems is essentially the same as for plain unconstrained FO2. namely non-deterministic exponential time. In contrast FO2 becomes undecidable for satisfiability and for finite satisfiability, if a sufficiently large number of predicates are required to be interpreted as orderings. wellorderings. or as arbitrary wellfounded relations. This undecidability result also entails the undecidability of the natural common extension of FO2 and computation tree logic CTL.

Guarded fixed point logic /spl mu/GF extends the guarded fragment by means of least and greatest fixed points, and thus plays the same role within the domain of guarded logics as the modal /spl mu/-calculus plays within the modal domain. We provide a semantic characterisation of /spl mu/GF within an appropriate fragment of second-order logic, in terms of invariance under guarded bisimulation. The corresponding characterisation of the modal /spl mu/-calculus, due to D. Janin and I. Walukiewicz (1999), is lifted from the modal to the guarded domain by means of model theoretic translations. At the methodological level, these translations make the intuitive analogy between modal and guarded logics available as a tool in the analysis of the guarded domain.

Abstract There are properties of finite structures that are expressible with the use of Hilbert's ∈-operator in a manner that does not depend on the actual interpretation for ∈-terms. but not expressible in plain first-order. This observation strengthens a corresponding result of Gurevich, concerning the invariant use of an auxiliary ordering in first-order logic over finite structures. The present result also implies that certain non-deterministic choice constructs, which have been considered in database theory, properly enhance the expressive power of first-order logic even as far as deterministic queries are concerned, thereby answering a question raised by Abiteboul and Vianu.

A positive first-order formula is bounded if the sequence of its stages converges to the least fixed point of the formula within a fixed finite number of steps independent of the input structure. The boundedness problem for a fragment C of first-order logic is the following decision problem: given a positive formula in L, is it bounded? In this paper, we investigate the boundedness problem for two-variable first-order logic FO/sup 2/. As a general rule, FO/sup 2/ is a well-behaved fragment of first-order logic, since it possesses the finite-model property and has a decidable satisfiability problem. Nonetheless, our main result asserts that the boundedness problem for FO/sup 2/ is undecidable, even when restricted to negation-free and equality-free formulas /spl phi/(X, x) in which x is the only free variable and X is a monadic relation symbol that occurs within the scopes of universal quantifiers only. This undecidability result contrasts sharply with earlier results asserting the decidability of boundedness for monadic Datalog programs, which amounts to the decidability of boundedness for negation-free and equality-free existential first-order formulas /spl psi/(X, x) in which x is the only free variable and X is a monadic relation symbol. We demonstrate that our main result has certain applications to circumscription, the most well-developed formalism of nonmonotonic reasoning. Specifically, using the undecidability of boundedness for FO/sup 2/, we show that it is an undecidable problem to tell whether the circumscription of a given FO/sup 2/-formula is equivalent to a first-order formula. In contrast, the circumscription of every FO/sup 1/-formula is equivalent to a first-order formula.

We prove that the satisfiability and the finite satisfiability problems for C/sup 2/ are decidable. C/sup 2/ is first-order logic with only two variables in the presence of arbitrary counting quantifiers 3/sup /spl ges/m/,m/spl ges/1. It considerably extends L/sup 2/ plain first-order with only two variables, which is known to be decidable by a result of Mortimer's. Unlike L/sup 2/, C/sup 2/ does not have the finite model property.

Abstract We study the expressive power in the finite of the logic Fixed-Point+Counting, the extension of first-order logic which is obtained through adding both the fixed-point constructor and the ability to count. To this end an isomorphism preserving (‘generic’) model of computation is introduced whose PTime restriction exactly corresponds to this level of expressive power, while its PSpace restriction corresponds to While+Counting. From this model we obtain a normal form which shows a rather clear separation of the relational vs. the arithmetical side of the algorithms involved. In parallel, we study the relations of Fixed-Point+Counting with the infinitary logics and the corresponding pebble games. The main result, however, involves the concept of anarithmetical invariant. By this we mean a functor taking every finite relational structure to an expansion of (an initial segment of) the standard arithmetical structure. In particular its values are linearly ordered structures. We establish the existence of a family of arithmetical invariants with the following properties: • The invariants themselves can be evaluated in polynomial time. • A class of finite relational structures is definable in Fixed-Point+Counting if and only if membership can be decided in polynomial time on the basis of the values of one of the invariants. • The invariant rclassifies all finite relational structures exactly up to equivalence with respect to the logic We also give a characterization of Fixed-Point+Counting in terms of sequences of formulae in the : It corresponds exactly to the polynomial time computable families (φn)n∈ωin these logics. Towards a positive assessment of the expressive power of Fixed-Point+Counting, it is shown that the natural extension of fixed-point logic by Lindström quantifiers, which capture all the PTime computable properties of cardinalities of definable predicates, is strictly weaker than what we get here. This implies in particular that every extension of fixed-point logic by means of monadic Lindström quantifiers, which stays within PTime, must be strictly contained in Fixed-Point+Counting.

We consider infinitary logic with two variable symbols and counting quantifiers, C/sup 2/, and its intersection with PTIME on finite relational structures. In particular we exhibit a PTIME canonization procedure for finite relational structures which provides unique representatives up to equivalence in C/sup 2/. As a consequence we obtain a recursive presentation for the class of all those queries on arbitrary finite relational structures which are both PTIME and definable in C/sup 2/. The proof renders a succinct normal form representation of this non-trivial semantically defined fragment of PTIME. Through specializations of the proof techniques similar results apply with respect to the logic L/sup 2/, infinitary logic with two variable symbols, itself.

We consider extensions of fixed-point logic by means of generalized quantifiers in the context of descriptive complexity. By the well-known theorem of N. Immerman and M. Vardi, fixed-point logic captures PTime over linearly ordered structures. It fails, however, to express even most fundamental structural properties, like simple cardinality properties, in the absence of order. We concentrate on extensions by generalized quantifiers which serve to adjoin simple or basic structural properties. An abstract notion of simplicity is put forward which isolates those structural properties, that can be characterized in terms of a concise structural invariant. The key examples are provided by all monadic and cardinality properties in a very general sense. The main theorem establishes that no extension by any family of such simple quantifiers can cover all of PTime. These limitations are proved on the basis of the semantically motivated notion of simplicity; in particular there is no implicit bound on the arities of the generalized quantifiers involved. Quite to the contrary, the natural applications concern infinite families of quantifiers adjoining certain structural properties across all arities in a uniform way.>

Abstract By means of an Ehrenfeucht-Mostowski construction we obtain an automorphism theorem for a syntactically characterized class of Laa-theories comprising in particular the finitely determinate ones. Examples of Laa-theories with only rigid models show this result to be optimal with respect to a classification in terms of prenex quantifier type: Rigidity is seen to hinge on quantification of type … ∀ … stat … permitting of the parametrization of families of disjoint stationary systems by the elements of the universe.