As per this paper by Grädel, Kolaitis and Moshe Vardi, they discuss computational complexity of satisfiability problem in $\mathrm{FO^2}$, In order to do this they use Scott's reduction. Which is the fact that any sentence in $\mathrm{FO^2}$ can be reduced to Scott's Normal form in polynomial time. The Scott's Normal form is given as $$\forall x \forall y \alpha(x,y) \land \bigwedge_{i=1}^{m} \forall x \exists y \beta_{i}(x,y) $$ Does anyone know of existing code base where scott's reduction is implemented, i.e I input an arbitrary $\mathrm{FO^2}$ sentence and get it's Scott's Normal Form?


1 Answer 1


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 the details are available here: https://arxiv.org/pdf/1610.02101.pdf


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.