Two-Variable First-Order Logic
The two-variable fragment of relational first-order logic, allowing only two reusable variable symbols. Satisfiability is NEXPTIME-complete.
Fragments of First-Order LogicThe directory29 published entries
Welcome to LogicalZoo
Explore formal logics, their expressive power, and their relationships. A growing reference guide from syntax and semantics to decidability and complexity.