Reintroducing the Second Player in EPR

TL;DR

This paper introduces a new PSPACE-complete sub-fragment of Bernays-Schoenfinkel logic that extends QBF, maintains a two-player game semantics, and helps classify problems in the polynomial hierarchy.

Contribution

The paper defines a novel PSPACE-complete sub-fragment of Bernays-Schoenfinkel logic extending QBF with a two-player game semantics, enabling classification of problems in the polynomial hierarchy.

Findings

Identified problems in the TPTP library within this fragment.

Established the fragment's correspondence to various levels of the polynomial hierarchy.

Demonstrated the fragment's relation to existing logical and computational frameworks.

Abstract

In this work we investigate the computational complexity of the satisfiability problem of sub-fragments of the Bernays-Schoenfinkel class of first-order logic, also known as EPR (Effectively Propositional). While Bernays-Schoenfinkel is NEXPTIME-complete, we already can obtain fragments that are PSPACE-complete by restricting our clauses to DET-HORN or KROM. However such restrictions yield very different formulas to the canonical PSPACE-complete language of Quantified Boolean Formulas (QBF). This is despite Bernays-Schoenfinkel having a natural connection to an extension of QBF known as Dependency QBF. Our main contribution is the definition of a PSPACE-complete sub-fragment of Bernays-Schoenfinkel that extends from a translation of QBF, retains a similar two-player game evaluation for its semantics and can be restricted in various ways to obtain other complete problems, particularly those at different levels in the polynomial hierarchy. We use this definition to identify problems in the TPTP library that fall into this fragment and their level in the polynomial hierarchy.