# Questions tagged [finite-model-theory]

The tag has no usage guidance.

20 questions
Filter by
Sorted by
Tagged with
1 vote
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'...
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?
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....
1 vote
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|$.. ...
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 ...
24 views

Let M a finite state transducer define as : $M=<X,Y,S,\delta,\lambda>$ What we mean by quasi-linear finite automata?
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 ...
1 vote
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 ...
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 ...
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 ...