Author name cluster

Anuj Dawar

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

35 papers

2 author rows

CSL Conference 2026 Conference Paper

Arity Hierarchies for Quantifiers Closed Under Partial Polymorphisms

Anuj Dawar
Lauri Hella
Benedikt Pago

We investigate the expressive power of generalized quantifiers closed under partial polymorphism conditions motivated by the study of constraint satisfaction problems. We answer a number of questions arising from the work of Dawar and Hella (CSL 2024) where such quantifiers were introduced. For quantifiers closed under partial near-unanimity polymorphisms, we establish hierarchy results clarifying the interplay between the arity of the polymorphisms and of the quantifiers: The expressive power of (𝓁+1)-ary quantifiers closed under 𝓁-ary partial near-unanimity polymorphisms is strictly between the class of all quantifiers of arity 𝓁-1 and 𝓁. We also establish an infinite hierarchy based on the arity of quantifiers with a fixed arity of partial near-unanimity polymorphisms. Finally, we prove inexpressiveness results for quantifiers with a partial Maltsev polymorphism. The separation results are proved using novel algebraic constructions in the style of Cai-Fürer-Immerman and the quantifier pebble games of Dawar and Hella (2024).

CSL Conference 2026 Conference Paper

Compactness in Semiring Semantics

Sophie Brinke
Anuj Dawar
Erich Grädel
Lovro Mrkonjic
Matthias Naaf

Semiring provenance was originally introduced in database theory with the aim of explaining why certain tuples are (not) contained in the answer of a query. To this end, logical statements are not just evaluated to true or false but to values in a commutative semiring. Depending on the underlying semiring, this allows us to track descriptions of the atomic facts that are responsible for the truth of a statement or practical information about the evaluation such as costs or confidence. Recently, this approach has been expanded to a systematic study of semiring semantics for first-order logic and other logical systems. This raises the question to what extent model-theoretic results can be generalised to semiring semantics and how this relates to the algebraic properties of the underlying semiring. Here we investigate the availability of compactness in semiring semantics. The appropriate setting for this is based on absorptive semirings with well-defined infinitary products. Compactness can be stated either in terms of satisfiability or in terms of entailment, and these two variants are trivially equivalent in Boolean semantics. However, this is no longer the case in semiring semantics. Compactness in terms of satisfiability, defined as the existence of non-zero valuations, indeed generalises to every infinitary absorptive semiring. For compactness in terms of entailment the situation is different. The entailment relation naturally extends to semiring semantics (via the natural order on the semiring) but this yields a stronger variant of compactness, which fails for certain important semirings, including the tropical semiring and the Łukasiewicz semiring. Our main positive results show that strong compactness does indeed hold for all finite semirings and all lattice semirings.

MFCS Conference 2025 Conference Paper

Symmetric Proofs in the Ideal Proof System

Anuj Dawar
Erich Grädel
Leon Kullmann
Benedikt Pago

We consider the Ideal Proof System (IPS) introduced by Grochow and Pitassi and pose the question of which tautologies admit symmetric proofs, and of what complexity. The symmetry requirement in proofs is inspired by recent work establishing lower bounds in other symmetric models of computation. We link the existence of symmetric IPS proofs to the expressive power of logics such as fixed-point logic with counting and Choiceless Polynomial Time, specifically regarding the graph isomorphism problem. We identify relationships and tradeoffs between the symmetry of proofs and other parameters of IPS proofs such as size, degree and linearity. We study these on a number of standard families of tautologies from proof complexity and finite model theory such as the pigeonhole principle, the subset sum problem and the Cai-Fürer-Immerman graphs, exhibiting non-trivial upper bounds on the size of symmetric IPS proofs.

CSL Conference 2025 Conference Paper

Undefinability of Approximation of 2-To-2 Games

Anuj Dawar
Bálint Molnár

Recent work by Atserias and Dawar [Albert Atserias and Anuj Dawar, 2019] and Tucker-Foltz [Jamie Tucker-Foltz, 2024] has established undefinability results in fixed-point logic with counting (FPC) corresponding to many classical complexity results from the hardness of approximation. In this line of work, NP-hardness results are turned into unconditional FPC undefinability results. We extend this work by showing the FPC undefinability of any constant factor approximation of weighted 2-to-2 games, based on the NP-hardness results of Khot, Minzer and Safra. Our result shows that the completely satisfiable 2-to-2 games are not FPC-separable from those that are not ε-satisfiable, for arbitrarily small ε. The perfect completeness of our inseparability is an improvement on the complexity result, as the NP-hardness of such a separation is still only conjectured. This perfect completeness enables us to show the FPC undefinability of other problems whose NP-hardness is conjectured. In particular, we are able to show that no FPC formula can separate the 3-colourable graphs from those that are not t-colourable, for any constant t.

