Positive First-Order Logic Is NP-Complete
Dexter C. Kozen · IBM Journal of Research and Development · 1981
The decision problem for positive first-order logic with equality is NP-complete. More generally, if Σ is a finite set of atomic sentences (i.e., atomic formulas of the form t1= t2or Rt1… tncontaining no variables) and negations of atomic sentences and if ɸ is a positive first-order sentence, then the problem of determining whether ɸ is true in all models of Σ is NP-complete.