Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [descriptive-complexity]

Descriptive complexity classifies problems based on how hard it is to express the problem in some logical formalism.

7
votes
1answer
144 views

P and Descriptive Complexity

In the Complexity Zoo, it says [1] that, in descriptive complexity, $P$ can be defined by three different kind of formulae, $FO(LFP)$ which is also $FO(n^{O(1)})$, and also as $SO(HORN)$. However, ...
1
vote
0answers
86 views

Proof of SAT is complete for NP via first-order reductions

So I have been reading this: https://people.cs.umass.edu/~immerman/book/ch7.pdf I do not understand the proof of theorem 7.16, which says that SAT is complete for NP via first-order reductions. My ...
4
votes
1answer
111 views

Descriptive model theory classification of Counting hierarchy

Descriptive model theory uses logic to characterize complexity classes How to model Counting Hierarchy PSPACE in descriptive model theory?
7
votes
1answer
311 views

Where does the “intuitive” understanding of Kolmogorov complexity fails

Often, the Kolmogorov complexity of some string $x$ is defined as the length of the shortest program producing $x$, for example on wikipedia. So to give this more formal meaning, define $$ K'(x) := ...
3
votes
2answers
130 views

Construct proof systems for common algorithmic task, like equivalence of regular expressions

A propositional proof system according to Cook and Reckhow for a language $L \subseteq \Sigma^{\ast}$ is a deterministic polynomial time function $f : \Sigma^{\ast} \to L$ that is onto. For $y \in L$ ...
0
votes
0answers
147 views

Questions about the definition of the Quantum Turing Machine

I am trying to have a better understanding of the definition of the Quantum Turing Machine. My questions: If the output of a quantum program is the eigenvalue of the ground state of a Hamiltonian ...
9
votes
0answers
189 views

reference request: deciding validity of higher-order quantified boolean formulas is not Kalmar-elementary

$\newcommand\iddots{⋰}$In "A simple proof of a theorem of Statman" (TCS 1992), Harry Mairson gives a simple proof of Statman's result that deciding $\beta\eta$-equality of terms in simply typed lambda ...
10
votes
1answer
202 views

What do dichotomy theorems feed on?

It is well known that certain classes of NP-problems have dichotomy theorems, which guarantee that every task in the class is either NP-complete or is in P. The best known such result is Schaefer's ...
1
vote
0answers
130 views

Do problems have to be statable in $\Pi_1$ to use Levin's universal search to find short proofs if P=NP

In If P=NP, could we obtain proofs of Goldbach's Conjecture etc.? it talks about the hypothetical world where P=NP and using the proof of it to prove a problem/theorem assuming that it has a short ...
5
votes
1answer
176 views

Expressiveness of Infinitary Logic

I'm trying to put together a general picture of the expressiveness of some logics: First-Order Logics, Fixed-Point Logics, (Finite Variable) Infinitary Logics and the respected versions with Counting. ...
7
votes
3answers
227 views

Completeness of the extension of first order logic with least fixed point order operator

Is there any result about the extension of first order logic with least fixed point operator, being complete (as logic in general on infinite structures too) or not? In other words does the Goedel ...
2
votes
1answer
65 views

Infinitary Counting Logics: 1-sorted vs. 2-sorted framework

There are two ways to extend infinitary logic with counting: Grädel's way (cf. p. 11): We extend $L_{\infty\omega}$ by introducing a counting existential quantifier: $$ \mathcal{A} \models \exists^{...
6
votes
1answer
182 views

Is infinitary logic a logic in the sense of Gurevich?

Gurevich provides an exact definition of what Logic capturing PTIME is. An abstract logic $L$ consists of a set of $L[\tau]$-sentences for each vocabulary $\tau$, and a mapping that maps a property $...
8
votes
1answer
364 views

What is wrong with this $\mathsf{L} \subseteq \mathsf{L}-$uniform $\mathsf{NC}^1$ argument?

The following is not believed to be true: $\mathsf{L} \subseteq \mathsf{L}-\mbox{uniform } \mathsf{NC}^1$ Can you help me see where the argument breaks down? The directed reachability problem is ...
3
votes
2answers
597 views

Context-free Grammar for a Context-free Language Intersecting a Regular Language (get the Maximum Number of Rules)

