Questions tagged [finite-model-theory]
The finite-model-theory tag has no usage guidance.
20
questions
1
vote
1
answer
46
views
How to express that a graph has Independent set of size at least $n/2$ in $\exists SO$
I am looking to provide a formula saying "A graph with $n$ vertices has an independent set $X$ of size at least $n/2$" in existentional second order logic.
(This is exercise 1.2. from Libkin'...
- 267
0
votes
0
answers
22
views
Practical applications of finite model theory to databases
I have heard that finite model theory has connections to database theory. Is there an example of where this database theory could be used by programmers developing database applications?
- 287
0
votes
0
answers
87
views
How to find the intersection of two FAs and then check if two FAs are equal?
I am still quite confused on how to properly handle in answering the intersection and equality of two FAs in terms of table form and manipulating its transformation....
- 13
1
vote
0
answers
105
views
Horn formulas, existential second order logic and the Cardinality constraint
Consider this Problem $P$ as follows: $~$ Given a set $S$ and a constant $K$.. $~$Is there a subset $M$ of $S$, such that $|M| \ge K$?
Of course, $P$ can be easily solved in time polynomial in $|S|$.. ...
3
votes
1
answer
136
views
How to describe Deterministic Transitive Closure in FOL?
In "Finite Model Theory and Its Applications", page 152, it is said that Deterministic Transitive Closure, on ordered finite structures, captures LOGSPACE.
Hence, taking into account that ...
- 407
0
votes
0
answers
24
views
About quasi-linear finite automata
Let M a finite state transducer define as : $M=<X,Y,S,\delta,\lambda>$
What we mean by quasi-linear finite automata?
4
votes
2
answers
82
views
Defining $a^n b^{n^2}$ with one existential SO binary relation
Is it possible to define the language:
$$L = \{ a^n \; b^{n^2} \}$$
using an existential second order sentence over strings (ordered structures with unary predicates $U_a(x), U_b(x)$) using only ...
- 12.4k
1
vote
0
answers
73
views
Datalog Program Equivalence with Fixed Universe Size
It is well known that to compute equivalence of two Datalog programs (or equivalently of two first order formulas with the least fixed point operator) wrt all possible inputs and universes, is ...
- 634
2
votes
0
answers
70
views
LTL and alternation
Apparently, model checking LTL on Kripke structures is PSPACE-complete (see this question). Usually, when something in finite model theory is PSPACE-hard, there is a simple proof using the APTIME ...
- 2,214
2
votes
1
answer
291
views
Datalog Self Interpretation
According to https://link.springer.com/article/10.1007%2Fs001530050135 (Logics that define their own semantics, Imhof 1999) the logic FO[LFP] can define its own semantics, though the proof (of ...
- 634
2
votes
1
answer
52
views
How to understand the notion of boolean query via Immerman's definition
A query is any mapping $I:STRUC[\sigma] \to STRUC[\tau]$ that is polynomially bounded. A boolean query is a map $I_b: STRUC[\sigma] \to \{0,1\}$. A boolean query can also be thought as the susbset:
$...
- 23
0
votes
2
answers
170
views
What is meant by the term 'state' in a finite-state machine?
What is meant by the term 'state' in a finite-state machine?
I have not seen a proper definition on the web and am looking for a university-level answer.
Thank you in advance.
- 41
-2
votes
1
answer
456
views
Finite State Automaton Transition Diagram
I got an alphabet E={x,y,z}. And i want to create a finite state automaton that accepts strings consisting of at least two x's, followed by at most three y's followed by any number of z's. And i want ...
- 101
5
votes
2
answers
379
views
propositional Modal logic filtration definition
Hello I have a slightly unusual question which relates to a definition of filtration structure. The following is my current state of the definition:
$ \mathcal{M} = (W, R, L) $, W is a set of worlds,
...
- 51
16
votes
0
answers
301
views
Using logic to prove non-regularity of a language
A language $L$ is regular if and only if it is definiable by a sentence in monadic second order logic (MSO) over strings (J.R. Buchi, Weak second-order arithmetic and Finite automata; Z. Math. Logik ...
- 12.4k
12
votes
2
answers
3k
views
Why is least fixed point (lfp) important in program analysis
I am trying to get a big picture on the importance of least fixed point (lfp) in program analysis. For instance abstract interpretation seems to use the existence of lfp. Many research papers on ...
- 223
5
votes
2
answers
682
views
Proof of Trakhtenbrot's theorem
In the proof of Trakhtenbrot's theorem (as given in "Elements of Finite Model Theory" by Leonid Libkin), for every Turing machine $M$, author constructs a FO sentence $\Phi_M$ of vocabulary $\sigma$ ...
- 191
4
votes
0
answers
149
views
Decidability over finite graphs of small degree [closed]
Suppose $\sigma$ is a vocabulary of First Order logic consisting of one binary relation $E$ and let $\phi$ be a $\sigma$ sentence (FO formula with no free variables). Is it decidable whether there is ...
- 191
20
votes
3
answers
347
views
Extension of SQL capturing $\mathsf{P}$
According to Immerman, the complexity class associated with SQL queries is exactly the class of safe queries in $\mathsf{Q(FO(COUNT))}$ (first-order queries plus counting operator): SQL captures safe ...
- 22.2k
19
votes
2
answers
1k
views
Does the 'difference' operation add expressiveness to a query language that already includes 'join'?
The set difference operator (e.g., EXCEPT in some SQL variants) is one of the many fundamental operators of relational algebra. However, there are some databases ...
- 3,078