Two-variable logic with two order relations

DOI10.2168/LMCS-8(1:15)2012MaRDI QIDQ5891508zbMATH OpenFDO

Authors Thomas Schwentick, Thomas Zeume

Publication date 3 April 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1110.1439

zbMATH Keywords

data wordlinear orderstwo-variable logic

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70) Complexity of computation (including implicit computational complexity) (03D15) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25)

Abstract: It is shown that the finite satisfiability problem for two-variable logic over structures with one total preorder relation, its induced successor relation, one linear order relation and some further unary relations is EXPSPACE-complete. Actually, EXPSPACE-completeness already holds for structures that do not include the induced successor relation. As a special case, the EXPSPACE upper bound applies to two-variable logic over structures with two linear orders. A further consequence is that satisfiability of two-variable logic over data words with a linear order on positions and a linear order and successor relation on the data is decidable in EXPSPACE. As a complementing result, it is shown that over structures with two total preorder relations as well as over structures with one total preorder and two linear order relations, the finite satisfiability problem for two-variable logic is undecidable.

Recommendations

• Two-variable logic with two order relations (extended abstract)
• Two-variable logic on 2-dimensional structures
• Decidability issues for two-variable logics with several linear orders
• Two-variable logic with counting and a linear order
• Two variable first-order logic over ordered domains

Cited in

(18)

• Decidability issues for two-variable logics with several linear orders
• Two-variable logic on data words
• Two-Variable Separation Logic and Its Inner Circle
• Two-variable logic on 2-dimensional structures
• Two variables and two successors
• Two-Variable Logic over Countable Linear Orderings
• Two-variable logic with a between relation
• Order-invariance of two-variable logic is decidable
• Register automata with extrema constraints, and an application to two-variable logic
• Finite satisfiability for two‐variable, first‐order logic with one transitive relation is decidable
• Synthesis of data word transducers
• Synthesis of Data Word Transducers
• Two-variable logic with two order relations (extended abstract)
• Church synthesis on register automata over linearly ordered data domains
• Reasoning on data words over numeric domains
• The adjacent fragment and Quine's limits of decision
• Church synthesis on register automata over linearly ordered data domains
• Pebble-intervals automata and \(\text{FO}^2\) with two orders

This page was built for publication: Two-variable logic with two order relations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5891508)