Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Homogeneous Model of Fluted Languages

Daumantas Kojelis

TL;DR

This paper studies the fluted fragment of first-order logic with periodic counting (FLPC) and proves that satisfiable FLPC sentences admit globally or locally homogeneous models, enabling a novel decision framework. By reducing model construction to solving linear Diophantine inequations in the two-variable case and extending to local homogeneity for higher arities, the authors establish that the finite satisfiability problem for FLPC^2 is in $N\mathrm{ExpTime}$ and that the finite satisfiability for FLPC^{\ell+1} lies in $\ell$-NExpTime, culminating in Tower-complete complexity for FLPC. The work also presents undecidability results for counting extensions with reversed relations, via reductions from Hilbert’s 10th problem and tiling problems, with $\Sigma^0_1$-hardness for finite satisfiability of FLC^3_{rev} and higher hardness for FLPC^4_{rev}. Together, these results delineate the boundaries of decidability for multi-variable logics with counting, and introduce homogeneous-model techniques that simplify analysis for FLPC and related fragments, with potential implications for description logics and their counting extensions.

Abstract

We study the fluted fragment of first-order logic which is often viewed as a multi-variable non-guarded extension to various systems of description logics lacking role-inverses. In this paper we show that satisfiable fluted sentences (even under reasonable extensions) admit special kinds of ``nice'' models which we call globally/locally homogeneous. Homogeneous models allow us to simplify methods for analysing fluted logics with counting quantifiers and establish a novel result for the decidability of the (finite) satisfiability problem for the fluted fragment with periodic counting. More specifically, we will show that the (finite) satisfiability problem for the language is ${\rm T{\small OWER}}$-complete. If only two variable are used, computational complexity drops to ${\rm NE{\small XP}T{\small IME}}$-completeness. We supplement our findings by showing that generalisations of fluted logics, such as the adjacent fragment, have finite and general satisfiability problems which are, respectively, $Π^0_1$- and $Σ^0_1$-complete. Additionally, satisfiability becomes $Σ^1_1$-complete if periodic counting quantifiers are permitted.

On Homogeneous Model of Fluted Languages

TL;DR

This paper studies the fluted fragment of first-order logic with periodic counting (FLPC) and proves that satisfiable FLPC sentences admit globally or locally homogeneous models, enabling a novel decision framework. By reducing model construction to solving linear Diophantine inequations in the two-variable case and extending to local homogeneity for higher arities, the authors establish that the finite satisfiability problem for FLPC^2 is in and that the finite satisfiability for FLPC^{\ell+1} lies in -NExpTime, culminating in Tower-complete complexity for FLPC. The work also presents undecidability results for counting extensions with reversed relations, via reductions from Hilbert’s 10th problem and tiling problems, with -hardness for finite satisfiability of FLC^3_{rev} and higher hardness for FLPC^4_{rev}. Together, these results delineate the boundaries of decidability for multi-variable logics with counting, and introduce homogeneous-model techniques that simplify analysis for FLPC and related fragments, with potential implications for description logics and their counting extensions.

Abstract

We study the fluted fragment of first-order logic which is often viewed as a multi-variable non-guarded extension to various systems of description logics lacking role-inverses. In this paper we show that satisfiable fluted sentences (even under reasonable extensions) admit special kinds of ``nice'' models which we call globally/locally homogeneous. Homogeneous models allow us to simplify methods for analysing fluted logics with counting quantifiers and establish a novel result for the decidability of the (finite) satisfiability problem for the fluted fragment with periodic counting. More specifically, we will show that the (finite) satisfiability problem for the language is -complete. If only two variable are used, computational complexity drops to -completeness. We supplement our findings by showing that generalisations of fluted logics, such as the adjacent fragment, have finite and general satisfiability problems which are, respectively, - and -complete. Additionally, satisfiability becomes -complete if periodic counting quantifiers are permitted.

Paper Structure

This paper contains 9 sections, 18 theorems, 32 equations, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. The Two-Variable Sub-fragment
  4. More Than Two Variables
  5. Counting With Reversed Relations
  6. Discussion
  7. Preliminaries
  8. Counting With Reversed Relations
  9. Discussion

Key Result

Lemma 1

Suppose $\varphi$ is an $\mathcal{FLPC}^{\ell{+}1}$-sentence. Then, we may compute, in polynomial time, an equisatisfiable normal-form $\mathcal{FLPC}^{\ell{+}1}$-sentence $\psi$.

Theorems & Definitions (19)

  • Lemma 1
  • Lemma 2
  • Lemma 3
  • Lemma 4
  • Theorem 5
  • Lemma 6
  • Lemma 7
  • Lemma 8
  • Theorem 9
  • Theorem 10
  • ...and 9 more