{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:12:20Z","timestamp":1753884740721,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031384981"},{"type":"electronic","value":"9783031384998"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T00:00:00Z","timestamp":1693612800000},"content-version":"vor","delay-in-days":244,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We show that SCL(FOL) can simulate the derivation of non-redundant clauses by superposition for first-order logic without equality. Superposition-based reasoning is performed with respect to a fixed reduction ordering. The completeness proof of superposition relies on the grounding of the clause set. It builds a ground partial model according to the fixed ordering, where minimal false ground instances of clauses then trigger non-redundant superposition inferences. We define a respective strategy for the SCL calculus such that clauses learned by SCL and superposition inferences coincide. From this perspective the SCL calculus can be viewed as a generalization of the superposition calculus.<\/jats:p>","DOI":"10.1007\/978-3-031-38499-8_8","type":"book-chapter","created":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T23:03:25Z","timestamp":1693609405000},"page":"134-152","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning"],"prefix":"10.1007","author":[{"given":"Martin","family":"Bromberger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chaahat","family":"Jain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,2]]},"reference":[{"issue":"3","key":"8_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1093\/logcom\/4.3.217","volume":"4","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Logic Comput. 4(3), 217\u2013247 (1994). Revised version of Max-Planck-Institut f\u00fcr Informatik technical report, MPI-I-91-208, 1991","journal-title":"J. Logic Comput."},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, chap. 2, pp. 19\u201399. Elsevier, Amsterdam (2001)","DOI":"10.1016\/B978-044450813-3\/50004-7"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"480","DOI":"10.1007\/978-3-030-99524-9_27","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Bromberger","year":"2022","unstructured":"Bromberger, M.: A sorted datalog hammer for supervisor verification conditions modulo simple linear arithmetic. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 480\u2013501. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_27"},{"key":"8_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-030-67067-2_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Bromberger","year":"2021","unstructured":"Bromberger, M., Fiori, A., Weidenbach, C.: Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories. In: Henglein, F., Shoham, S., Vizel, Y. (eds.) VMCAI 2021. LNCS, vol. 12597, pp. 511\u2013533. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-67067-2_23"},{"key":"8_CR5","unstructured":"Bromberger, M., Gehl, T., Leutgeb, L., Weidenbach, C.: A two-watched literal scheme for first-order logic. In: Konev, B., Schon, C., Steen, A. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC\/IJCAR 2022), CEUR Workshop Proceedings, Haifa, Israel, 11\u201312 August 2022, vol. 3201. CEUR-WS.org (2022)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Bromberger, M., Jain, C., Weidenbach, C.: SCL(FOL) can simulate non-redundant superposition clause learning (2023)","DOI":"10.1007\/978-3-031-38499-8_8"},{"key":"8_CR7","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Leutgeb, L., Weidenbach, C.: An efficient subsumption test pipeline for bs(lra) clauses. In: Blanchette, J., Kovacs, L., Pattinson, D. (eds.) Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Held as Part of the Federated Logic Conference, Proceedings. LNCS, vol. 13385, pp. 147\u2013168. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_10","DOI":"10.1007\/978-3-031-10769-6_10"},{"key":"8_CR8","unstructured":"Bromberger, M., Schwarz, S., Weidenbach, C.: Exploring partial models with SCL. In: Konev, B., Schon, C., Steen, A. (eds.) Proceedings of the Workshop on Practical Aspects of Automated Reasoning Co-located with the 11th International Joint Conference on Automated Reasoning (FLoC\/IJCAR 2022), CEUR Workshop Proceedings, Haifa, Israel, 11\u201312 August 2022, vol. 3201 (2022)"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"Bromberger, M., Schwarz, S., Weidenbach, C.: SCL(FOL) revisited (2023). https:\/\/doi.org\/10.48550\/ARXIV.2302.05954. https:\/\/arxiv.org\/abs\/2302.05954","DOI":"10.48550\/ARXIV.2302.05954"},{"key":"8_CR10","unstructured":"Desharnais, M.: A formalization of the SCL(FOL) calculus: Simple clause learning for first-order logic. Archive of Formal Proofs ( 2023). https:\/\/isa-afp.org\/entries\/Simple_Clause_Learning.html, Formal proof development"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-030-29436-6_14","volume-title":"Automated Deduction \u2013 CADE 27","author":"A Fiori","year":"2019","unstructured":"Fiori, A., Weidenbach, C.: SCL clause learning from simple models. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 233\u2013249. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_14"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Korovin, K.: New directions in instatiation-based theorem proving. In: Abramsky, S. (ed.) 18th Annual IEEE Symposium on Logic in Computer Science, LICS 2003, pp. 55\u201364. IEEE Computer Society (2003)","DOI":"10.1109\/LICS.2003.1210045"},{"key":"8_CR13","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"DE Knuth","year":"1970","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Leech, I. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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 (LNAI), vol. 5195, pp. 292\u2013298. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_24"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-37651-1_10","volume-title":"Programming Logics","author":"K Korovin","year":"2013","unstructured":"Korovin, K.: Inst-Gen \u2013 a modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 239\u2013270. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37651-1_10"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-39799-8_1","volume-title":"Computer Aided Verification","author":"L Kov\u00e1cs","year":"2013","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1\u201335. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1"},{"key":"8_CR17","doi-asserted-by":"publisher","unstructured":"Leidinger, H., Weidenbach, C.: SCL(EQ): SCL for first-order logic with equality. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, 8\u201310 August 2022, Proceedings. Lecture Notes in Computer Science, vol. 13385, pp. 228\u2013247. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_14","DOI":"10.1007\/978-3-031-10769-6_14"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, chap. 7, pp. 371\u2013443. Elsevier (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Schlichtkrull, A., Blanchette, J.C., Traytel, D., Waldmann, U.: Formalization of bachmair and ganzinger\u2019s ordered resolution prover. Archive of Formal Proofs (2018). https:\/\/isa-afp.org\/entries\/Ordered_Resolution_Prover.html, Formal proof development","DOI":"10.29007\/pn71"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-030-29436-6_29","volume-title":"Automated Deduction \u2013 CADE 27","author":"S Schulz","year":"2019","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, higher, stronger: E 2.3. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 495\u2013507. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29"},{"key":"8_CR21","doi-asserted-by":"publisher","unstructured":"Waldmann, U., Tourret, S., Robillard, S., Blanchette, J.: A comprehensive framework for saturation theorem proving. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, 1\u20134 July 2020, Proceedings, Part I. Lecture Notes in Computer Science, vol. 12166, pp. 316\u2013334. Springer, Heidelberg (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_18","DOI":"10.1007\/978-3-030-51074-9_18"},{"key":"8_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 140\u2013145. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 29"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-38499-8_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,27]],"date-time":"2024-10-27T10:35:31Z","timestamp":1730025331000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-38499-8_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031384981","9783031384998"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-38499-8_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"2 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rome","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easyconferences.eu\/cade2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"36% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}