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 show that 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.