{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:12:15Z","timestamp":1750306335906,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,7,5]],"date-time":"2016-07-05T00:00:00Z","timestamp":1467676800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,7,5]]},"DOI":"10.1145\/2933575.2934532","type":"proceedings-article","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T13:34:47Z","timestamp":1476452087000},"page":"86-95","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Deciding First-Order Satisfiability when Universal and Existential Variables are Separated"],"prefix":"10.1145","author":[{"given":"Thomas","family":"Sturm","sequence":"first","affiliation":[{"name":"CNRS, LORIA, Inria, and University of Lorraine, Nancy, France, and Max Planck Institute for Informatics, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Voigt","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Informatics, Saarbr\u00fccken, Germany, and Graduate School of Computer Science, Saarland University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[{"name":"Max Planck Institute for Informatics, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,7,5]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_1_1_1","DOI":"10.1007\/978-3-319-24246-0_5"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_2_1","DOI":"10.1007\/11916277_39"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1007\/BF01459101"},{"key":"e_1_3_2_1_4_1","first-page":"25","volume-title":"Workshop on Practical Aspects in Automated Reasoning (PAAR'14)","author":"Bonacina M. P.","year":"2014","unstructured":"M. P. Bonacina and D. A. Plaisted . SGGS Theorem Proving: an Exposition . In Workshop on Practical Aspects in Automated Reasoning (PAAR'14) , EPiC 31, pages 25 -- 38 . EasyChair , 2014 . M. P. Bonacina and D. A. Plaisted. SGGS Theorem Proving: an Exposition. In Workshop on Practical Aspects in Automated Reasoning (PAAR'14), EPiC 31, pages 25--38. EasyChair, 2014."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_5_1","DOI":"10.1007\/978-3-642-59207-2"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.1007\/s10472-013-9337-y"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/978-3-642-16242-8_14","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), LNCS 6397","author":"Charatonik W.","year":"2010","unstructured":"W. Charatonik and P. Witkowski . On the Complexity of the Bernays-- Sch\u00f6nfinkel Class with Datalog . In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), LNCS 6397 , pages 187 -- 201 . Springer , 2010 . W. Charatonik and P. Witkowski. On the Complexity of the Bernays-- Sch\u00f6nfinkel Class with Datalog. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), LNCS 6397, pages 187--201. Springer, 2010."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1007\/s10817-010-9216-8"},{"key":"e_1_3_2_1_9_1","volume-title":"The Decision Problem: Solvable Classes of Quantificational Formulas","author":"Dreben B.","year":"1979","unstructured":"B. Dreben and W. D. Goldfarb . The Decision Problem: Solvable Classes of Quantificational Formulas . Addison-Wesley , 1979 . B. Dreben and W. D. Goldfarb. The Decision Problem: Solvable Classes of Quantificational Formulas. Addison-Wesley, 1979."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_10_1","DOI":"10.1007\/978-1-4757-2355-7"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.5555\/778522.778534"},{"key":"e_1_3_2_1_12_1","first-page":"263","volume-title":"Frontiers of Combining Systems (FroCoS'09), LNCS 5749","author":"Fontaine P.","year":"2009","unstructured":"P. Fontaine . Combinations of theories for decidable fragments of first-order logic . In Frontiers of Combining Systems (FroCoS'09), LNCS 5749 , pages 263 -- 278 , 2009 . P. Fontaine. Combinations of theories for decidable fragments of first-order logic. In Frontiers of Combining Systems (FroCoS'09), LNCS 5749, pages 263--278, 2009."},{"key":"e_1_3_2_1_13_1","first-page":"55","volume-title":"Logic in Computer Science (LICS'03)","author":"Ganzinger H.","year":"2003","unstructured":"H. Ganzinger and K. Korovin . New Directions in Instantiation-Based Theorem Proving . In Logic in Computer Science (LICS'03) , pages 55 -- 64 . IEEE , 2003 . H. Ganzinger and K. Korovin. New Directions in Instantiation-Based Theorem Proving. In Logic in Computer Science (LICS'03), pages 55--64. IEEE, 2003."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_14_1","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_3_2_1_15_1","volume-title":"The Decision Problem for the Logic of Predicates and Operations. Algebra i Logika, 8:284--308","author":"Gurevich Y.","year":"1969","unstructured":"Y. Gurevich . The Decision Problem for the Logic of Predicates and Operations. Algebra i Logika, 8:284--308 , 1969 . Y. Gurevich. The Decision Problem for the Logic of Predicates and Operations. Algebra i Logika, 8:284--308, 1969."},{"key":"e_1_3_2_1_16_1","first-page":"167","volume-title":"Infinistic Methods","author":"Henkin L.","year":"1961","unstructured":"L. Henkin . Some remarks on infinitely long formulas . In Infinistic Methods , pages 167 -- 183 . Pergamon Press , 1961 . L. Henkin. Some remarks on infinitely long formulas. In Infinistic Methods, pages 167--183. Pergamon Press, 1961."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/978-3-642-36675-8_4","volume-title":"Automated Reasoning and Mathematics -- Essays in Memory of William W. McCune, LNCS 7788","author":"Hillenbrand T.","year":"2013","unstructured":"T. Hillenbrand and C. Weidenbach . Superposition for bounded domains . In Automated Reasoning and Mathematics -- Essays in Memory of William W. McCune, LNCS 7788 , pages 68 -- 100 . Springer , 2013 . T. Hillenbrand and C. Weidenbach. Superposition for bounded domains. In Automated Reasoning and Mathematics -- Essays in Memory of William W. McCune, LNCS 7788, pages 68--100. Springer, 2013."},{"key":"e_1_3_2_1_18_1","first-page":"261","volume-title":"Frontiers of Combining Systems (FroCoS'13), LNCS 8152","author":"Korovin K.","year":"2013","unstructured":"K. Korovin . From Resolution and DPLL to Solving Arithmetic Constraints . In Frontiers of Combining Systems (FroCoS'13), LNCS 8152 , pages 261 -- 262 . Springer , 2013 . K. Korovin. From Resolution and DPLL to Solving Arithmetic Constraints. In Frontiers of Combining Systems (FroCoS'13), LNCS 8152, pages 261--262. Springer, 2013."},{"key":"e_1_3_2_1_19_1","first-page":"214","volume-title":"Frontiers of Combining Systems (FroCoS'13), LNCS 8152","author":"Korovin K.","year":"2013","unstructured":"K. Korovin . Non-cyclic Sorts for First-Order Satisfiability . In Frontiers of Combining Systems (FroCoS'13), LNCS 8152 , pages 214 -- 228 , 2013 . K. Korovin. Non-cyclic Sorts for First-Order Satisfiability. In Frontiers of Combining Systems (FroCoS'13), LNCS 8152, pages 214--228, 2013."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_20_1","DOI":"10.1016\/0022-0000(80)90027-6"},{"key":"e_1_3_2_1_21_1","first-page":"563","article-title":"Decidability of the monadic predicate calculus with unary function symbols","volume":"32","author":"L\u00f6b M.","year":"1967","unstructured":"M. L\u00f6b . Decidability of the monadic predicate calculus with unary function symbols . J. Symb. Logic , 32 : 563 , 1967 . M. L\u00f6b. Decidability of the monadic predicate calculus with unary function symbols. J. Symb. Logic, 32:563, 1967.","journal-title":"J. Symb. Logic"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_22_1","DOI":"10.1007\/BF01458217"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_24_1","DOI":"10.1007\/s10817-009-9161-6"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_25_1","DOI":"10.2178\/jsl\/1344862166"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_26_1","DOI":"10.1112\/plms\/s2-30.1.264"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_27_1","DOI":"10.1007\/BF01171114"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_28_1","DOI":"10.1145\/2933575.2934532"},{"key":"e_1_3_2_1_29_1","first-page":"314","volume-title":"Automated Deduction (CADE-16), LNCS 1632","author":"Weidenbach C.","year":"1999","unstructured":"C. Weidenbach . Towards an Automatic Analysis of Security Protocols in First-Order Logic . In Automated Deduction (CADE-16), LNCS 1632 , pages 314 -- 328 , 1999 . C. Weidenbach. Towards an Automatic Analysis of Security Protocols in First-Order Logic. In Automated Deduction (CADE-16), LNCS 1632, pages 314--328, 1999."},{"key":"e_1_3_2_1_30_1","first-page":"366","volume-title":"Frontiers of Combining Systems (FroCoS'09), LNCS 5749","author":"Wies T.","year":"2009","unstructured":"T. Wies , R. Piskac , and V. Kuncak . Combining Theories with Shared Set Operations . In Frontiers of Combining Systems (FroCoS'09), LNCS 5749 , pages 366 -- 382 . Springer , 2009 . T. Wies, R. Piskac, and V. Kuncak. Combining Theories with Shared Set Operations. In Frontiers of Combining Systems (FroCoS'09), LNCS 5749, pages 366--382. Springer, 2009."}],"event":{"sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"],"acronym":"LICS '16","name":"LICS '16: 31st Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"New York NY USA"},"container-title":["Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2933575.2934532","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2933575.2934532","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:54:53Z","timestamp":1750222493000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2933575.2934532"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,7,5]]},"references-count":30,"alternative-id":["10.1145\/2933575.2934532","10.1145\/2933575"],"URL":"https:\/\/doi.org\/10.1145\/2933575.2934532","relation":{},"subject":[],"published":{"date-parts":[[2016,7,5]]},"assertion":[{"value":"2016-07-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}