H. Kleine Büning and T. Lettmann, “Classes of first order formulas under various satisfiability definitions,” in 8th International Conference on Automated Deduction, Berlin, Heidelberg, 1986.