MFCS Conference 2024 Conference Paper

Preservation Theorems on Sparse Classes Revisited

Anuj Dawar
Ioannis Eleftheriadis

We revisit the work studying homomorphism preservation for first-order logic in sparse classes of structures initiated in [Atserias et al. , JACM 2006] and [Dawar, JCSS 2010]. These established that first-order logic has the homomorphism preservation property in any sparse class that is monotone and addable. It turns out that the assumption of addability is not strong enough for the proofs given. We demonstrate this by constructing classes of graphs of bounded treewidth which are monotone and addable but fail to have homomorphism preservation. We also show that homomorphism preservation fails on the class of planar graphs. On the other hand, the proofs of homomorphism preservation can be recovered by replacing addability by a stronger condition of amalgamation over bottlenecks. This is analogous to a similar condition formulated for extension preservation in [Atserias et al. , SiCOMP 2008].

CSL Conference 2024 Conference Paper

Quantifiers Closed Under Partial Polymorphisms

Anuj Dawar
Lauri Hella

We study Lindström quantifiers that satisfy certain closure properties which are motivated by the study of polymorphisms in the context of constraint satisfaction problems (CSP). When the algebra of polymorphisms of a finite structure 𝔅 satisfies certain equations, this gives rise to a natural closure condition on the class of structures that map homomorphically to 𝔅. The collection of quantifiers that satisfy closure conditions arising from a fixed set of equations are rather more general than those arising as CSP. For any such conditions 𝒫, we define a pebble game that delimits the distinguishing power of the infinitary logic with all quantifiers that are 𝒫-closed. We use the pebble game to show that the problem of deciding whether a system of linear equations is solvable in ℤ / 2ℤ is not expressible in the infinitary logic with all quantifiers closed under a near-unanimity condition.

CSL Conference 2022 Conference Paper

MSO Undecidability for Hereditary Classes of Unbounded Clique Width

Anuj Dawar
Abhisekh Sankaran

Seese’s conjecture for finite graphs states that monadic second-order logic (MSO) is undecidable on all graph classes of unbounded clique-width. We show that to establish this it would suffice to show that grids of unbounded size can be interpreted in two families of graph classes: minimal hereditary classes of unbounded clique-width; and antichains of unbounded clique-width under the induced subgraph relation. We explore all the currently known classes of the former category and establish that grids of unbounded size can indeed be interpreted in them.

CSL Conference 2021 Conference Paper

Extension Preservation in the Finite and Prefix Classes of First Order Logic

Anuj Dawar
Abhisekh Sankaran

It is well known that the classic Łoś-Tarski preservation theorem fails in the finite: there are first-order definable classes of finite structures closed under extensions which are not definable (in the finite) in the existential fragment of first-order logic. We strengthen this by constructing for every n, first-order definable classes of finite structures closed under extensions which are not definable with n quantifier alternations. The classes we construct are definable in the extension of Datalog with negation and indeed in the existential fragment of transitive-closure logic. This answers negatively an open question posed by Rosen and Weinstein.

CSL Conference 2021 Conference Paper

Game Comonads & Generalised Quantifiers

Adam Ó Conghaile
Anuj Dawar

Game comonads, introduced by Abramsky, Dawar and Wang and developed by Abramsky and Shah, give an interesting categorical semantics to some Spoiler-Duplicator games that are common in finite model theory. In particular they expose connections between one-sided and two-sided games, and parameters such as treewidth and treedepth and corresponding notions of decomposition. In the present paper, we expand the realm of game comonads to logics with generalised quantifiers. In particular, we introduce a comonad graded by two parameter n ≤ k such that isomorphisms in the resulting Kleisli category are exactly Duplicator winning strategies in Hella’s n-bijection game with k pebbles. We define a one-sided version of this game which allows us to provide a categorical semantics for a number of logics with generalised quantifiers. We also give a novel notion of tree decomposition that emerges from the construction.

MFCS Conference 2021 Conference Paper

On the Relative Power of Linear Algebraic Approximations of Graph Isomorphism

