English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Paper

Deciding First-Order Satisfiability when Universal and Existential Variables are Separated

MPS-Authors
/persons/resource/persons73108

Sturm,  Thomas
Automation of Logic, MPI for Informatics, Max Planck Society;

/persons/resource/persons101767

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

/persons/resource/persons45719

Weidenbach,  Christoph
Automation of Logic, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

arXiv:1511.08999.pdf
(Preprint), 340KB

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

Sturm, T., Voigt, M., & Weidenbach, C. (2016). Deciding First-Order Satisfiability when Universal and Existential Variables are Separated. Retrieved from http://arxiv.org/abs/1511.08999.


Cite as: https://hdl.handle.net/11858/00-001M-0000-002C-4377-6
Abstract
We introduce a new decidable fragment of first-order logic with equality, which strictly generalizes two already well-known ones -- the Bernays-Sch\"onfinkel-Ramsey (BSR) Fragment and the Monadic Fragment. The defining principle is the syntactic separation of universally quantified variables from existentially quantified ones at the level of atoms. Thus, our classification neither rests on restrictions on quantifier prefixes (as in the BSR case) nor on restrictions on the arity of predicate symbols (as in the monadic case). We demonstrate that the new fragment exhibits the finite model property and derive a non-elementary upper bound on the computing time required for deciding satisfiability in the new fragment. For the subfragment of prenex sentences with the quantifier prefix $\exists^* \forall^* \exists^*$ the satisfiability problem is shown to be complete for NEXPTIME. Finally, we discuss how automated reasoning procedures can take advantage of our results.