<p>Apparently a tableau for <span class="math-container">$FO^2$</span> has not been given explicitly but a tableau for the expressively equivalent description logic <span class="math-container">$ALBO^{id}$</span> has been given in:</p>
<p>Renate Schmidt and Dmitry Tishkovsky, <a href="https://dl.acm.org/doi/10.1145/2559947" rel="nofollow noreferrer"><em>Using Tableau to Decide Description Logics with Full Role Negation and Identity</em></a>,  ACM Trans. Comput. Log. 15(1): 7:1-7:31 (2014)</p>

CC BY-SA 4.0
2021-01-20T16:38:42.920Z
2021-01-20T16:38:42.920Z
Nicola Gigante
<p>You might check the FO2 solver by Tomer Kotek: <a href="https://forsyte.at/alumni/kotek/fo2-solver/" rel="nofollow noreferrer">https://forsyte.at/alumni/kotek/fo2-solver/</a> 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).</p>
<p>I'm not aware of any tableaux algorithm for FO2.</p>

CC BY-SA 4.0
2021-01-17T21:49:46.730Z
Thanks for the pointer! That solver looks interesting
Nicola Gigante
CC BY-SA 4.0
2021-01-18T13:53:27.227Z
Don't you know any tableau algorithm even in form of a tableau for some equivalent modal logic?
Nicola Gigante
CC BY-SA 4.0
2021-01-18T14:23:34.067Z
I'm not aware of any such Tableaux. FO2 is equivalent to the description logic ALCIOB. (or ALCIObHself extended with role negation). So I would recommend you to take a look at them.
Bartosz Bednarczyk
CC BY-SA 4.0
2021-01-18T15:01:51.400Z
I'm not an expert of description logics: does B stand for Boolean connectives over roles?
Nicola Gigante
CC BY-SA 4.0
2021-01-18T15:27:56.177Z
Yes. And small b stand for guarded combinations of roles. (so you cannot fully negate)
Bartosz Bednarczyk
CC BY-SA 4.0
2021-01-18T15:29:53.750Z
Thanks, so according to http://www.cs.man.ac.uk/~ezolin/dl/, ALCB is already NEXPTIME-complete (without I and O). Is it still equivalent to $FO^2$?
Nicola Gigante
CC BY-SA 4.0
2021-01-18T16:08:26.957Z
No, ALCB is not equivalent to FO2. For example, it cannot state that every red element has an R-predecessor, which can be done with \forall{x} red(x) -> \exists{y} R(y,x)
Bartosz Bednarczyk
CC BY-SA 4.0
2021-01-18T16:10:02.390Z
Ok, so I need inverse roles, i.e. ALCIB. What about O? Are nominals needed?
Nicola Gigante
CC BY-SA 4.0
2021-01-18T21:26:15.833Z
\forall{x} \forall{y} A(x) /\ A(y) => x =y
Bartosz Bednarczyk
CC BY-SA 4.0
2021-01-20T16:39:42.647Z
Thanks to your suggestion, after digging a bit into DLs I've found a tableau for an expressively equivalent description logic (I've added an answer). Thanks!
Nicola Gigante
CC BY-SA 4.0
2021-01-20T20:14:33.550Z
WOW, that's a great news! I was not aware of it
Bartosz Bednarczyk
CC BY-SA 4.0
2021-01-17T20:36:29.803Z
2021-01-20T20:27:28.050Z
2021-01-20T20:27:28.050Z
Bartosz Bednarczyk
<p><span class="math-container">$FO^2$</span>, i.e. two-variable first-order logic, has a NEXPTIME-complete satisfiability problem (see Grädel, Kolaitis and Vardi '97). However, the decidability and complexity of this fragment is proved by that paper in an indirect way, as far as I can tell.</p>
<p>What I need instead is an effective way to solve <span class="math-container">$FO^2$</span> satisfiability. What are the actual algorithms and methods available for this logic?</p>
<p>In particular, I would need a tableau-based method for <span class="math-container">$FO^2$</span> satisfiability. Is there any resource describing such a thing? Has it ever been developed?</p>

<first-order-logic>
Tableau method for two-variable first-order logic
Nicola Gigante
# Tableau method for two-variable first-order logic

(Asked by: username_0 on 2021-01-17)

$FO^2$, i.e. two-variable first-order logic, has a NEXPTIME-complete satisfiability problem (see Grädel, Kolaitis and Vardi '97). However, the decidability and complexity of this fragment is proved by that paper in an indirect way, as far as I can tell.

What I need instead is an effective way to solve $FO^2$ satisfiability. What are the actual algorithms and methods available for this logic?

In particular, I would need a tableau-based method for $FO^2$ satisfiability. Is there any resource describing such a thing? Has it ever been developed?

**Tags:** first-order-logic

---

## 2 answers

### Answer by username_0 on 2021-01-20. Score: 2 | Accepted answer

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*](https://dl.acm.org/doi/10.1145/2559947), ACM Trans. Comput. Log. 15(1): 7:1-7:31 (2014)


---

### Answer by username_1 on 2021-01-17. Score: 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.

> **Comments:**
> **username_0**: Thanks for the pointer! That solver looks interesting  
> **username_0**: Don't you know any tableau algorithm even in form of a tableau for some equivalent modal logic?  
> **username_1**: I'm not aware of any such Tableaux. FO2 is equivalent to the description logic ALCIOB. (or ALCIObHself extended with role negation). So I would recommend you to take a look at them.  
> **username_0**: I'm not an expert of description logics: does B stand for Boolean connectives over roles?  
> **username_1**: Yes. And small b stand for guarded combinations of roles. (so you cannot fully negate)  
> **username_0**: Thanks, so according to http://www.cs.man.ac.uk/~ezolin/dl/, ALCB is already NEXPTIME-complete (without I and O). Is it still equivalent to $FO^2$?  
> **username_1**: No, ALCB is not equivalent to FO2. For example, it cannot state that every red element has an R-predecessor, which can be done with \forall{x} red(x) -> \exists{y} R(y,x)  
> **username_0**: Ok, so I need inverse roles, i.e. ALCIB. What about O? Are nominals needed?  
> **username_1**: \forall{x} \forall{y} A(x) /\ A(y) => x =y  
> **username_0**: Thanks to your suggestion, after digging a bit into DLs I've found a tableau for an expressively equivalent description logic (I've added an answer). Thanks!  
> **username_1**: WOW, that's a great news! I was not aware of it  

---

