English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Paper

On Generalizing Decidable Standard Prefix Classes of First-Order Logic

MPS-Authors
/persons/resource/persons101767

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

Locator
There are no locators available
Fulltext (public)

arXiv:1706.03949.pdf
(Preprint), 455KB

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

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
Abstract
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.