6
$\begingroup$

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?

$\endgroup$
7
$\begingroup$

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 are working on developing something too).

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

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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