6533b88afe1ef96bd12e2486
RESEARCH PRODUCT
FO^2 with one transitive relation is decidable
Szwast, WieslawTendera, Lidiasubject
Data processing Computer scienceclassical decision problem two-variable first-order logic decidability computational complexityddc:004Computer Science::Formal Languages and Automata Theorydescription
We show that the satisfiability problem for the two-variable first-order logic, FO^2, over transitive structures when only one relation is required to be transitive, is decidable. The result is optimal, as FO^2 over structures with two transitive relations, or with one transitive and one equivalence relation, are known to be undecidable, so in fact, our result completes the classification of FO^2-logics over transitive structures with respect to decidability. We show that the satisfiability problem is in 2-NExpTime. Decidability of the finite satisfiability problem remains open.
| year | journal | country | edition | language |
|---|---|---|---|---|
| 2013-01-01 |