<p>You might check the FO2 solver by Tomer Kotek et. al (ICDT 2017): <a href="https://forsyte.at/alumni/kotek/fo2-solver/" rel="nofollow noreferrer">https://forsyte.at/alumni/kotek/fo2-solver/</a></p>
<p>as well as an FO2 solver by Tony Tan and his students (LICS 2021):
<a href="https://arxiv.org/abs/2104.10621" rel="nofollow noreferrer">https://arxiv.org/abs/2104.10621</a></p>
<p>Answering the question, the authors implemented an improved version of Scott Normal Form, called therein &quot;Skolemized Scott Normal Form&quot;. All the details are available here: <a href="https://arxiv.org/pdf/1610.02101.pdf" rel="nofollow noreferrer">https://arxiv.org/pdf/1610.02101.pdf</a></p>

CC BY-SA 4.0
2020-07-30T12:08:26.337Z
2021-06-18T10:55:59.647Z
2021-06-18T10:55:59.647Z
Bartosz Bednarczyk
<p>As per this <a href="https://www.jstor.org/stable/421196?read-now=1&amp;seq=8#page_scan_tab_contents" rel="noreferrer">paper</a> by Grädel, Kolaitis and Moshe Vardi, they discuss computational complexity of satisfiability problem in <span class="math-container">$\mathrm{FO^2}$</span>, In order to do this they use Scott's reduction. Which is the fact that any sentence in <span class="math-container">$\mathrm{FO^2}$</span> can be reduced to Scott's Normal form in polynomial time. The Scott's Normal form is given as
<span class="math-container">$$\forall x \forall y \alpha(x,y) \land \bigwedge_{i=1}^{m} \forall x \exists y \beta_{i}(x,y) $$</span>
Does anyone know of existing code base where scott's reduction is implemented, i.e I input an arbitrary <span class="math-container">$\mathrm{FO^2}$</span> sentence and get it's Scott's Normal Form?</p>

<reductions><first-order-logic>
Existing implementation of Scott's reduction?
SagarM
# Existing implementation of Scott's reduction?

(Asked by: username_0 on 2020-07-30)

As per this [paper](https://www.jstor.org/stable/421196?read-now=1&seq=8#page_scan_tab_contents) 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?

**Tags:** reductions, first-order-logic


---

## 1 answers

### Answer by username_1 on 2020-07-30. Score: 11 | Accepted answer

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>


---

