Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On two-variable guarded fragment logic with expressive local Presburger constraints

Chia-Hsuan Lu, Tony Tan

TL;DR

The paper extends GF^2 by introducing GP^2, a two-variable guarded fragment with local Presburger quantifiers that express linear counting constraints around elements. It presents a graph-based, deterministic exponential-time algorithm to decide satisfiability, achieving EXP-completeness by combining a lower bound from GC^2 with a novel elimination-based upper bound, and it contrasts its approach with tableau-based methods like BF22. By encoding models as type graphs and reducing satisfiability to the existence of a good subgraph, the work provides a concrete, graph-centric method for handling numeric neighbourhood constraints within guarded fragments. The results have implications for description logics with counting, offering a precise complexity characterization and a practical decision procedure that avoids exponential branching inherent in tableaux, while highlighting avenues for finite-model analysis and further comparisons with related techniques.

Abstract

We consider the extension of the two-variable guarded fragment logic with local Presburger quantifiers. These are quantifiers that can express properties such as "the number of incoming blue edges plus twice the number of outgoing red edges is at most three times the number of incoming green edges" and captures various description logics with counting, but without constant symbols. We show that the satisfiability problem for this logic is EXP-complete. While the lower bound already holds for the standard two-variable guarded fragment logic, the upper bound is established by a novel, yet simple deterministic graph-based algorithm.

On two-variable guarded fragment logic with expressive local Presburger constraints

TL;DR

The paper extends GF^2 by introducing GP^2, a two-variable guarded fragment with local Presburger quantifiers that express linear counting constraints around elements. It presents a graph-based, deterministic exponential-time algorithm to decide satisfiability, achieving EXP-completeness by combining a lower bound from GC^2 with a novel elimination-based upper bound, and it contrasts its approach with tableau-based methods like BF22. By encoding models as type graphs and reducing satisfiability to the existence of a good subgraph, the work provides a concrete, graph-centric method for handling numeric neighbourhood constraints within guarded fragments. The results have implications for description logics with counting, offering a precise complexity characterization and a practical decision procedure that avoids exponential branching inherent in tableaux, while highlighting avenues for finite-model analysis and further comparisons with related techniques.

Abstract

We consider the extension of the two-variable guarded fragment logic with local Presburger quantifiers. These are quantifiers that can express properties such as "the number of incoming blue edges plus twice the number of outgoing red edges is at most three times the number of incoming green edges" and captures various description logics with counting, but without constant symbols. We show that the satisfiability problem for this logic is EXP-complete. While the lower bound already holds for the standard two-variable guarded fragment logic, the upper bound is established by a novel, yet simple deterministic graph-based algorithm.
Paper Structure (10 sections, 10 theorems, 24 equations)

This paper contains 10 sections, 10 theorems, 24 equations.

Table of Contents

  1. Introduction
  2. Presburger arithmetic
  3. Two-variable guarded fragment with local Presburger quantifiers GP²
  4. The satisfiability of GP² with arithmetic over 𝔑∞
  5. Terminology
  6. The characterisation of the satisfiability of Ψ
  7. The algorithm
  8. The complexity analysis of Algorithm \ref{['alg:gp2']}
  9. Comparison with the approach by Bednarczyk and Fiuk [BF22]
  10. Concluding remarks

Key Result

Theorem 2.1

There are constants $c_1,c_2\in \mathbb{N}$ such that for every system $\mathcal{C}$ of linear constraints, the following holds where $t=|\mathcal{C}|$ and $M$ is the maximal coefficient in $\mathcal{C}$.The results by Eisenbrand and Shmonin caratheodory-integer and Papadimitriou papa-ilp are stated

Theorems & Definitions (27)

  • Theorem 2.1
  • Corollary 2.2
  • proof
  • Corollary 2.3
  • Remark 3.1
  • Remark 3.2
  • Lemma 3.3
  • proof
  • Remark 3.4
  • Definition 4.1
  • ...and 17 more