The tag has no wiki summary.

learn more… | top users | synonyms

4
votes
1answer
119 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. ...
2
votes
1answer
54 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 ...
6
votes
1answer
123 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 ...
1
vote
1answer
223 views

What are good conferences for algorithms about finite automata?

I am writing a research paper, which describes some properties about finite automata. It also provides a couple of algorithms that can measure some aspects of the properties. Could you point out some ...
8
votes
1answer
287 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 ...
1
vote
0answers
75 views

Decidability one relation, binary FOL over finite models

Suppose $\sigma$ is a vocabulary consisting of one binary relation $E$ and let $\phi$ be a $\sigma$ sentence. Is it decidable whether there is a finite directed graph $G$, with all in- and out-degrees ...
-1
votes
0answers
92 views

How does “δ:Q×Σ→Q” read in the definition of a DFA (deterministic finite acceptor)? [closed]

How do you say "δ:Q×Σ→Q" in English? Describing what "×" and "→" mean would also help.
2
votes
0answers
101 views

Applications of FMT in Algebra

Most of the applications of Finite Model Theory I have seen are in graphs, using FMT one can prove that certain properties of finite graphs are not FO definable. I am interested in similar kind of ...
6
votes
2answers
694 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 ...
8
votes
1answer
200 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 ...
11
votes
0answers
209 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 ...
15
votes
3answers
509 views

What is the minimal extension of FO that captures the class of regular languages?

Context: relations between logic and automata Büchi's Theorem states that Monadic Second Order logic over strings (MSO) captures the class of regular languages. The proof actually shows that ...
2
votes
1answer
249 views

FSMs with finite memory

Consider an FSM and a finite set of variables. The FSM has the special property that each state contains a set of commands, with each command taking the form of "variable = expr(variable, ...)" e.g., ...
5
votes
0answers
157 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 ...
8
votes
1answer
326 views

Database query languages for efficient queries

It seems that in popular query languages for relational databases, it is possible to create queries that will require a lot of resources to answer. In practice, database admins manage this by limiting ...
9
votes
3answers
334 views

Finding a finite model

I know that the question "does a first order formula $\phi$ have a model" is undecidable in general. Could anyone give me a link or a book which give the answer for finite models. If I have a first ...
17
votes
5answers
641 views

Ambiguity and Logic

In automata theory (finite automata, pushdown automata, ...) and in complexity, there is a notion of "ambiguity". An automaton is ambiguous if there is a word $w$ with at least two distinct accepting ...
5
votes
1answer
344 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 ...
5
votes
1answer
290 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 ...
2
votes
3answers
137 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 ...
7
votes
1answer
274 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 ...
35
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 ...