6533b86efe1ef96bd12cb1d8

RESEARCH PRODUCT

On Finite Satisfiability of Two-Variable First-Order Logic with Equivalence Relations

Lidia TenderaEmanuel Kieronski

subject

Nondeterministic algorithmDiscrete mathematicsTransitive relationLogical equivalenceComputer Science::Logic in Computer SciencePreorderEquivalence relationSatisfiabilityDecidabilityMathematicsFirst-order logic

description

We show that every finitely satisfiable two-variable first-order formula with two equivalence relations has a model of size at most triply exponential with respect to its length. Thus the finite satisfiability problem for two-variable logic over the class of structures with two equivalence relations is decidable in nondeterministic triply exponential time. We also show that replacing one of the equivalence relations in the considered class of structures by a relation which is only required to be transitive leads to undecidability. This sharpens the earlier result that two-variable logic is undecidable over the class of structures with two transitive relations.

yearjournalcountryeditionlanguage
2009-08-012009 24th Annual IEEE Symposium on Logic In Computer Science
https://doi.org/10.1109/lics.2009.39