{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:05Z","timestamp":1772164085517,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004359","name":"Vetenskapsr\u00e5det","doi-asserted-by":"publisher","award":["GenPro D0497701"],"award-info":[{"award-number":["GenPro D0497701"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["eVeS: Reasoning for Verification and Security"],"award-info":[{"award-number":["eVeS: Reasoning for Verification and Security"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["Starting Grant 2014 - SYMCAR 639270"],"award-info":[{"award-number":["Starting Grant 2014 - SYMCAR 639270"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004063","name":"Knut och Alice Wallenbergs Stiftelse","doi-asserted-by":"publisher","award":["Wallenberg Academy Fellowship 2014 TheProSE"],"award-info":[{"award-number":["Wallenberg Academy Fellowship 2014 TheProSE"]}],"id":[{"id":"10.13039\/501100004063","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["RiSE S11409-N23"],"award-info":[{"award-number":["RiSE S11409-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009887","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"260-270","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Coming to terms with quantified reasoning"],"prefix":"10.1145","author":[{"given":"Laura","family":"Kov\u00e1cs","sequence":"first","affiliation":[{"name":"Vienna University of Technology, Austria"}]},{"given":"Simon","family":"Robillard","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[{"name":"University of Manchester, UK \/ Chalmers University of Technology, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190028"},{"key":"e_1_3_2_1_2_1","series-title":"LNCS","volume-title":"CAV","author":"Barrett C.","year":"2011","unstructured":"C. Barrett , C. Conway , M. Deters , L. Hadarean , D. Jovanovic , T. King , A. Reynolds , and C. Tinelli . CVC4 . In CAV , volume 6806 of LNCS . Springer , 2011 . C. Barrett, C. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, and C. Tinelli. CVC4. In CAV, volume 6806 of LNCS. Springer, 2011."},{"key":"e_1_3_2_1_3_1","volume-title":"The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org","author":"Barrett C.","year":"2016","unstructured":"C. Barrett , P. Fontaine , and C. Tinelli . The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org , 2016 . C. Barrett, P. Fontaine, and C. Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016."},{"key":"e_1_3_2_1_5_1","volume-title":"Higher-order program verification as satisfiability modulo theories with algebraic data-types. arXiv preprint arXiv:1306.5264","author":"Bjorner N.","year":"2013","unstructured":"N. Bjorner , K. McMillan , and A. Rybalchenko . Higher-order program verification as satisfiability modulo theories with algebraic data-types. arXiv preprint arXiv:1306.5264 , 2013 . N. Bjorner, K. McMillan, and A. Rybalchenko. Higher-order program verification as satisfiability modulo theories with algebraic data-types. arXiv preprint arXiv:1306.5264, 2013."},{"key":"e_1_3_2_1_6_1","volume-title":"Extending Sledgehammer with SMT solvers. Automated Deduction\u2013Cade-23, 6803: 116\u2013130","author":"Blanchette J. C.","year":"2013","unstructured":"J. C. Blanchette , S. B\u00f6hme , and L. C. Paulson . Extending Sledgehammer with SMT solvers. Automated Deduction\u2013Cade-23, 6803: 116\u2013130 , 2013 . J. C. Blanchette, S. B\u00f6hme, and L. C. Paulson. Extending Sledgehammer with SMT solvers. Automated Deduction\u2013Cade-23, 6803:116\u2013130, 2013."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_27"},{"key":"e_1_3_2_1_8_1","volume-title":"Springer","author":"Clark K. L.","year":"1978","unstructured":"K. L. Clark . Negation as failure. In Logic and data bases, pages 293\u2013322 . Springer , 1978 . K. L. Clark. Negation as failure. In Logic and data bases, pages 293\u2013322. Springer, 1978."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/647487.726658"},{"key":"e_1_3_2_1_11_1","volume-title":"Fundamental properties of infinite trees. Theoretical computer science, 25(2):95\u2013169","author":"Courcelle B.","year":"1983","unstructured":"B. Courcelle . Fundamental properties of infinite trees. Theoretical computer science, 25(2):95\u2013169 , 1983 . B. Courcelle. Fundamental properties of infinite trees. Theoretical computer science, 25(2):95\u2013169, 1983."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_2_1_14_1","series-title":"LNCS","first-page":"340","volume-title":"TACAS","author":"de Moura L. M.","unstructured":"L. M. de Moura and N. Bj\u00f8rner . Z3: An Efficient SMT Solver . In TACAS , volume 4963 of LNCS , pages 337\u2013 340 . Springer, 2008. L. M. de Moura and N. Bj\u00f8rner. Z3: An Efficient SMT Solver. In TACAS, volume 4963 of LNCS, pages 337\u2013340. Springer, 2008."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0062837"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321997"},{"key":"e_1_3_2_1_17_1","volume-title":"Universit\u00e9 de Paris","author":"Herbrand J.","year":"1930","unstructured":"J. Herbrand . Recherches sur la th\u00e9orie de la d\u00e9monstration. PhD thesis , Universit\u00e9 de Paris , 1930 . J. Herbrand. Recherches sur la th\u00e9orie de la d\u00e9monstration. PhD thesis, Universit\u00e9 de Paris, 1930."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511551574"},{"key":"e_1_3_2_1_19_1","volume-title":"Universit\u00e9 Paris VII","author":"Huet G.","year":"1976","unstructured":"G. Huet . R\u00e9solution d\u2019\u00e9quations dans des langages d\u2019ordre 1, 2... PhD thesis , Universit\u00e9 Paris VII , 1976 . G. Huet. R\u00e9solution d\u2019\u00e9quations dans des langages d\u2019ordre 1, 2... PhD thesis, Universit\u00e9 Paris VII, 1976."},{"key":"e_1_3_2_1_20_1","series-title":"Lecture Notes in Computer Science","first-page":"237","volume-title":"Computer Science Logic","author":"Korovin K.","unstructured":"K. Korovin and A. Voronkov . Integrating linear arithmetic into superposition calculus . In Computer Science Logic , volume 4646 of Lecture Notes in Computer Science , pages 223\u2013 237 . Srpinger, 2007. K. Korovin and A. Voronkov. Integrating linear arithmetic into superposition calculus. In Computer Science Logic, volume 4646 of Lecture Notes in Computer Science, pages 223\u2013237. Srpinger, 2007."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"e_1_3_2_1_22_1","first-page":"357","volume-title":"Proceedings of the Third Annual Symposium onLogic in Computer Science","author":"Maher M. J.","unstructured":"M. J. Maher . Complete axiomatizations of the algebras of finite, rational and infinite trees . In Proceedings of the Third Annual Symposium onLogic in Computer Science , pages 348\u2013 357 . IEEE Computer Society, 1988. M. J. Maher. Complete axiomatizations of the algebras of finite, rational and infinite trees. In Proceedings of the Third Annual Symposium onLogic in Computer Science, pages 348\u2013357. IEEE Computer Society, 1988."},{"key":"e_1_3_2_1_23_1","first-page":"729","article-title":"Axiomatizable classes of locally free algebras of certain types","volume":"3","author":"Mal\u2019cev A. I.","year":"1962","unstructured":"A. I. Mal\u2019cev . Axiomatizable classes of locally free algebras of certain types . Sibirsk. Mat. Zh , 3 : 729 \u2013 743 , 1962 . A. I. Mal\u2019cev. Axiomatizable classes of locally free algebras of certain types. Sibirsk. Mat. Zh, 3:729\u2013743, 1962.","journal-title":"Sibirsk. Mat. Zh"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357169"},{"key":"e_1_3_2_1_25_1","first-page":"443","volume-title":"Handbook of Automated Reasoning","author":"Nieuwenhuis R.","unstructured":"R. Nieuwenhuis and A. Rubio . Paramodulation-Based Theorem Proving . In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning , volume I , chapter 7, pages 371\u2013 443 . Elsevier Science, 2001. R. Nieuwenhuis and A. Rubio. Paramodulation-Based Theorem Proving. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 7, pages 371\u2013443. Elsevier Science, 2001."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/800113.803646"},{"key":"e_1_3_2_1_28_1","series-title":"LNCS","first-page":"213","volume-title":"Automated Deduction\u2013CADE-25","author":"Reynolds A.","unstructured":"A. Reynolds and J. C. Blanchette . A decision procedure for (co)datatypes in SMT solvers . In Automated Deduction\u2013CADE-25 , volume 9195 of LNCS , pages 197\u2013 213 . Springer, 2015. A. Reynolds and J. C. Blanchette. A decision procedure for (co)datatypes in SMT solvers. In Automated Deduction\u2013CADE-25, volume 9195 of LNCS, pages 197\u2013213. Springer, 2015."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/371316.371494"},{"issue":"2","key":"e_1_3_2_1_31_1","first-page":"111","article-title":"a brainiac theorem prover","volume":"15","author":"Schulz S.","year":"2002","unstructured":"S. Schulz . E - a brainiac theorem prover . AI Communications , 15 ( 2-3 ): 111 \u2013 126 , 2002 . S. Schulz. E - a brainiac theorem prover. AI Communications, 15(2-3): 111\u2013126, 2002.","journal-title":"AI Communications"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/23005.24037"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/275487.275515"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429121"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009887","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009887","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:05:34Z","timestamp":1750259134000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009887"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":31,"alternative-id":["10.1145\/3009837.3009887","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009887","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009887","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}