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

DOI10.1145/2933575.2934532zbMath1394.03013arXiv1511.08999OpenAlexW3102630320MaRDI QIDQ4635864

Christoph Weidenbach, Thomas Sturm, Marco Voigt

Publication date: 23 April 2018

Published in: Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1511.08999

zbMATH Keywords

finite model propertymonadic fragmentBernays-Schönfinkel-Ramsey fragmentdecidable first-order fragment

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items (3)

Data Centric Workflows for Crowdsourcing ⋮ On the complexity of team logic and its two-variable fragment ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates

This page was built for publication: Deciding First-Order Satisfiability when Universal and Existential Variables are Separated