Adding Path-Functional Dependencies to the Guarded Two-Variable Fragment with Counting

TL;DR

This paper investigates the computational complexity of satisfiability problems in a logical framework that combines guarded two-variable logic with counting and path-functional dependencies, establishing their ExpTime-completeness.

Contribution

It extends the understanding of the logical fragment by incorporating path-functional dependencies and analyzing their impact on satisfiability complexity.

Findings

Satisfiability and finite satisfiability are ExpTime-complete for the extended logic.

The work demonstrates the decidability of the logic with added path-functional dependencies.

Provides a complexity classification for the combined logical framework.

Abstract

The satisfiability and finite satisfiability problems for the two-variable guarded fragment of first-order logic with counting quantifiers, a database, and path-functional dependencies are both ExpTime-complete.