2022 Developer Survey is open! Take survey.
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/...
user avatar
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_{...
user avatar
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 ...
user avatar
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,...
user avatar
  • 7,643
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. ...
user avatar
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 ...
user avatar
  • 580
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$-...
user avatar
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 ...
user avatar
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$ ...
user avatar
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 ...
user avatar
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 ...
user avatar
  • 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 ...
user avatar
  • 13.1k
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 ...
user avatar
  • 26.4k
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 ...
user avatar
  • 13.1k
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 ...
user avatar
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.
user avatar
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/...
user avatar
  • 1,456
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 ...
user avatar
  • 1,112
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 ...
user avatar
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 ...
user avatar
2 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 ...
user avatar
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. ...
user avatar
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 ...
user avatar
1 vote

Can modern SAT-Solvers utilise the symmetry of First Order Logic?

I take that by "symmetry" we are talking about reasoning over the generalities in a first-order formula instead of grounding all the possible assignments. I may be misinterpreting the ...
user avatar

Only top scored, non community-wiki answers of a minimum length are eligible