Help Privacy Policy Disclaimer
  Advanced SearchBrowse





On Generalizing Decidable Standard Prefix Classes of First-Order Logic


Voigt,  Marco
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (public)

(Preprint), 455KB

Supplementary Material (public)
There is no public supplementary material available

Voigt, M. (2017). On Generalizing Decidable Standard Prefix Classes of First-Order Logic. Retrieved from http://arxiv.org/abs/1706.03949.

Cite as: http://hdl.handle.net/21.11116/0000-0002-EFAE-E
Recently, the separated fragment (SF) of first-order logic has been introduced. Its defining principle is that universally and existentially quantified variables may not occur together in atoms. SF properly generalizes both the Bernays-Sch\"onfinkel-Ramsey (BSR) fragment and the relational monadic fragment. In this paper the restrictions on variable occurrences in SF sentences are relaxed such that universally and existentially quantified variables may occur together in the same atom under certain conditions. Still, satisfiability can be decided. This result is established in two ways: firstly, by an effective equivalence-preserving translation into the BSR fragment, and, secondly, by a model-theoretic argument. Slight modifications to the described concepts facilitate the definition of other decidable classes of first-order sentences. The paper presents a second fragment which is novel, has a decidable satisfiability problem, and properly contains the Ackermann fragment and---once more---the relational monadic fragment. The definition is again characterized by restrictions on the occurrences of variables in atoms. More precisely, after certain transformations, Skolemization yields only unary functions and constants, and every atom contains at most one universally quantified variable. An effective satisfiability-preserving translation into the monadic fragment is devised and employed to prove decidability of the associated satisfiability problem.