Questions tagged [descriptive-complexity]

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

58 questions
Filter by
Sorted by
Tagged with
131 views

Why is order/choice an issue for a logic for PTIME

As I'm reading on the question of a logic for PTIME and in particular about CPT and its variants, whilst things make sense and I follow along, I came to realise that I don't fundamentally understand ...
1 vote
44 views

• 513
427 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 ...
• 2,309
841 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$ ...
• 301
337 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 ...
• 41
1k 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)...
• 101
1 vote
397 views

• 513
308 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 ...
• 513
281 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))$?
• 21.6k
464 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 ...
• 1,561
320 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 ...
• 2,924
231 views

• 901
155 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 ...
• 123
455 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 ...
174 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, ...
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{...