It is well known that the intersection of $L \cap R$ of a context-free Language $L$ and a regular Language $R$ is context-free. Each proof I have seen constructs a automaton (a PDA) that accepts $L$ ...
2
votes
1answer
281 views

What is a commutative transitive closure operator?

When reading about descriptive complexity theory, I have read about a "commutative transitive closure operator". I understand transitive closure operators, but what is a commutative transitive closure ...
9
votes
2answers
899 views

How can we express “$P=PSPACE$” as a first-order formula? [closed]

How can we express "$P=PSPACE$" as a first-order formula? Which level of the arithmetic hierarchy contains this formula (and what is the currently known minimum level of the hierarchy that contains it)...
1
vote
1answer
289 views

Least fixed point logic is efficiently $\operatorname{P}$-bounded for $\operatorname{P} \Leftrightarrow L_\leq$ is a logic for $\operatorname{P}$

A least-fixed point (LFP) formula is $\leq m$-invariant iff f.a. structrues $\mathcal{A}$ with $|A| \leq m$ and all orderings $<_1,<_2$ on $A$ $$(\mathcal{A},<_1) \models_{LFP} \varphi \...
2
votes
1answer
142 views

Consequences of a $p$-optimal proof system for $\operatorname{TAUT}$

I'm reading a paper which shows the result: $(1)$ There is a $p$-optimal proof system for $\operatorname{TAUT}$. $\Leftrightarrow$ $(2)$ $L_{\leq}$ is a $P$-bounded logic for $P$. Both $(1)$ and $(...
9
votes
3answers
3k views

Understanding least-fixed point logic

To better understand a paper I'm trying to get a brief understanding of least-fixed point logic. There are a few points where I am stuck. If $G = (V,E)$ is a graph and $$ \Phi(P) = \{(a,b) \mid G \...
9
votes
2answers
258 views

Intuition behind proof systems

I'm trying to under stand the paper On p-Optimal Proof Systems and Logic for PTIME. There is a notion called proof systems in the paper and I do not get the intution: $\Sigma = \{0,1\}$ ... We ...
20
votes
0answers
255 views

Descriptive complexity characterization of TimeSpace classes

Are there descriptive complexity characterizations for TimeSpace complexity classes like $\mathsf{SC^i}= \mathsf{DTimeSpace}(n^{O(1)},O(\lg^i n))$?
9
votes
1answer
280 views

FO-uniform AC0 with some predicate

My question is about finite model theory/descriptive complexity, so $FO(R)$ will mean "first order over finite binary words, using predicates Rs and a unary predicate P true on the position of the 1 ...
14
votes
0answers
287 views

Proof assistant formalizations of Finite Model Theory

I'm wondering if anyone knows of a formalization (even limited) of any part of finite model theory in any of the major proof assistants. (I'm most familiar with Coq, but Isabelle, Agda, etc. would ...
10
votes
2answers
205 views

When does an FO property kill off NL-hardness?

Context: We consider only digraphs. Let CYCLE be the language of graphs with a cycle; it is an NL-complete problem. Let HASEDGE be the language of graphs with at least one edge. Then trivially, $\...
5
votes
0answers
189 views

Logic capturing automorphism-invariant $\mathsf{AC^0}$ properties

Q1. Is there a logic that is computable in polynomial-time which contains all order-invariant properties computable in smaller classes like $\mathsf{AC^0}$ (or $\mathsf{TC^0}$)? Motivation As you ...
7
votes
1answer
151 views

Using MSOL for solving BIDS problem

From "Linear Time Solvable Optimization Problems on Graphs of Bounded Clique Width" (B. Courcelle et al) we know that any problem that can be written on MSOL (Monadic Second Order Logic) has a linear ...
19
votes
5answers
1k views

Why do relational databases work at all, given the theoretical exponential complexity of answer finding (in the size of the query)?

It seems to be known that to find an answer to a query $Q$ over a relational database $D$, one needs time $|D|^{|Q|}$, and one cannot get rid of the exponent $|Q|$. As $D$ can be very large, we ...
6
votes
3answers
822 views

What is First-Order Rewritable (and FO-Query)?

