Satisfiability of bright formulas

Abstract

We investigate one solvable subclass of quantified formulas in pure predicate calculus and obtain a necessary and sufficient condition for the satisfiability of formulas from this subclass.