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

摘要

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