I just wonder what FO Rewritable is, put an example to make it clearer for me. Also, I heard that a language that is FO Rewritable is very good, in what sense? It is said as follow: A class C of ...
10
votes
2answers
417 views

MSOL optimization problems on graphs of bounded cliquewidth, with cardinality predicates

CMSOL is Counting Monadic Second Order Logic, i.e. a logic of graphs where the domain is the set of vertices and edges, there are predicates for vertex-vertex adjacency and edge-vertex incidence, ...
5
votes
1answer
305 views

What is the parameterized complexity of following model checking problem?

Input: Graph $G$ and formula $\varphi_1(\vec x),\varphi_2(\vec x)$ Parameter: $tw(G)+|\varphi_1|+|\varphi_2|$ Problem: Decide if $|\varphi_1(G)|=|\varphi_2(G)|$ where $tw(G)$ is the treewidth of $...
2
votes
3answers
145 views

Searching for matching queries

Suppose you have a large set of queries (could be in SQL form, but conceivably the same problem exists for search engine query strings or Lucene expressions, etc...) stored and you want to know which ...
10
votes
1answer
380 views

Could a descriptive complexity version of Rice's theorem be used to separate AC0 and PSPACE?

In this question, it was mentioned that there are descriptive complexity versions of Rice's theorem. I found a proof of the following theorem: Given a complexity class C, nontrivial properties of ...
8
votes
1answer
153 views

Is testing two SO-Horn queries for equivalence decidable?

It follows from Rice's theorem that you cannot determine whether or not two Turing machines decide the same language. My question is: Does this also apply in descriptive complexity settings, ...
20
votes
2answers
714 views

Are there descriptive complexity representations of quantum complexity classes?

The title more or less says it all, but I guess I could add a bit of background and some specific examples I'm interested in. Descriptive complexity theorists, such as Immerman and Fagin, have ...
8
votes
1answer
324 views

SAT in finite model theory without order

It is well known in finite model theory that without an order on the input, the expressivity is very limited. For example it is known that $FO(<,\textit{PFP})$ is equal to PSPACE, and $FO(\textit{...
10
votes
1answer
432 views

Finite One-Way Permutation with Infinite Domain

Let $\pi \colon \{0,1\}^* \to \{0,1\}^*$ be a permutation. Note that while $\pi$ acts on an infinite domain, its description might be finite. By description, I mean a program that describes $\pi$'s ...
20
votes
0answers
489 views

Model-checking for three-variable logics and restricted structures

Denote the $k$-variable fragment of logic $L$ by $L^{(k)}$. The model-checking problem for a logic $L$ with respect to a class of structures $C$, denoted $MC(L,C)$, is the decision problem $MC(L,C)...
6
votes
1answer
151 views

Non-interesting numbers via resource-bounded properties?

There is an old joke about the smallest non-interesting number being interesting in itself (I have heard it attributed to Richard Hamming). This is then used to justify the argument that every number ...
12
votes
3answers
230 views

Is there a natural restriction of VO logic which captures P or NP?

The paper Lauri Hella and José María Turull-Torres, Computing queries with higher-order logics, TCS 355 197–214, 2006. doi: 10.1016/j.tcs.2006.01.009 proposes logic VO, variable-order logic. This ...
10
votes
1answer
478 views

Ehrenfeucht-Fraïssé games (Ajtai-Fagin in fact) for regular languages.

Immerman (Descriptive Complexity, 1999) presents the EF games for existential monadic second order (Ajtai-Fagin games) on page 127. As $\exists$MSO on words is equivalent to regular languages, the ...
38
votes
5answers
1k views

Is there a logic without induction that captures much of P?

The Immerman-Vardi theorem states that PTIME (or P) is precisely the class of languages that can be described by a sentence of First-Order Logic together with a fixed-point operator, over the class of ...
10
votes
0answers
335 views

Collapsing of exptime and alternation bounded turing machine

This question was already asked on math overflow, but I did not find any answer to my question (or let say the answer was that up to the knowledge of those people, no answer were known) Let C be a ...
18
votes
0answers
456 views

To what extent MSO = WS1S, when adding relations?

[This question has been asked on MathOverflow with no luck a month ago.] Let me first clarify my definitions. For a word $w \in \Sigma^*$, with $\Sigma =\{a_1, \ldots, a_n\}$, I define two ...