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


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


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


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