11
Here is one possibility, but other people might use different words. I will use first-order logic as a running example.
Language
The language is a collection of expressions, which are syntactic entities, i.e., finite configurations without any a priori meaning. A language is described by the grammar, which determines which finite configurations are valid ...
8
There are recent exciting results concerning the search for a logic capturing PTIME.
The famous example by Cai, Fürer and Immerman showing that LFP+C does not capture
PTIME was based on a seemingly artificial class of graphs, though. Of course, it was constructed for the particular
task of demonstrating the restrictions of LFP+C. Only recently it was shown ...
8
You can express that $s$ is connected to $t\ne s$ in $G=(V,E)$ by the $\exists\mathrm{MSO}_2$ formula
“there exists $E'\subseteq E$ such that in the graph $(V,E')$, $s$ and $t$ have degree $1$, and all other vertices have degree $0$ or $2$.”
Note that the formula after the initial $\exists E'$ quantifier is first-order.
A graph of degree $\le2$ is a ...
7
Parity cannot be expressed in MSOL (see for instance http://www.cs.technion.ac.il/~janos/COURSES/236331-15/Lec-1.pdf), but connectedness Yes. Using instead $C_2$MSOL, one can express the existence of an eulerian cycle by using the equivalent characterisation : connected and every vertex has degree even.
6
There is a famous example of Cai, Fürer and Immerman, which shows that the $\mathcal{C}_{\infty\omega}^k$-hierarchy is strict and in particular that $\mathcal{C}_{\infty\omega}^\omega$ cannot express every query on finite structures. The paper is quite famous because it disproved a conjecture that IFP+C captures PTIME. Your proof that $\mathcal{L}_{\infty\...
6
The main conferences where automata are among the main topics are ICALP, LICS, STACS, CSL, MFCS, FSTTCS.
If you feel your paper is not strong enough for these conferences (which accept about a quarter of the papers that are sent each year), you can send to conferences which are a little less exigeant.
The ICALP submission deadline is soon (in a week), ...
6
In fact, the circuit depends on the input structure, not only on the input structure size. We take a tree-decomposition of the graph with additional colours and turn it into a convolution tree. The evaluation of the formula on this tree is reduced to computing the value of the convolution tree. To compute the value of the tree, it is turned into an ...
5
You could start with the survey article by Peter Hinman, Recursion on Abstract Structures, Chapter 11 of the Handbook on Computability Theory (editor E. R. Griffor). If you follow the references there you'll find a wealth of material.
5
This is only a partial answer (to the $PSPACE$ characterization), but I don't have the reputation to comment.
$PSPACE$ has the following (equivalent) descriptive characterizations:
$FO[2^{n^{O(1)}}]$, first-order logic with exponentially iterated quantifier blocks.
$SO[n^{O(1)}]$, second-order logic with polynomially iterated quantifier blocks.
$SO[TC]$, ...
3
Here is another attempt at a more comprehensive answer. Your question already contains the formal definition of FO-rewritability, which at its core says that you can reduce a query answering problem:
The problem $D\cup\Sigma\models Q$ is being reduced to a problem $D\models Q_\Sigma$.
Several noteworthy things are happening here. The original problem is ...
2
There are Nitpick and Nunchaku that are model finders for higher-order logic.
Nunchaku is more recent and can build models for axioms containing higher-order quantification. But, as the problem is generally undecidable, it may not find a (finite) model even if one exists.
2
As mentioned above: question answered by reference to FO(TC) games presented in Finite Model Theory by Ebbinghaus and Flum.
2
First question: A set $M$ is decidable if there is a Turing Machine which halts on all inputs and accepts all inputs $x$ with $x \in M$.
We try to encode $\bigwedge_{\phi \in X} \phi$ for arbitrary sets of $\mathsf{FO}[\tau]$-formulars $X$. Since, $\mathcal{P}(X)$ is uncountable there can be no code with finite alphabet. Hence, there can be no Turing ...
2
this is a very old post so you might have already encountered the answer as desired. Since I have been studying FO(LFP) for the past few months. I have some understanding of the answers you require.
To answer the requirement of positivity, the need comes from the fact that testing whether the formula captures a monotone operator or not is undecidable both ...
1
As a complement to Janoma's answer above: it's 'very good'--- from the point of view of implementation --- because given a FO-rewritable language, we can use the powerful engines (for evaluating queries directly against a database without dependencies) that are available. That's basically reducing the problem to evaluation of SQL queries.
Only top voted, non community-wiki answers of a minimum length are eligible
