11
votes
Accepted
Existing implementation of Scott's reduction?
You might check the FO2 solver by Tomer Kotek et. al (ICDT 2017): https://forsyte.at/alumni/kotek/fo2-solver/
as well as an FO2 solver by Tony Tan and his students (LICS 2021):
https://arxiv.org/abs/...
- 1,185
9
votes
Accepted
For any two non-isomorphic graphs $G, H$, does there exist a polysize, polylog quantifier depth first order formula which witnesses this?
Thanks to my colleague Maxim Zhukovskii for suggesting this answer.
It turns out that the answer is negative, and the counterexample is rather simple. Just take $G=K_m\sqcup \overline{K_m}$ and $H=K_{...
- 546
8
votes
Accepted
Validity problem of intuitionistic two-variable logic
The two-variable fragment of intuitionistic first-order logic is undecidable, as proved in
Roman Kontchakov, Agi Kurucz, and Michael Zakharyaschev: Undecidability of First-Order Intuitionistic and ...
- 16.5k
7
votes
Accepted
Kleene Algebra for star-free regular expressions
You might be interested in bounded synchronization delay expressions.
See [1] for details on these expressions.
To sum up, they are equivalent to star-free expressions, but instead of using complement,...
- 8,588
6
votes
The theory of definitions in first order logic
I don't have the books handy at the moment, but I think Shoenfield's "Mathematical Logic" and Hinman's "Fundamentals of Mathemtical Logic" would contain much if not all of what you're looking for.
...
- 161
5
votes
Evaluating asymptotic probabilities of First Order Logic Formulas?
By slightly modifying Grandjean's algorithm (reference in Emil's answer), one can show that for any fixed $k\geq 1$ and for a fixed finite (relational) language $L$, the problem of determining the ...
- 939
5
votes
Looking for some lecture videos on logic, models of computation and computational complexity/tcs fundamentals
Ryan O'Donnell (professor at Carnegie Mellon) has a wonderful undergraduate complexity theory series that goes through the fundamentals quite well, and he's an engaging lecturer. He also has a similar ...
- 1,134
5
votes
Accepted
Is Scott's reduction sound for $\mathrm{FO}^2$ with equality?
Yes. Just employ the formula $\forall{x}\forall{y} \; R(x,y) \leftrightarrow (x=y)$ (for a fresh binary predicate $R$), which allows you to "hide" the equality inside the $\forall\forall$-...
- 1,185
4
votes
Accepted
Normal forms for counting quantifiers?
I believe that the formula with the quantifier prefix you want to achieve are strictly less expressive than the two-variable logic with counting quantifiers. So there is no hope that you can translate ...
- 1,185
4
votes
Can modern SAT-Solvers utilise the symmetry of First Order Logic?
There exist first order (FO) logic systems that allow you to actually write FO constraints, and to reason with them in very intricate ways. E.g., see the IDP system.
For instance, I took a small ...
- 141
4
votes
A clear and rigorous explanation of critical pairs and the Knuth-Bendix completion algorithm?
The two obvious references are:
Chapter 7 of Term Rewriting and All That, notable for its pedagogy and accessible examples
Chapter 7 of Term Rewriting Systems, notable for its completeness and ...
- 13.7k
4
votes
A first order logic extended with binding terms like the familiar set descriptors $\{x:\varphi\}$
I would recommend looking at higher-order logics (HOL), for instance Lambek and Scott's Introduction to Higher-Order Categorical Logic. Such a logic will set up binding of bound variables and treat ...
- 28.1k
4
votes
Evaluating asymptotic probabilities of First Order Logic Formulas?
I assume you are talking about purely relational sentences, as otherwise the 0–1 law does not hold. As should be explained somewhere in those notes, an FO sentence in a finite relational language $L$ ...
- 16.5k
4
votes
Accepted
Resources for first-order and second-order monadic logics with a model-checking objective
It depends what precisely do you want to learn. A good reference is the finite model theory book by Libkin. https://homepages.inf.ed.ac.uk/libkin/fmt/fmt.pdf (chapters 2 and 7).
If you want more ...
- 1,185
3
votes
Accepted
Why isn't the proof obtained using Buss's proof of the derivational completeness of LK anchored?
The answer occurred to me right after I finished typing up the post. Rather than delete it, I figured I would post it anyway in case anyone else has the same question.
Answer
The mistake in the ...
- 201
3
votes
Evaluating asymptotic probabilities of First Order Logic Formulas?
As stated, the problem can be reduced to the query evaluation problem over the Rado graph (or the corresponding structure for non-binary vocabularies). Hence, there is a huge chance that the problem ...
- 1,185
3
votes
Accepted
Scott's normal form for $\exists y \forall x R(x,y) $
Your solution is correct. It suffices to see that the formulae $\exists{y} P(y)$ and $\forall{x} \exists{y} P(y)$ are equi-satisfiable, which allows you to put your formulae in the desired form.
- 1,185
3
votes
Accepted
State of the Art for the Monadic Class?
I found signs that such a decision procedure was implemented in the (general purpose) theorem prover SPASS.
In particular see the thesis of Ann-Christin Knoll, On Resolution
Decision Procedures
for ...
- 13.7k
3
votes
State of the Art for the Monadic Class?
In a 1993 LICS paper, Bachmair, Ganzinger and Waldmann showed that set constraints are equivalent to monadic FOL, in Set Constraints are the Monadic Class. If memory serves, set constraints are ...
- 32.3k
2
votes
Accepted
Tableau method for two-variable first-order logic
Apparently a tableau for $FO^2$ has not been given explicitly but a tableau for the expressively equivalent description logic $ALBO^{id}$ has been given in:
Renate Schmidt and Dmitry Tishkovsky, Using ...
- 1,558
2
votes
Tableau method for two-variable first-order logic
You might check the FO2 solver by Tomer Kotek: https://forsyte.at/alumni/kotek/fo2-solver/ This is the only existing FO2 solver (Tony Tan with his student have a paper under submission, in which they ...
- 1,185
2
votes
A clear and rigorous explanation of critical pairs and the Knuth-Bendix completion algorithm?
There is a rather technically-detailed description to be found in any of the following:
D.F. Holt, D.B.A. Epstein, and S. Rees.
The use of knuth-bendix methods to solve the word problem in automatic ...
- 773
2
votes
Complexity of Model Enumeration in function free, equality free, First Order Logic with only Unary Predicates?
Reading the discussion below the other answer made me realize that it’s not immediately obvious what is the complexity of translation of FO sentences in this language to equivalent FO1 sentences. ...
- 16.5k
2
votes
Looking for some lecture videos on logic, models of computation and computational complexity/tcs fundamentals
Prof. Tim Roughgarden (Stanford University) Lectures on algorithms and more are also great. He is one of the best lecturers out there...
https://www.youtube.com/channel/UCcH4Ga14Y4ELFKrEYM1vXCg/...
- 1,596
2
votes
Accepted
References on second-order quantifier elimination and related topics
Since there are no answer I think it may be useful to post what I've found:
Dov M. Gabbay, Renate A. Schmidt, Andrzej Szalas
Second-Order Quantifier Elimination - Foundations, Computational Aspects ...
- 1,558
2
votes
Second-order reachability in second-order logic
In fact, we can always stay in the second-order realm (as long as our "base structure" is infinite)!
First, let's look at the particular case where our base structure is $\mathcal{N}=(\...
- 568
1
vote
Accepted
Inexpressibility results for first-order logic that fail extending the language
As noted in the comments it takes some care to phrase this question in a nontrivial way. However, this can be done in at least a couple ways, one yielding a positive answer and the other yielding a ...
- 568
1
vote
Accepted
Number of equivalent formulas in a function-free first order logic language?
One can prove in a quite straightforward manner an upper bound on the number of non-equivalent formulas with quantifier rank at most $q$ over a fixed finite relational vocabulary. I will sketch an ...
- 939
1
vote
Accepted
reducing this problem to a decision problem
Your problem is coNP-hard, by reduction from SAT. In particular, using inequalities $x \ge 1$, $x \le 0$ and interpreting $0$ as false and $1$ as true, we can encode any SAT formula $\varphi$ into ...
- 11.6k
1
vote
Accepted
Complexity of Model Enumeration in function free, equality free, First Order Logic with only Unary Predicates?
Answering your second question, the logic you mean is known as Monadic FO or Monadic Predicate Calculus. It is known the logic is equivalent to FO1 (as Emil Jeřábek suggested) by some very old works ...
- 1,185
Only top scored, non community-wiki answers of a minimum length are eligible