Satisfiability for two-variable logic with two successor relations on finite linear orders

2012/04/11 by Diego Figueira, Figueira, Diego
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.1204.2495

openalex publication_date 2012/04/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

We study the finitary satisfiability problem for first order logic with two variables and two binary relations, corresponding to the induced successor relations of two finite linear orders. We show that the problem is decidable in NEXPTIME.

Citations

• On Representatives of Subsets

Related

• A Short Note on Two-Variable Logic with a Linear Order Successor and a Preorder Successor
• Order-Invariance of Two-Variable Logic is Decidable
• Two-Variable Logic for Hierarchically Partitioned and Ordered Data
• On the satisfiability problem for fragments of the two-variable logic with one transitive relation
• Order-Invariance in the Two-Variable Fragment of First-Order Logic