Anuj Dawar
Danny Vagnozzi

We compare the capabilities of two approaches to approximating graph isomorphism using linear algebraic methods: the invertible map tests (introduced by Dawar and Holm) and proof systems with algebraic rules, namely polynomial calculus, monomial calculus and Nullstellensatz calculus. In the case of fields of characteristic zero, these variants are all essentially equivalent to the Weisfeiler-Leman algorithms. In positive characteristic we show that the distinguishing power of the monomial calculus is no greater than the invertible map method by simulating the former in a fixed-point logic with solvability operators. In turn, we show that the distinctions made by this logic can be implemented in the Nullstellensatz calculus.

CSL Conference 2020 Conference Paper

Symmetric Computation (Invited Talk)

Anuj Dawar

We discuss a recent convergence of notions of symmetric computation arising in the theory of linear programming, in logic and in circuit complexity. This leads us to a coherent and robust definition of problems that are efficiently and symmetrically solvable. This is at once a rich class of problems and one for which we have methods for proving lower bounds. In this paper, we take a tour through results which show applications of these methods in a number of areas.

CSL Conference 2018 Conference Paper

Definable Inapproximability: New Challenges for Duplicator

Albert Atserias
Anuj Dawar

We consider the hardness of approximation of optimization problems from the point of view of definability. For many NP-hard optimization problems it is known that, unless P = NP, no polynomial-time algorithm can give an approximate solution guaranteed to be within a fixed constant factor of the optimum. We show, in several such instances and without any complexity theoretic assumption, that no algorithm that is expressible in fixed-point logic with counting (FPC) can compute an approximate solution. Since important algorithmic techniques for approximation algorithms (such as linear or semidefinite programming) are expressible in FPC, this yields lower bounds on what can be achieved by such methods. The results are established by showing lower bounds on the number of variables required in first-order logic with counting to separate instances with a high optimum from those with a low optimum for fixed-size instances.

CSL Conference 2018 Conference Paper

Symmetric Circuits for Rank Logic

Anuj Dawar
Gregory Wilsenach

Fixed-point logic with rank (FPR) is an extension of fixed-point logic with counting (FPC) with operators for computing the rank of a matrix over a finite field. The expressive power of FPR properly extends that of FPC and is contained in P, but it is not known if that containment is proper. We give a circuit characterization for FPR in terms of families of symmetric circuits with rank gates, along the lines of that for FPC given by [Anderson and Dawar 2017]. This requires the development of a broad framework of circuits in which the individual gates compute functions that are not symmetric (i. e. , invariant under all permutations of their inputs). This framework also necessitates the development of novel techniques to prove the equivalence of circuits and logic. Both the framework and the techniques are of greater generality than the main result.

CSL Conference 2017 Conference Paper

The Ackermann Award 2017

Anuj Dawar
Daniel Leivant

The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2017 edition of the award.

CSL Conference 2016 Conference Paper

The Ackermann Award 2016

Thierry Coquand
Anuj Dawar

