@online{Voigt_arXiv1706.03949,
TITLE = {On Generalizing Decidable Standard Prefix Classes of First-Order Logic},
AUTHOR = {Voigt, Marco},
LANGUAGE = {eng},
URL = {http://arxiv.org/abs/1706.03949},
EPRINT = {1706.03949},
EPRINTTYPE = {arXiv},
YEAR = {2017},
ABSTRACT = {Recently, the separated fragment (SF) of first-order logic has been<br>introduced. Its defining principle is that universally and existentially<br>quantified variables may not occur together in atoms. SF properly generalizes<br>both the Bernays-Sch\"onfinkel-Ramsey (BSR) fragment and the relational monadic<br>fragment. In this paper the restrictions on variable occurrences in SF<br>sentences are relaxed such that universally and existentially quantified<br>variables may occur together in the same atom under certain conditions. Still,<br>satisfiability can be decided. This result is established in two ways: firstly,<br>by an effective equivalence-preserving translation into the BSR fragment, and,<br>secondly, by a model-theoretic argument.<br> Slight modifications to the described concepts facilitate the definition of<br>other decidable classes of first-order sentences. The paper presents a second<br>fragment which is novel, has a decidable satisfiability problem, and properly<br>contains the Ackermann fragment and---once more---the relational monadic<br>fragment. The definition is again characterized by restrictions on the<br>occurrences of variables in atoms. More precisely, after certain<br>transformations, Skolemization yields only unary functions and constants, and<br>every atom contains at most one universally quantified variable. An effective<br>satisfiability-preserving translation into the monadic fragment is devised and<br>employed to prove decidability of the associated satisfiability problem.<br>},
}