11

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 ...


9

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_{m+1}\sqcup \overline{K_{m-1}}$ for $n=2m$ and $G=K_m\sqcup \overline{K_{m+1}}$ and $H=K_{m+1}\sqcup \overline{K_m}$ for $n=2m+1$. (Here $K_s$ is an $s$-clique ...


7

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, they restrict the use of the Kleene star to certain languages: the prefix codes with bounded synchronization delay. This way, you can have your ...


6

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. Probably not what you want but perhaps worth mentioning anyway is A. P. Morse's book "A Theory of Sets". This is a development of (a rather idiosyncratic version ...


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 ...


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 ...


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 ...


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 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 variable contexts properly (single-sorted first-order logic tends to have a somewhat simplistic view of those). Note that your suggestion to always bind just a ...


3

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 the Monadic Fragment and Guarded Negation Fragment. This implements what you want, though I couldn't find the implementation online.


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

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 equivalent to regular tree grammars, so most of the algorithms developed there should portable to monadic FOL as well. I don't know the area that well, but set ...


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