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.

翻译：本文研究了伯奈斯-舍恩芬克尔一阶逻辑类（亦称有效命题逻辑EPR）子片段可满足性问题的计算复杂性。虽然伯奈斯-舍恩芬克尔类具有NEXPTIME完全性，但通过将子句限制为DET-HORN或KROM形式，我们已可获得具有PSPACE完全性的片段。然而此类限制产生的公式，与经典的PSPACE完全语言——量化布尔公式（QBF）存在显著差异。尽管伯奈斯-舍恩芬克尔类与QBF的扩展形式——依赖量化布尔公式存在天然联系。我们的主要贡献在于：通过QBF的转换定义了一个PSPACE完全的伯奈斯-舍恩芬克尔子片段，该片段保留了类似的双参与者博弈语义评估机制，并能通过不同限制方式获得其他完全性问题，特别是多项式谱系中不同层级的问题。基于此定义，我们识别了TPTP库中属于该片段的问题及其在多项式谱系中的层级。