{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T09:32:15Z","timestamp":1758274335121,"version":"3.41.0"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_17","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"274-290","source":"Crossref","is-referenced-by-count":7,"title":["A Unifying Principle for Clause Elimination in First-Order Logic"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Kiesl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Suda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"unstructured":"Hoder, K., Khasidashvili, Z., Korovin, K., Voronkov, A.: Preprocessing techniques for first-order clausification. In: Proceedings of the 12th Conference on Formal Methods in Computer-Aided Design (FMCAD 2012). IEEE, pp. 44\u201351 (2012)","key":"17_CR1"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-319-40970-2_22","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"Z Khasidashvili","year":"2016","unstructured":"Khasidashvili, Z., Korovin, K.: Predicate elimination for preprocessing in first-order theorem proving. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 361\u2013372. Springer, Cham (2016). doi: 10.1007\/978-3-319-40970-2_22"},{"key":"17_CR3","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1613\/jair.4694","volume":"53","author":"MJH Heule","year":"2015","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Lonsing, F., Seidl, M., Biere, A.: Clause elimination for SAT and QSAT. J. Artif. Intell. Res. 53, 127\u2013168 (2015)","journal-title":"J. Artif. Intell. Res."},{"key":"17_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-016-9394-0","volume":"58","author":"MJH Heule","year":"2017","unstructured":"Heule, M.J.H., Seidl, M., Biere, A.: Solution validation and extraction for QBF preprocessing. J. Autom. Reasoning 58, 1\u201329 (2017)","journal-title":"J. Autom. Reasoning"},{"doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Covered clause elimination. In: Short Papers for the 17th International Conference on Logic for Programming, Artificial intelligence, and Reasoning (LPAR-17-short), vol. 13. EPiC Series, EasyChair, pp. 41\u201346 (2010)","key":"17_CR5","DOI":"10.29007\/cl8s"},{"doi-asserted-by":"crossref","unstructured":"Heule, M.J.H., J\u00e4rvisalo, M., Biere, A.: Clause elimination procedures for CNF formulas. In: Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), LNCS, vol. 6397, pp. 357\u2013371. Springer, Heidelberg (2010)","key":"17_CR6","DOI":"10.1007\/978-3-642-16242-8_26"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-642-31365-3_28","volume-title":"Automated Reasoning","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Heule, M.J.H., Biere, A.: Inprocessing rules. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 355\u2013370. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31365-3_28"},{"doi-asserted-by":"crossref","unstructured":"Kiesl, B., Suda, M., Seidl, M., Tompits, H., Biere, A.: Blocked clauses in first-order logic. In: Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-21), vol. 46. EPiC Series in Computing, EasyChair, pp. 31\u201348 (2017)","key":"17_CR8","DOI":"10.29007\/c3wq"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-642-12002-2_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M J\u00e4rvisalo","year":"2010","unstructured":"J\u00e4rvisalo, M., Biere, A., Heule, M.: Blocked clause elimination. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 129\u2013144. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-12002-2_10"},{"unstructured":"Biere, A.: Splatz, Lingeling, Plingeling, Treengeling, YalSAT entering the SAT competition 2016. In: Proceedings of SAT Competition 2016 - Solver and Benchmark Descriptions, vol. B-2016-1 of Department of Computer Science Series of Publications B, University of Helsinki, pp. 44\u201345 (2016)","key":"17_CR10"},{"key":"17_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). doi: 10.1007\/978-3-319-09284-3_31"},{"key":"17_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M Fitting","year":"1996","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, New York (1996)","edition":"2"},{"doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press, pp. 19\u201399 (2001)","key":"17_CR13","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"17_CR14","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/S0166-218X(99)00037-2","volume":"96\u201397","author":"O Kullmann","year":"1999","unstructured":"Kullmann, O.: On a generalization of extended resolution. Discrete Appl. Math. 96\u201397, 149\u2013176 (1999)","journal-title":"Discrete Appl. Math."},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-642-22438-6_10","volume-title":"Automated Deduction \u2013 CADE-23","author":"A Biere","year":"2011","unstructured":"Biere, A., Lonsing, F., Seidl, M.: Blocked clause elimination for QBF. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 101\u2013115. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_10"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"418","DOI":"10.1007\/978-3-662-48899-7_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F Lonsing","year":"2015","unstructured":"Lonsing, F., Bacchus, F., Biere, A., Egly, U., Seidl, M.: Enhancing search-based QBF solving by dynamic blocked clause elimination. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 418\u2013433. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48899-7_29"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/11499107_5","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2005","unstructured":"E\u00e9n, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61\u201375. Springer, Heidelberg (2005). doi: 10.1007\/11499107_5"},{"key":"17_CR18","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T19:24:45Z","timestamp":1750533885000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}