{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:13:15Z","timestamp":1767928395544,"version":"3.49.0"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030798758","type":"print"},{"value":"9783030798765","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We prove the SOS strategy for first-order resolution to be refutationally complete on a clause set<jats:italic>N<\/jats:italic>and set-of-support<jats:italic>S<\/jats:italic>if and only if there exists a clause in<jats:italic>S<\/jats:italic>that occurs in a resolution refutation from<jats:inline-formula><jats:alternatives><jats:tex-math>$$N\\cup S$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>N<\/mml:mi><mml:mo>\u222a<\/mml:mo><mml:mi>S<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>. This strictly generalizes and sharpens the original completeness result requiring<jats:italic>N<\/jats:italic>to be satisfiable. The generalized SOS completeness result supports automated reasoning on a new notion of relevance aiming at capturing the support of a clause in the refutation of a clause set. A clause<jats:italic>C<\/jats:italic>is<jats:italic>relevant<\/jats:italic>for refuting a clause set<jats:italic>N<\/jats:italic>if<jats:italic>C<\/jats:italic>occurs in every refutation of<jats:italic>N<\/jats:italic>. The clause<jats:italic>C<\/jats:italic>is<jats:italic>semi-relevant<\/jats:italic>, if it occurs in some refutation, i.e., if there exists an SOS refutation with set-of-support<jats:inline-formula><jats:alternatives><jats:tex-math>$$S = \\{C\\}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>S<\/mml:mi><mml:mo>=<\/mml:mo><mml:mo>{<\/mml:mo><mml:mi>C<\/mml:mi><mml:mo>}<\/mml:mo><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>from<jats:inline-formula><jats:alternatives><jats:tex-math>$$N\\setminus \\{C\\}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>N<\/mml:mi><mml:mo>\\<\/mml:mo><mml:mo>{<\/mml:mo><mml:mi>C<\/mml:mi><mml:mo>}<\/mml:mo><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>. A clause that does not occur in any refutation from<jats:italic>N<\/jats:italic>is<jats:italic>irrelevant<\/jats:italic>, i.e., it is not semi-relevant. Our new notion of relevance separates clauses in a proof that are ultimately needed from clauses that may be replaced by different clauses. In this way it provides insights towards proof explanation in refutations beyond existing notions such as that of an unsatisfiable core.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_19","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"327-343","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5139-4503","authenticated-orcid":false,"given":"Fajar","family":"Haifani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6070-796X","authenticated-orcid":false,"given":"Sophie","family":"Tourret","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6002-0458","authenticated-orcid":false,"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"issue":"1","key":"19_CR1","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1093\/logcom\/exn058","volume":"20","author":"F Baader","year":"2010","unstructured":"Baader, F., Pe\u00f1aloza, R.: Axiom pinpointing in general tableaux. J. Log. Comput. 20(1), 5\u201334 (2010)","journal-title":"J. Log. Comput."},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Journal of Logic and Computation 4(3), 217\u2013247 (1994), revised version of Max-Planck-Institut f\u00fcr Informatik technical report, MPI-I-91-208, 1991","DOI":"10.1093\/logcom\/4.3.217"},{"key":"19_CR3","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/BF01459101","volume":"99","author":"P Bernays","year":"1928","unstructured":"Bernays, P., Sch\u00f6nfinkel, M.: Zum entscheidungsproblem der mathematischen logik. Mathematische Annalen 99, 342\u2013372 (1928)","journal-title":"Mathematische Annalen"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Bourgaux, C., Ozaki, A., Pe\u00f1aloza, R., Predoiu, L.: Provenance for the description logic elhr. In: Bessiere, C. (ed.) Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020. pp. 1862\u20131869. ijcai.org (2020)","DOI":"10.24963\/ijcai.2020\/258"},{"issue":"1","key":"19_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/200836.200838","volume":"42","author":"T Eiter","year":"1995","unstructured":"Eiter, T., Gottlob, G.: The complexity of logic-based abduction. Journal of the ACM 42(1), 3\u201342 (1995)","journal-title":"Journal of the ACM"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Fetzer, C., Weidenbach, C., Wischnewski, P.: Compliance, functional safety and fault detection by formal methods. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10\u201314, 2016, Proceedings, Part II. Lecture Notes in Computer Science, vol. 9953, pp. 626\u2013632 (2016)","DOI":"10.1007\/978-3-319-47169-3_48"},{"key":"19_CR7","unstructured":"Haifani, F., Koopmann, P., Tourret, S., Weidenbach, C.: On a notion of relevance. In: Borgwardt, S., Meyer, T. (eds.) Proceedings of the 33rd International Workshop on Description Logics (DL 2020) co-located with the 17th International Conference on Principles of Knowledge Representation and Reasoning (KR 2020), Online Event [Rhodes, Greece], September 12th to 14th, 2020. CEUR Workshop Proceedings, vol. 2663. CEUR-WS.org (2020)"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Kalyanpur, A., Parsia, B., Horridge, M., Sirin, E.: Finding all justifications of OWL DL entailments. In: Aberer, K., Choi, K., Noy, N.F., Allemang, D., Lee, K., Nixon, L.J.B., Golbeck, J., Mika, P., Maynard, D., Mizoguchi, R., Schreiber, G., Cudr\u00e9-Mauroux, P. (eds.) The Semantic Web, 6th International Semantic Web Conference, 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea, November 11-15, 2007. Lecture Notes in Computer Science, vol.\u00a04825, pp. 267\u2013280. Springer (2007)","DOI":"10.1007\/978-3-540-76298-0_20"},{"key":"19_CR9","unstructured":"Kleine B\u00fcning, H., Kullmann, O.: Minimal unsatisfiability and autarkies. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 339\u2013401. IOS Press (2009)"},{"issue":"1\u20133","key":"19_CR10","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0166-218X(00)00262-6","volume":"107","author":"O Kullmann","year":"2000","unstructured":"Kullmann, O.: Investigations on autark assignments. Discret. Appl. Math. 107(1\u20133), 99\u2013137 (2000)","journal-title":"Discret. Appl. Math."},{"key":"19_CR11","unstructured":"Lee, C.T.: A Completeness Theorem and a Computer Program for Finding Theorems Derivable from Given Axioms. Phd thesis, University of Berkeley, California, Department of Electrical Engineering (1967)"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Lev-Ami, T., Weidenbach, C., Reps, T.W., Sagiv, M.: Labelled clauses. In: Pfenning, F. (ed.) Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings. LNCS, vol.\u00a04603, pp. 311\u2013327. Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_21"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Nienhuys-Cheng, S., de\u00a0Wolf, R.: The equivalence of the subsumption theorem and the refutation-completeness for unconstrained resolution. In: Kanchanasut, K., L\u00e9vy, J. (eds.) Algorithms, Concurrency and Knowledge: 1995 Asian Computing Science Conference, ACSC \u201995, Pathumthani, Thailand, December 11-13, 1995, Proceedings. Lecture Notes in Computer Science, vol.\u00a01023, pp. 269\u2013285. Springer (1995)","DOI":"10.1007\/3-540-60688-2_50"},{"issue":"1","key":"19_CR14","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"JA Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM 12(1), 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"19_CR15","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001)"},{"key":"19_CR16","unstructured":"Schlobach, S., Cornet, R.: Non-standard reasoning services for the debugging of description logic terminologies. In: Gottlob, G., Walsh, T. (eds.) IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, Acapulco, Mexico, August 9\u201315, 2003. pp. 355\u2013362. Morgan Kaufmann (2003)"},{"issue":"1","key":"19_CR17","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/s10844-016-0422-7","volume":"49","author":"R Walter","year":"2017","unstructured":"Walter, R., Felfernig, A., K\u00fcchlin, W.: Constraint-based and sat-based diagnosis of automotive configuration problems. J. Intell. Inf. Syst. 49(1), 87\u2013118 (2017)","journal-title":"J. Intell. Inf. Syst."},{"issue":"4","key":"19_CR18","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L Wos","year":"1965","unstructured":"Wos, L., Robinson, G., Carson, D.: Efficiency and completeness of the set of support strategy in theorem proving. Journal of the ACM 12(4), 536\u2013541 (1965)","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T05:28:59Z","timestamp":1672723739000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 July 2021","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":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","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":"76","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":"29","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":"0","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":"38% - 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":"5","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)"}},{"value":"2 invited papers and 7 system descriptions are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}