{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T02:34:36Z","timestamp":1774060476171,"version":"3.50.1"},"reference-count":22,"publisher":"Oxford University Press (OUP)","issue":"1","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Logic Computation"],"published-print":{"date-parts":[[2017,2]]},"DOI":"10.1093\/logcom\/exv059","type":"journal-article","created":{"date-parts":[[2015,9,9]],"date-time":"2015-09-09T01:04:11Z","timestamp":1441760651000},"page":"109-128","source":"Crossref","is-referenced-by-count":5,"title":["Boolean unification with predicates"],"prefix":"10.1093","volume":"27","author":[{"given":"Sebastian","family":"Eberhard","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Hetzl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Weller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2015,9,8]]},"reference":[{"key":"2017012307250551000_27.1.109.1","doi-asserted-by":"crossref","unstructured":"Ackermann W. Untersuchungen \u00fcber das Eliminationsproblem der mathematischen Logik. Mathematische Annalen, 390\u2013413, 1935.","DOI":"10.1007\/BF01448035"},{"key":"2017012307250551000_27.1.109.2","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(98)00106-9"},{"key":"2017012307250551000_27.1.109.3","doi-asserted-by":"crossref","unstructured":"Baader F. Nipkow T. Term Rewriting and All That. Cambridge University Press, 1998.","DOI":"10.1017\/CBO9781139172752"},{"key":"2017012307250551000_27.1.109.4","doi-asserted-by":"crossref","unstructured":"Baader F. Snyder W. Robinson A. Voronkov A. Unification theory. In Handbook of Automated Reasoning, pp. 445\u2013532. 2001.","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"key":"2017012307250551000_27.1.109.5","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(87)80065-2"},{"key":"2017012307250551000_27.1.109.6","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005722130532"},{"key":"2017012307250551000_27.1.109.7","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2015.01.002"},{"key":"2017012307250551000_27.1.109.8","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.72.8.2877"},{"key":"2017012307250551000_27.1.109.9","unstructured":"Gabbay D. M. Ohlbach H. J. Nebel B. Rich C. Swartout W. Quantifier elimination in second\u2013order predicate logic. In Principles of Knowledge Representation and Reasoning (KR92), pp. 425\u2013435. Morgan Kaufmann, 1992."},{"key":"2017012307250551000_27.1.109.10","unstructured":"Gabbay D. M. Schmidt R. A. Sza\u0142as A. Second-Order Quantifier Elimination. College Publications, 2008."},{"key":"2017012307250551000_27.1.109.11","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2008.10.005"},{"key":"2017012307250551000_27.1.109.12","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","article-title":"The undecidability of the second-order unification problem","volume":"13","author":"Goldfarb","year":"1981","journal-title":"Theoretical Computer Science"},{"key":"2017012307250551000_27.1.109.13","doi-asserted-by":"crossref","unstructured":"Hetzl S. Leitsch A. Reis G. Tapolczai J. Weller D. Introducing quantified cuts in logic with equality. In IJCAR. Vol. 8562 of LNCS , pp. 240\u2013254, 2014.","DOI":"10.1007\/978-3-319-08587-6_17"},{"key":"2017012307250551000_27.1.109.14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tcs.2014.05.018","article-title":"Algorithmic introduction of quantified cuts","volume":"549","author":"Hetzl","year":"2014","journal-title":"Theoretical Computer Science"},{"key":"2017012307250551000_27.1.109.15","doi-asserted-by":"crossref","unstructured":"Hetzl S. Leitsch A. Weller D. Towards Algorithmic Cut-Introduction. In Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18). Vol. 7180 of Lecture Notes in Computer Science , pp. 228\u2013242. Springer, 2012.","DOI":"10.1007\/978-3-642-28717-6_19"},{"key":"2017012307250551000_27.1.109.16","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80013-6"},{"key":"2017012307250551000_27.1.109.17","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/BF00297246","article-title":"Unification in boolean rings","volume":"4","author":"Martin","year":"1989","journal-title":"Journal of Automated Reasoning"},{"key":"2017012307250551000_27.1.109.18","unstructured":"Papadimitriou C. H. Computational Complexity. Addison-Wesley, 1994."},{"key":"2017012307250551000_27.1.109.19","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1145\/321160.321166","article-title":"A machine oriented logic based on the resolution principle","volume":"10","author":"Robinson","year":"1965","journal-title":"Journal of the ACM"},{"key":"2017012307250551000_27.1.109.20","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/12.6.929"},{"key":"2017012307250551000_27.1.109.21","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2001.0438"},{"key":"2017012307250551000_27.1.109.22","unstructured":"Sipser M. Introduction to the Theory of Computation, 2nd edn., Thomson, 2006."}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/27\/1\/109\/9688747\/exv059.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,30]],"date-time":"2019-08-30T08:32:31Z","timestamp":1567153951000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article-lookup\/doi\/10.1093\/logcom\/exv059"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9,8]]},"references-count":22,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2017,1,23]]},"published-print":{"date-parts":[[2017,2]]}},"alternative-id":["10.1093\/logcom\/exv059"],"URL":"https:\/\/doi.org\/10.1093\/logcom\/exv059","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,9,8]]}}}