The Ackermann Award is the EACSL Outstanding Dissertation Award for Logic in Computer Science. It is presented during the annual conference of the EACSL (CSL'xx). This contribution reports on the 2016 edition of the award.

CSL Conference 2015 Conference Paper

A Definability Dichotomy for Finite Valued CSPs

Anuj Dawar
Pengming Wang 0001

Finite valued constraint satisfaction problems are a formalism for describing many natural optimisation problems, where constraints on the values that variables can take come with rational weights and the aim is to find an assignment of minimal cost. Thapper and Zivny have recently established a complexity dichotomy for valued constraint languages. They show that each such languages either gives rise to a polynomial-time solvable optimisation problem, or to an NP-hard one, and establish a criterion to distinguish the two cases. We refine the dichotomy by showing that all optimisation problems in the first class are definable in fixed-point language with counting, while all languages in the second class are not definable, even in infinitary logic with counting. Our definability dichotomy is not conditional on any complexity-theoretic assumption.

CSL Conference 2015 Conference Paper

The Ackermann Award 2015

Anuj Dawar
Dexter Kozen
Simona Ronchi Della Rocca

The eleventh Ackermann Award is presented at CSL'15 in Berlin, Germany. This year, again, the EACSL Ackermann Award is generously sponsored by the Kurt Gödel Society. Besides providing financial support for the Ackermann Award, the Kurt Gödel Society has also committed to inviting the recipients of the Award for a special lecture to be given to the Society in Vienna.

Highlights Conference 2013 Conference Abstract

On symmetric circuits and FPC

Matthew Anderson
Anuj Dawar

We study queries on graphs (and other relational structures) defined by families of Boolean circuits that are invariant under permutations of the vertices. In particular, we study circuits that are symmetric, that is, circuits whose invariance is explicitly witnessed by automorphisms of the circuit induced by the permutation of their inputs. We show a close connection between queries defined on structures by uniform families of symmetric circuits and definability in fixed-point logics.

CSL Conference 2013 Conference Paper

The Ackermann Award 2013

Anuj Dawar
Thomas A. Henzinger
Damian Niwinski

Report on the Ackermann Award 2013.

CSL Conference 2012 Conference Paper

Definability of linear equation systems over groups and rings

Anuj Dawar
Erich Grädel
Bjarki Holm
Eryk Kopczynski
Wied Pakusa

Motivated by the quest for a logic for PTIME and recent insights that the descriptive complexity of problems from linear algebra is a crucial aspect of this problem, we study the solvability of linear equation systems over finite groups and rings from the viewpoint of logical (inter-)definability. All problems that we consider are decidable in polynomial time, but not expressible in fixed-point logic with counting. They also provide natural candidates for a separation of polynomial time from rank logics, which extend fixed-point logics by operators for determining the rank of definable matrices and which are sufficient for solvability problems over fields. Based on the structure theory of finite rings, we establish logical reductions among various solvability problems. Our results indicate that all solvability problems for linear equation systems that separate fixed-point logic with counting from PTIME can be reduced to solvability over commutative rings. Further, we prove closure properties for classes of queries that reduce to solvability over rings. As an application, these closure properties provide normal forms for logics extended with solvability operators.

CSL Conference 2012 Conference Paper

The Ackermann Award 2012

Thierry Coquand
Anuj Dawar
Damian Niwinski

Report on the Ackermann Award 2012.

TCS Journal 2009 Journal Article

Affine systems of equations and counting infinitary logic

Albert Atserias
Andrei Bulatov
Anuj Dawar

We study the definability of constraint satisfaction problems (CSPs) in various fixed-point and infinitary logics. We show that testing the solvability of systems of equations over a finite Abelian group, a tractable CSP that was previously known not to be definable in Datalog, is not definable in the infinitary logic with finitely many variables and counting. This implies that it is not definable in least fixed-point logic or its extension with counting. We relate definability of CSPs to their classification obtained from tame congruence theory of the varieties generated by the algebra of polymorphisms of the template structure. In particular, we show that if this variety admits either the unary or affine type, the corresponding CSP is not definable in the infinitary logic with counting.

MFCS Conference 2009 Conference Paper

Parameterized Complexity Classes under Logical Reductions

Anuj Dawar
Yuguo He

Abstract The parameterized complexity classes of the W -hierarchy are usually defined as the problems reducible to certain natural complete problems by means of fixed-parameter tractable ( fpt ) reductions. We investigate whether the classes can be characterised by means of weaker, logical reductions. We show that each class W [ t ] has complete problems under slicewise bounded-variable first-order reductions. These are a natural weakening of slicewise bounded-variable LFP reductions which, by a result of Flum and Grohe, are known to be equivalent to fpt -reductions. If we relax the restriction on having a bounded number of variables, we obtain reductions that are too strong and, on the other hand, if we consider slicewise quantifier-free first-order reductions, they are considerably weaker. These last two results are established by considering the characterisation of W [ t ] as the closure of a class of Fagin-definability problems under fpt -reductions. We show that replacing these by slicewise first-order reductions yields a hierarchy that collapses, while allowing only quantifier-free first-order reductions yields a hierarchy that is provably strict.

CSL Conference 2008 Conference Paper

The Descriptive Complexity of Parity Games

Anuj Dawar
Erich Grädel

Abstract We study the logical definablity of the winning regions of parity games. For games with a bounded number of priorities, it is well-known that the winning regions are definable in the modal μ -calculus. Here we investigate the case of an unbounded number of priorities, both for finite game graphs and for arbitrary ones. In the general case, winning regions are definable in guarded second-order logic (GSO), but not in least-fixed point logic (LFP). On finite game graphs, winning regions are LFP-definable if, and only if, they are computable in polynomial time, and this result extends to any class of finite games that is closed under taking bisimulation quotients.

I&C Journal 2007 Journal Article

Expressiveness and complexity of graph logic

Anuj Dawar
Philippa Gardner
Giorgio Ghelli

We investigate the complexity and expressive power of a spatial logic for reasoning about graphs. This logic was previously introduced by Cardelli, Gardner and Ghelli, and provides the simplest setting in which to explore such results for spatial logics. We study several forms of the logic: the logic with and without recursion, and with either an exponential or a linear version of the basic composition operator. We study the combined complexity and the expressive power of the four combinations. We prove that, without recursion, the linear and exponential versions of the logic correspond to significant fragments of first-order (FO) and monadic second-order (MSO) Logics; the two versions are actually equivalent to FO and MSO on graphs representing strings. However, when the two versions are enriched with μ-style recursion, their expressive power is sharply increased. Both are able to express PSPACE-complete problems, although their combined complexity and data complexity still belong to PSPACE.

MFCS Conference 2007 Invited Paper

Finite Model Theory on Tame Classes of Structures

Anuj Dawar

Abstract The early days of finite model theory saw a variety of results establishing that the model theory of the class of finite structures is not well-behaved. Recent work has shown that considering subclasses of the class of finite structures allows us to recover some good model-theoretic behaviour. This appears to be especially true of some classes that are known to be algorithmically well-behaved. We review some results in this area and explore the connection between logic and algorithms.

TCS Journal 2007 Journal Article

Generalising automaticity to modal properties of finite structures

Anuj Dawar
Stephan Kreutzer

We introduce a complexity measure of modal properties of finite structures which generalises the automaticity of languages. It is based on graph-automata-like devices called labelling systems. We define a measure of the size of a structure that we call rank, and show that any modal property of structures can be approximated up to any fixed rank n by a labelling system. The function that takes n to the size of the smallest labelling system doing this is called the labelling index of the property. We demonstrate that this is a useful and fine-grained measure of complexity and show that it is especially well suited to characterise the expressive power of modal fixed-point logics. From this we derive several separation results of modal and non-modal fixed-point logics, some of which are already known whereas others are new.

CSL Conference 2007 Invited Paper

Model-Checking First-Order Logic: Automata and Locality

Anuj Dawar

Abstract The satisfaction problem for first-order logic, namely to decide, given a finite structure \(\mathbb{A}\) and a first-order formula φ, whether or not \(\mathbb{A} \models \phi\) is known to be PSpace -complete. In terms of parameterized complexity, where the length of φ is taken as the parameter, the problem is AW [ ⋆ ]-complete and therefore not expected to be fixed-parameter tractable ( FPT ). Nonetheless, the problem is known to be FPT when we place some structural restrictions on A. For some restrictions, such as when we place a bound on the treewidth of \(\mathbb{A}\), the result is obtained as a corollary of the fact that the satisfaction problem for monadic second-order logic ( MSO ) is FPT in the presence of such restriction [1]. This fact is proved using automata-based methods. In other cases, such as when we bound the degree of \(\mathbb{A}\), the result is obtained using methods based on the locality of first-order logic (see [3]) and does not extend to MSO. We survey such fixed-parameter tractability results, including the recent [2] and explore the relationship between methods based on automata, locality and decompositions.

CSL Conference 2007 Conference Paper

The Power of Counting Logics on Restricted Classes of Finite Structures

Anuj Dawar
David Richerby

Abstract Although Cai, Fürer and Immerman have shown that fixed-point logic with counting (IFP+C) does not express all polynomial-time properties of finite structures, there have been a number of results demonstrating that the logic does capture P on specific classes of structures. Grohe and Mariño showed that IFP+C captures P on classes of structures of bounded treewidth, and Grohe showed that IFP+C captures P on planar graphs. We show that the first of these results is optimal in two senses. We show that on the class of graphs defined by a non-constant bound on the tree-width of the graph, IFP+C fails to capture P. We also show that on the class of graphs whose local tree-width is bounded by a non-constant function, IFP+C fails to capture P. Both these results are obtained by an analysis of the Cai–Fürer–Immerman (CFI) construction in terms of the treewidth of graphs, and cops and robber games; we present some other implications of this analysis. We then demonstrate the limits of this method by showing that the CFI construction cannot be used to show that IFP+C fails to capture P on proper minor-closed classes.

TCS Journal 2006 Journal Article

Backtracking games and inflationary fixed points

Anuj Dawar
Erich Grädel
Stephan Kreutzer

We define a new class of games, called backtracking games. Backtracking games are essentially parity games with an additional rule allowing players, under certain conditions, to return to an earlier position in the play and revise a choice or to force a countback of the number of moves. This new feature makes backtracking games more powerful than parity games. As a consequence, winning strategies become more complex objects and computationally harder. The corresponding increase in expressiveness allows us to use backtracking games as model-checking games for inflationary fixed-point logics such as IFP or MIC. We identify a natural subclass of backtracking games, the simple games, and show that these are the “right” model-checking games for IFP by (a) giving a translation of formulae φ and structures A into simple games such that A ⊨ φ if, and only if, Player 0 wins the corresponding game and (b) showing that the winner of simple backtracking games can again be defined in IFP.

MFCS Conference 2005 Conference Paper

Complexity Bounds for Regular Games

Paul Hunter 0001
Anuj Dawar

Abstract We consider the complexity of infinite games played on finite graphs. We establish a framework in which the expressiveness and succinctness of different types of winning conditions can be compared. We show that the problem of deciding the winner in Muller games is PSPACE-complete. This is then used to establish PSPACE-completeness for Emerson-Lei games and for games described by Zielonka DAGs. Adaptations of the proof show PSPACE-completeness for the emptiness problem for Muller automata as well as the model-checking problem for such automata on regular trees. We also show co-NP-completeness for two classes of union-closed games: games specified by a basis and superset Muller games.

CSL Conference 2003 Conference Paper

A Fixed-Point Logic with Symmetric Choice

Anuj Dawar
David Richerby

Abstract Gire and Hoang introduce a fixed-point logic with a ‘symmetric’ choice operator that makes a nondeterministic choice from a definable set of tuples at each stage in the inductive construction of a relation, as long as the set of tuples is an automorphism class of the structure. We present a clean definition of the syntax and semantics of this logic and investigate its expressive power. We extend the logic of Gire and Hoang with parameterized and nested fixed points and first-order combinations of fixed points. We show that the ability to supply parameters to fixed points strictly increases the power of the logic. Our logic can express the graph isomorphism problem and we show that, on almost all structures, it captures P GI, the class of problems decidable in polynomial time by a deterministic Turing machine with an oracle for graph isomorphism.

CSL Conference 2001 Conference Paper

Inflationary Fixed Points in Modal Logic

Anuj Dawar
Erich Grädel
Stephan Kreutzer

Abstract We consider an extension of modal logic with an operator for constructing inflationary fixed points, just as the modal μ-calculus extends basic modal logic with an operator for least fixed points. Least and inflationary fixed point operators have been studied and compared in other contexts, particularly in finite model theory, where it is known that the logics IFP and LFP that result from adding such fixed point operators to first order logic have equal expressive power. As we show, the situation in modal logic is quite different, as the modal iteration calculus (MIC) we introduce has much greater expressive power than the μ-calculus. Greater expressive power comes at a cost: the calculus is algorithmically much less manageable.

I&C Journal 1998 Journal Article

A Restricted Second Order Logic for Finite Structures

Anuj Dawar

We introduce a restricted version of second order logic SO ω in which the second order quantifiers range over relations that are closed under the equivalence relation ≡ k ofkvariable equivalence, for somek. This restricted second order logic is an effective fragment of the infinitary logicL ω ∞ω, but it differs from other such fragments in that it is not based on a fixed point logic. We explore the relationship of SO ω with fixed point logics, showing that its inclusion relations with these logics are equivalent to problems in complexity theory. We also look at the expressibility of NP-complete problems in this logic.

CSL Conference 1996 Conference Paper

First Order Logic, Fixed Point Logic and Linear Order

Anuj Dawar
Steven Lindell
Scott Weinstein

Abstract The Ordered conjecture of Kolaitis and Vardi asks whether fixed-point logic differs from first-order logic on every infinite class of finite ordered structures. In this paper, we develop the tool of bounded variable element types, and illustrate its application to this and the original conjectures of McColm, which arose from the study of inductive definability and infinitary logic on proficient classes of finite structures (those admitting an unbounded induction). In particular, for a class of finite structures, we introduce a compactness notion which yields a new proof of a ramified version of McColm's second conjecture. Furthermore, we show a connection between a model-theoretic preservation property and the Ordered Conjecture, allowing us to prove it for classes of strings (colored orderings). We also elaborate on complexity-theoretic implications of this line of research.