The Finite Satisfiability Problem for Two-Variable, First-Order Logic with one Transitive Relation is Decidable
Logic in Computer Science
2024-04-24 v1
Abstract
We consider the two-variable fragment of first-order logic with one distinguished binary predicate constrained to be interpreted as a transitive relation. The finite satisfiability problem for this logic is shown to be decidable, in triply exponential non-deterministic time. The complexity falls to doubly exponential non-deterministic time if the distinguished binary predicate is constrained to be interpreted as a partial order.
Cite
@article{arxiv.1707.05558,
title = {The Finite Satisfiability Problem for Two-Variable, First-Order Logic with one Transitive Relation is Decidable},
author = {Ian Pratt-Hartmann},
journal= {arXiv preprint arXiv:1707.05558},
year = {2024}
}