Finite satisfiability for two-variable, first-order logic with one transitive relation is decidable

摘要

We consider two-variable, first-order logic in which a single distinguished predicate is required to be interpreted as a transitive relation.We showthat the finite satisfiability problem for this logic is decidable in triply exponential non-deterministic time. Complexity falls to doubly exponential non-deterministic time if the transitive relation is constrained to be a partial order.