Extending two-variable logic on trees
From MaRDI portal
Abstract: The finite satisfiability problem for the two-variable fragment of first-order logic interpreted over trees was recently shown to be ExpSpace-complete. We consider two extensions of this logic. We show that adding either additional binary symbols or counting quantifiers to the logic does not affect the complexity of the finite satisfiability problem. However, combining the two extensions and adding both binary symbols and counting quantifiers leads to an explosion of this complexity. We also compare the expressive power of the two-variable fragment over trees with its extension with counting quantifiers. It turns out that the two logics are equally expressive, although counting quantifiers do add expressive power in the restricted case of unordered trees.
Recommendations
Cited in
(16)- Modulo-counting quantifiers over finite trees
- Extending \(\mathcal{ALCQIO}\) with trees
- Register automata with extrema constraints, and an application to two-variable logic
- One-Dimensional Logic over Trees
- Modulo counting on words and trees
- Register Automata with Extrema Constraints, and an Application to Two-Variable Logic
- Two-variable first-order logic with counting in forests
- Two-variable logic with counting and trees
- Two-variable logic with counting and trees
- Complexity of two-variable logic on finite trees
- Complexity of two-variable logic on finite trees
- An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
- An auxiliary logic on trees: on the tower-hardness of logics featuring reachability and submodel reasoning
- Lifted inference with tree axioms
- On two-variable first-order logic with a partial order
- The adjacent fragment and Quine's limits of decision
This page was built for publication: Extending two-variable logic on trees
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5111178)
