# Questions tagged [finite-model-theory]

The tag has no usage guidance.

30 questions
Filter by
Sorted by
Tagged with
55 views

### Inexpressibility of Second order

In finite model theory, Ehrenfeucht-Fraïssé games gives us tools to prove inexpressibility results for FOL. Pebble games do the same for infinitary logic with finitely many variables. Do we have such ...
3k views

190 views

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 $... 1answer 492 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 ... 1answer 373 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 ... 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 ... 0answers 93 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 ... 0answers 117 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. 0answers 115 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 ... 0answers 290 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 ... 1answer 295 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 ... 3answers 601 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 ... 1answer 256 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., ... 0answers 193 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 you ... 1answer 377 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 ... 5answers 1k 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 ... 1answer 305 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 of$...
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{...