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?

Improve this question
$\endgroup$

2 Answers 2

Reset to default
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)

Improve this answer
$\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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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