The finite-model-theory tag has no wiki summary.
-5
votes
0answers
63 views
Turing machines question [closed]
I was having a hard time understanding and solving this question that wants me to show the final tape and figuring out if whether or not the turning machine accepts it or not. I have a list of 20 ...
1
vote
0answers
62 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
75 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
90 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 ...
5
votes
2answers
324 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
162 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
152 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
479 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
248 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., ...
4
votes
0answers
134 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 ...
0
votes
0answers
153 views
Transition Graph per alphabet? [closed]
How do you determine how many different Transition Graphs are over a particular alphabet? For example How many TG's are over the alphabet {x, y}. I am taking a class with a similar question from ...
8
votes
1answer
296 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
305 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 ...
16
votes
5answers
459 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
266 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
276 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
133 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 ...
6
votes
1answer
246 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 ...
30
votes
4answers
813 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 ...
