{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,22]],"date-time":"2025-06-22T04:04:30Z","timestamp":1750565070543,"version":"3.41.0"},"publisher-location":"Cham","reference-count":29,"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_21","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"344-356","source":"Crossref","is-referenced-by-count":2,"title":["Scavenger 0.1: A Theorem Prover Based on Conflict Resolution"],"prefix":"10.1007","author":[{"given":"Daniyar","family":"Itegulov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Slaney","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruno","family":"Woltzenlogel Paleo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-24246-0_5","volume-title":"Frontiers of Combining Systems","author":"G Alagi","year":"2015","unstructured":"Alagi, G., Weidenbach, C.: NRCL - a model building approach to\u00a0the Bernays-Sch\u00f6nfinkel fragment. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS, vol. 9322, pp. 69\u201384. Springer, Cham (2015). doi: 10.1007\/978-3-319-24246-0_5"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Baumgartner, P.: A first order Davis-Putnam-Longeman-Loveland procedure. In: Proceedings of the 17th International Conference on Automated Deduction (CADE), pp. 200\u2013219 (2000)","DOI":"10.1007\/10721959_16"},{"issue":"1","key":"21_CR3","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1109\/MIS.2013.124","volume":"29","author":"P Baumgartner","year":"2014","unstructured":"Baumgartner, P.: Model evolution-based theorem proving. IEEE Intell. Syst. 29(1), 4\u201310 (2014). http:\/\/dx.doi.org\/10.1109\/MIS.2013.124","journal-title":"IEEE Intell. Syst."},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1007\/11916277_39","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P Baumgartner","year":"2006","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Lemma learning in the model evolution calculus. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS, vol. 4246, pp. 572\u2013586. Springer, Heidelberg (2006). doi: 10.1007\/11916277_39"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-540-45085-6_32","volume-title":"Automated Deduction \u2013 CADE-19","author":"P Baumgartner","year":"2003","unstructured":"Baumgartner, P., Tinelli, C.: The model evolution calculus. In: Baader, F. (ed.) CADE 2003. LNCS, vol. 2741, pp. 350\u2013364. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45085-6_32"},{"key":"21_CR6","unstructured":"Bonacina, M.P., Plaisted, D.A.: Constraint manipulation in SGGS. In: Kutsia, T., Ringeissen, C. (eds.) Proceedings of the Twenty-Eighth Workshop on Unification (UNIF), Seventh International Joint Conference on Automated Reasoning (IJCAR) and Sixth Federated Logic Conference (FLoC), pp. 47\u201354, Technical reports of the Research Institute for Symbolic Computation, Johannes Kepler Universit\u00e4t Linz (2014). http:\/\/vsl2014.at\/meetings\/UNIF-index.html"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Plaisted, D.A.: SGGS theorem proving: an exposition. In: Schulz, S., Moura, L.D., Konev, B. (eds.) Proceedings of the Fourth Workshop on Practical Aspects in Automated Reasoning (PAAR), Seventh International Joint Conference on Automated Reasoning (IJCAR) and Sixth Federated Logic Conference (FLoC), July 2014. EasyChair Proceedings in Computing (EPiC), vol. 31, pp. 25\u201338, July 2015","DOI":"10.29007\/m2vf"},{"issue":"2","key":"21_CR8","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/s10817-015-9334-4","volume":"56","author":"MP Bonacina","year":"2016","unstructured":"Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: model representation. J. Autom. Reasoning 56(2), 113\u2013141 (2016). http:\/\/dx.doi.org\/10.1007\/s10817-015-9334-4","journal-title":"J. Autom. Reasoning"},{"key":"21_CR9","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Plaisted, D.A.: Semantically-guided goal-sensitive reasoning: Inference system and completeness. J. Autom. Reasoning, 1\u201354 (2017). http:\/\/dx.doi.org\/10.1007\/s10817-016-9384-2","DOI":"10.1007\/s10817-016-9384-2"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/978-3-319-08587-6_29","volume-title":"Automated Reasoning","author":"J Boudou","year":"2014","unstructured":"Boudou, J., Fellner, A., Woltzenlogel Paleo, B.: Skeptik: a proof compression system. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 374\u2013380. Springer, Cham (2014). doi: 10.1007\/978-3-319-08587-6_29"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-642-31365-3_11","volume-title":"Automated Reasoning","author":"CE Brown","year":"2012","unstructured":"Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 111\u2013117. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31365-3_11"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Claessen, K.: The anatomy of Equinox - an extensible automated reasoning tool for first-order logic and beyond (talk abstract). In: Proceedings of the 23rd International Conference on Automated Deduction (CADE-23), pp. 1\u20133 (2011)","DOI":"10.1007\/978-3-642-22438-6_1"},{"key":"21_CR13","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM 7, 201\u2013215 (1960)","journal-title":"J. ACM"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Hodgson, K., Slaney, J.K.: System description: SCOTT-5. In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18\u201323, 2001, Proceedings, pp. 443\u2013447 (2001). http:\/\/dx.doi.org\/10.1007\/3-540-45744-5_36","DOI":"10.1007\/3-540-45744-5_36"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008). doi: 10.1007\/978-3-540-71070-7_24"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Korovin, K.: Inst-Gen - a modular approach to instantiation-based automated reasoning. In: Programming Logics, pp. 239\u2013270 (2013)","DOI":"10.1007\/978-3-642-37651-1_10"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/978-3-642-04244-7_41","volume-title":"Principles and Practice of Constraint Programming - CP 2009","author":"K Korovin","year":"2009","unstructured":"Korovin, K., Tsiskaridze, N., Voronkov, A.: Conflict resolution. In: Gent, I.P. (ed.) CP 2009. LNCS, vol. 5732, pp. 509\u2013523. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04244-7_41"},{"key":"21_CR18","doi-asserted-by":"crossref","unstructured":"Jo\u00e3o Marques-Silva, I.L., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 127\u2013149 (2008)","DOI":"10.3233\/978-1-58603-929-5-131"},{"key":"21_CR19","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"57","author":"GL Martin Davis","year":"1962","unstructured":"Martin Davis, G.L., Loveland, D.: A machine program for theorem proving. Commun. ACM 57, 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"key":"21_CR20","first-page":"1","volume":"2","author":"J McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R., Wos, L.: Complexity and related enhancements for automated theorem-proving programs. Comput. Math. Appl. 2, 1\u201316 (1976)","journal-title":"Comput. Math. Appl."},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1007\/3-540-52885-7_131","volume-title":"CADE 1990","author":"W McCune","year":"1990","unstructured":"McCune, W.: Otter 2.0. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 663\u2013664. Springer, Heidelberg (1990). doi: 10.1007\/3-540-52885-7_131"},{"key":"21_CR22","unstructured":"McCune, W.: OTTER 3.3 reference manual. CoRR cs.SC\/0310056 (2003),. http:\/\/arxiv.org\/abs\/cs.SC\/0310056"},{"key":"21_CR23","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Hillenbrand, T., Riazanov, A., Voronkov, A.: On the evaluation of indexing techniques for theorem proving. In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18\u201323, 2001, Proceedings, pp. 257\u2013271 (2001). doi: http:\/\/dx.doi.org\/10.1007\/3-540-45744-5_19","DOI":"10.1007\/3-540-45744-5_19"},{"key":"21_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/11814771_28","volume-title":"Automated Reasoning","author":"H Nivelle","year":"2006","unstructured":"Nivelle, H., Meng, J.: Geometric resolution: a proof procedure based on finite model search. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS, vol. 4130, pp. 303\u2013317. Springer, Heidelberg (2006). doi: 10.1007\/11814771_28"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Slaney, J., Woltzenlogel Paleo, B.: Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning. J. Autom. Reasoning, 1\u201324 (2017). http:\/\/dx.doi.org\/10.1007\/s10817-017-9408-6","DOI":"10.1007\/s10817-017-9408-6"},{"key":"21_CR26","unstructured":"Slaney, J.K.: SCOTT: a model-guided theorem prover. In: Bajcsy, R. (ed.) Proceedings of the 13th International Joint Conference on Artificial Intelligence. Chamb\u00e9ry, France, August 28 - September 3, 1993, pp. 109\u2013115. Morgan Kaufmann (1993). http:\/\/ijcai.org\/Proceedings\/93-1\/Papers\/016.pdf"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning","author":"A Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 367\u2013373. Springer, Cham (2014). doi: 10.1007\/978-3-319-08587-6_28"},{"issue":"4","key":"21_CR28","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reasoning 43(4), 337\u2013362 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"21_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-319-08867-9_46","volume-title":"Computer Aided Verification","author":"A Voronkov","year":"2014","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696\u2013710. Springer, Cham (2014). doi: 10.1007\/978-3-319-08867-9_46"}],"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_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,21]],"date-time":"2025-06-21T19:24:53Z","timestamp":1750533893000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}