2
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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)

$\endgroup$
2
$\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 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.

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

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.