Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [finite-model-theory]

The tag has no usage guidance.

4
votes
1answer
115 views

Is graph connectivity definable in existential MSO with vertices and edges?

Can $\exists$MSO$_2$ express graph connectivity? Monadic SO (MSO) is the fragment of second-order logic in which the second-order quantifiers range over relations of arity 1 only. $\exists$MSO is the ...
2
votes
1answer
87 views

Is Eulerian Path (or Eulerian Cycle) definable in Monadic Second Order Logic?

Does there exist a monadic second order logic formula which is satisfied by a graph if and only if it has an Eulerian path (or Eulerian cycle). I am looking for properties of graphs which are ...
5
votes
1answer
135 views

Turing machines over a structure

I have heard of models of computation where you have a Turing machine, but instead of symbols over a finite alphabet you have elements from some tau-structure, and write instructions are replaced with ...
4
votes
1answer
106 views

Descriptive model theory classification of Counting hierarchy

Descriptive model theory uses logic to characterize complexity classes How to model Counting Hierarchy PSPACE in descriptive model theory?
3
votes
0answers
56 views

Decidability of the monadic second-order theory of a class of finite structures

Let $L$ be the set of sentences in some logic. I am interested in cases where $L$ is the set of sentences in monadic second-order logic, or it is its $\Pi^1_1$ fragment. Let $K$ be a class of finite ...
1
vote
0answers
87 views

Is there a signature of a first-order language that characterize the class of regular languages?

A previous question on this site was about extending the first-order logic with logical constants (quantifiers, fixed-point operators, etc.) to obtain a logical characterization of the class of ...
7
votes
1answer
323 views

Standard reference for basic model theory definitions

I am trying to give a formal presentation of the model-theoretical semantics of a language and I am a bit lost in the terminology. In particular, could somebody clarify the exact definitions of model-...
5
votes
1answer
175 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
65 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 \exists^{...
6
votes
1answer
182 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 $...
2
votes
1answer
461 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
363 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 ...
1
vote
0answers
91 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
115 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
114 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 ...
9
votes
3answers
3k 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 \...
9
votes
1answer
278 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 ...
14
votes
0answers
287 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 ...
17
votes
3answers
589 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
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., ...
5
votes
0answers
188 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 ...
9
votes
1answer
369 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 ...
11
votes
4answers
445 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
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 ...
6
votes
3answers
810 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
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 $...
2
votes
3answers
144 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 ...
8
votes
1answer
324 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 $FO(\textit{...
38
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 ...