{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:24:09Z","timestamp":1742919849124,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"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>Unlike other methods for theorem proving modulo with constrained clauses\u00a0[12, 13], equational theorem proving modulo with constrained clauses along with its simplification techniques has not been well studied. We introduce a basic paramodulation calculus modulo equational theories <jats:italic>E<\/jats:italic> satisfying certain properties of <jats:italic>E<\/jats:italic> and present a new framework for equational theorem proving modulo <jats:italic>E<\/jats:italic> with constrained clauses. We propose an inference rule called Generalized <jats:italic>E<\/jats:italic>-Parallel for constrained clauses, which makes our inference system completely basic, meaning that we do not need to allow any paramodulation in the constraint part of a constrained clause for refutational completeness. We present a saturation procedure for constrained clauses based on relative reducibility and show that our inference system including our contraction rules is refutationally complete.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_10","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"166-182","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Equational Theorem Proving Modulo"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1973-615X","authenticated-orcid":false,"given":"Dohan","family":"Kim","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1141-0665","authenticated-orcid":false,"given":"Christopher","family":"Lynch","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"10_CR1","first-page":"415","volume-title":"Automated Reasoning - IJCAR 2004, Cork, Ireland, July 4\u20138","author":"J Avenhaus","year":"2004","unstructured":"Avenhaus, J.: Efficient Algorithms for Computing Modulo Permutation Theories. In: Basin, D., Rusinowitch, M. (eds.) Automated Reasoning - IJCAR 2004, Cork, Ireland, July 4\u20138, pp. 415\u2013429. Springer, Berlin, Heidelberg (2004)"},{"key":"10_CR2","unstructured":"Baader, F.: Combination of compatible reduction orderings that are total on ground terms. In: Winskel, G. (ed.) Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science. pp. 2\u201313. IEEE Computer Society Press, Warsaw, Poland (1997)"},{"key":"10_CR3","doi-asserted-by":"publisher","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, UK (1998)"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Baader, F., Snyder, W.: Unification Theory. In: Handbook of Automated Reasoning, chap. 8, pp. 445\u2013532. Volume I, Elsevier, Amsterdam (2001)","DOI":"10.1016\/B978-044450813-3\/50010-2"},{"issue":"2","key":"10_CR5","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0304-3975(89)90003-0","volume":"67","author":"L Bachmair","year":"1989","unstructured":"Bachmair, L., Dershowitz, N.: Completion for rewriting modulo a congruence. Theoretical Computer Science 67(2), 173\u2013201 (1989)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"10_CR6","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. Log. Comput. 4(3), 217\u2013247 (1994)","journal-title":"J. Log. Comput."},{"key":"10_CR7","first-page":"1","volume-title":"Conditional and Typed Rewriting Systems","author":"L Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H.: Associative-commutative superposition. In: Dershowitz, N., Lindenstrauss, N. (eds.) Conditional and Typed Rewriting Systems, pp. 1\u201314. Springer, Berlin, Heidelberg (1995)"},{"key":"10_CR8","unstructured":"Bachmair, L., Ganzinger, H.: Equational Reasoning in Saturation-Based Theorem Proving. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction. A basis for applications, chap. 11, p. 353\u2013397. Volume I, Kluwer, Dordrecht, Netherlands (1998)"},{"issue":"2","key":"10_CR9","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1006\/inco.1995.1131","volume":"121","author":"L Bachmair","year":"1995","unstructured":"Bachmair, L., Ganzinger, H., Lynch, C., Snyder, W.: Basic Paramodulation. Information and Computation 121(2), 172\u2013192 (1995)","journal-title":"Information and Computation"},{"key":"10_CR10","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/s10817-011-9244-z","volume":"50","author":"M Bofill","year":"2013","unstructured":"Bofill, M., Rubio, A.: Paramodulation with Non-Monotonic Orderings and Simplification. Journal of Automated Reasoning 50, 51\u201398 (2013)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Plaisted, D.A.: Rewriting. In: Handbook of Automated Reasoning, chap. 9, pp. 535\u2013610. Volume I, Elsevier, Amsterdam (2001)","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"key":"10_CR12","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-15240-5_14","volume-title":"Theoretical Computer Science","author":"G Dowek","year":"2010","unstructured":"Dowek, G.: Polarized Resolution Modulo. In: Calude, C.S., Sassone, V. (eds.) Theoretical Computer Science, pp. 182\u2013196. Springer, Berlin, Heidelberg (2010)"},{"issue":"1","key":"10_CR13","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem Proving Modulo. Journal of Automated Reasoning 31(1), 33\u201372 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-319-99840-4_6","volume-title":"Rewriting Logic and Its Applications","author":"F Dur\u00e1n","year":"2018","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: Associative Unification and Symbolic Reasoning Modulo Associativity in Maude. In: Rusu, V. (ed.) Rewriting Logic and Its Applications, pp. 98\u2013114. Springer, Cham (2018)"},{"issue":"7","key":"10_CR15","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. The Journal of Logic and Algebraic Programming 81(7), 898\u2013928 (2012)","journal-title":"The Journal of Logic and Algebraic Programming"},{"key":"10_CR16","unstructured":"Kim, D., Lynch, C.: Equational Theorem Proving Modulo (2021), Technical Report, Web link: https:\/\/people.clarkson.edu\/~clynch\/PAPERS\/etpm.pdf"},{"key":"10_CR17","unstructured":"Kim, D., Lynch, C.: An RPO-based ordering modulo permutation equations and its applications to rewrite systems. In: 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, Buenos Aires, Argentina (Virtual Conference), July 17\u201324, to appear. vol. 195, pp. 19:1\u201319:17. LIPIcs (2021), preprint: http:\/\/people.clarkson.edu\/~dohkim\/tech_reports\/ERPO.pdf"},{"key":"10_CR18","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-030-29007-8_18","volume-title":"Frontiers of Combining Systems","author":"D Kim","year":"2019","unstructured":"Kim, D., Lynch, C., Narendran, P.: Reviving Basic Narrowing Modulo. In: Herzig, A., Popescui, A. (eds.) Frontiers of Combining Systems, pp. 313\u2013329. Springer, Cham, Switzerland (2019)"},{"key":"10_CR19","unstructured":"Kirchner, C., Kirchner, H.: Rewriting, Solving, Proving (1999), Preliminary version: http:\/\/citeseerx.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.144.5349"},{"key":"10_CR20","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-55253-7_22","volume-title":"ESOP \u201992","author":"R Nieuwenhuis","year":"1992","unstructured":"Nieuwenhuis, R., Rubio, A.: Basic superposition is complete. In: Krieg-Br\u00fcckner, B. (ed.) ESOP \u201992, pp. 371\u2013389. Springer, Berlin, Heidelberg (1992)"},{"issue":"1","key":"10_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/jsco.1996.0074","volume":"23","author":"R Nieuwenhuis","year":"1997","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation with Built-in AC-Theories and Symbolic Constraints. Journal of Symbolic Computation 23(1), 1\u201321 (1997)","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning, chap. 7, pp. 371\u2013443. Volume I, Elsevier, Amsterdam (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"10_CR23","first-page":"133","volume-title":"Machine Intelligence 4","author":"G Robinson","year":"1969","unstructured":"Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence 4, pp. 133\u2013150. American Elsevier, New York (1969)"},{"issue":"1","key":"10_CR24","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. J. ACM 12(1), 23\u201341 (1965)","journal-title":"J. ACM"},{"key":"10_CR25","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/3-540-61377-3_53","volume-title":"Computer Science Logic","author":"A Rubio","year":"1996","unstructured":"Rubio, A.: Theorem Proving modulo Associativity. In: B\u00fcning, H.K. (ed.) Computer Science Logic, pp. 452\u2013467. Springer, Berlin, Heidelberg (1996)"},{"key":"10_CR26","doi-asserted-by":"publisher","first-page":"530","DOI":"10.1007\/3-540-58156-1_39","volume-title":"Automated Deduction - CADE-12","author":"L Vigneron","year":"1994","unstructured":"Vigneron, L.: Associative-Commutative Deduction with Constraints. In: Bundy, A. (ed.) Automated Deduction - CADE-12, pp. 530\u2013544. Springer, Berlin (1994)"},{"key":"10_CR27","unstructured":"Wertz, U.: First-order theorem proving modulo equations. Tech. Rep. MPI-I-92-216, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken (1992)"}],"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_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:27:05Z","timestamp":1625650025000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"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)"}}]}}