Complexity of the Guarded Two-Variable Fragment with Counting Quantifiers

TL;DR

This paper proves that the finite satisfiability problem for the guarded two-variable fragment with counting quantifiers is in EXPTIME, providing a simpler proof and extending understanding of its computational complexity.

Contribution

It offers a new, simplified proof that the satisfiability problem for this logic fragment is in EXPTIME, confirming recent results and enhancing theoretical understanding.

Findings

Finite satisfiability problem is in EXPTIME

Provides a simpler proof of existing results

Extends knowledge of guarded two-variable fragment complexity

Abstract

We show that the finite satisfiability problem for the guarded two-variable fragment with counting quantifiers is in EXPTIME. The method employed also yields a simple proof of a result recently obtained by Y. Kazakov, that the satisfiability problem for the guarded two-variable fragment with counting quantifiers is in EXPTIME.