# Tableau method for two-variable first-order logic

$$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?

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)

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.

• Thanks for the pointer! That solver looks interesting – gigabytes Jan 17 at 21:49
• Don't you know any tableau algorithm even in form of a tableau for some equivalent modal logic? – gigabytes Jan 18 at 13:53
• 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 Jan 18 at 14:23
• I'm not an expert of description logics: does B stand for Boolean connectives over roles? – gigabytes Jan 18 at 15:01
• Yes. And small b stand for guarded combinations of roles. (so you cannot fully negate) – Bartosz Bednarczyk Jan 18 at 15:27