10

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/2104.10621 Answering the question, the authors implemented an improved version of Scott Normal Form, called therein "Skolemized Scott Normal Form". All ...


5

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$-part of the Scott normal form. Then you proceed as usual. EDIT: I've noticed that you wrote that $\alpha$ in $\forall{x}\forall{y} \; \alpha$ is a binary ...


5

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 graduate lecture series that mostly picks up where the undergrad series left off. (Note that this series does not cover logic, and I'm not aware of any videos ...


4

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 variation of your example and coded it up in the online IDP editor: vocabulary V{ type D P(D) } theory T: V{ ?x: P(x). } structure S:V{ D = {a;b} } ...


4

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 any C2 formuale into such a form. Similar types of Scott-normal forms were obtained in: Bartosz Bednarczyk, Witold Charatonik: Modulo Counting on Words and ...


3

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.


3

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 attention to detail, though a bit dated at this point I guess. Note that neither refers to completion as "Knuth-Bendix" completion in the index, since the ...


2

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/playlists


2

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 Tableau to Decide Description Logics with Full Role Negation and Identity, ACM Trans. Comput. Log. 15(1): 7:1-7:31 (2014)


2

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 proposed another algorithm, based on probabilistic methods). I'm not aware of any tableaux algorithm for FO2.


2

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 groups. J. Symbolic Computation, 12:397--414, 1991. Charles C. Sims. Computation with Finitely Presented Groups. Cambridge, 1994. Derek F. Holt. The warwick ...


2

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. While the quoted fact that satisfiability of these sentences is NEXP-complete (whereas satisfiability of FO1 sentences is in NP) implies that any such translation ...


1

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 by Behmann and Loewenheim. Regarding the first question, I do not know what is the complexity of model enumeration, but satisfiability checking is NExpTime-...


1

The core of DPLL uses essentially QSAT identity $∃xA = A[x/1] \vee A[x/0]$. When implemented with backtracking space requirements are not high. function DPLL(Φ) [...] return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {not(l)}); If you supply the negation $\neg B$ of your problem to a SAT solver, the SAT solver will decide QSAT $∀x_1..∀x_nB$ for you and act as a ...


1

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 question, but I'll answer anyway. First off, there is some definitional inconsistency with first-order logic depending on the field. Modern automated theorem provers ...


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