{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T12:57:36Z","timestamp":1743080256834,"version":"3.40.3"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030510732"},{"type":"electronic","value":"9783030510749"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-51074-9_10","type":"book-chapter","created":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T22:02:47Z","timestamp":1593468167000},"page":"163-180","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols"],"prefix":"10.1007","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,6,24]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/9781139025355","volume-title":"An Introduction to Description Logic","author":"F Baader","year":"2017","unstructured":"Baader, F., et al.: An Introduction to Description Logic. Cambridge University Press, Cambridge (2017)"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F., Kapur, D.: Deciding the word problem for ground identities with commutative and extensional symbols. LTCS-Report 20-02, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit\u00e4t Dresden, Dresden (2020). https:\/\/tu-dresden.de\/inf\/lat\/reports#BaKa-LTCS-20-02","DOI":"10.25368\/2022.260"},{"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 (1998)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/10720084_16","volume-title":"Frontiers of Combining Systems","author":"L Bachmair","year":"2000","unstructured":"Bachmair, L., Ramakrishnan, I.V., Tiwari, A., Vigneron, L.: Congruence closure modulo associativity and commutativity. In: Kirchner, H., Ringeissen, C. (eds.) FroCoS 2000. LNCS (LNAI), vol. 1794, pp. 245\u2013259. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10720084_16"},{"issue":"4","key":"10_CR5","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"P Downey","year":"1980","unstructured":"Downey, P., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4), 758\u2013771 (1980)","journal-title":"J. ACM"},{"issue":"1","key":"10_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/138027.138032","volume":"40","author":"J Gallier","year":"1993","unstructured":"Gallier, J.: An algorithm for finding canonical sets of ground rewrite rules in polynomial time. J. ACM 40(1), 1\u201316 (1993)","journal-title":"J. ACM"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-62950-5_59","volume-title":"Rewriting Techniques and Applications","author":"D Kapur","year":"1997","unstructured":"Kapur, D.: Shostak\u2019s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 23\u201337. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-62950-5_59"},{"issue":"1","key":"10_CR8","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s11424-019-8377-8","volume":"32","author":"D Kapur","year":"2019","unstructured":"Kapur, D.: Conditional congruence closure over uninterpreted and interpreted symbols. J. Syst. Sci. Complex. 32(1), 317\u2013355 (2019). https:\/\/doi.org\/10.1007\/s11424-019-8377-8","journal-title":"J. Syst. Sci. Complex."},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1007\/3-540-52885-7_128","volume-title":"International Conference on Automated Deduction","author":"T K\u00e4ufl","year":"1990","unstructured":"K\u00e4ufl, T., Zabel, N.: The theorem prover of the program verifier Tatzelwurm. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 657\u2013658. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52885-7_128"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Complexity of finitely presented algebras. In: Proceedings of the 9th ACM Symposium on Theory of Computing, pp. 164\u2013177. ACM (1977)","DOI":"10.1145\/800105.803406"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-53904-2_115","volume-title":"Rewriting Techniques and Applications","author":"P Narendran","year":"1991","unstructured":"Narendran, P., Rusinowitch, M.: Any ground associative-commutative theory has a finite canonical system. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 423\u2013434. Springer, Heidelberg (1991). https:\/\/doi.org\/10.1007\/3-540-53904-2_115"},{"issue":"4","key":"10_CR12","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(4), 356\u2013364 (1980)","journal-title":"J. ACM"},{"issue":"4","key":"10_CR13","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1016\/j.ic.2006.08.009","volume":"205","author":"R Nieuwenhuis","year":"2007","unstructured":"Nieuwenhuis, R., Oliveras, A.: Fast congruence closure and extensions. Inf. Comput. 205(4), 557\u2013580 (2007)","journal-title":"Inf. Comput."},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-24312-2_4","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"RA Schmidt","year":"2015","unstructured":"Schmidt, R.A., Waldmann, U.: Modal Tableau systems with blocking and congruence closure. In: De Nivelle, H. (ed.) TABLEAUX 2015. LNCS (LNAI), vol. 9323, pp. 38\u201353. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24312-2_4"},{"issue":"7","key":"10_CR15","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"RE Shostak","year":"1978","unstructured":"Shostak, R.E.: An algorithm for reasoning about equality. Commun. ACM 21(7), 583\u2013585 (1978)","journal-title":"Commun. ACM"},{"issue":"4","key":"10_CR16","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1006\/jsco.1993.1029","volume":"15","author":"W Snyder","year":"1993","unstructured":"Snyder, W.: A fast algorithm for generating reduced ground rewriting systems from a set of ground equations. J. Symb. Comput. 15(4), 415\u2013450 (1993)","journal-title":"J. Symb. Comput."},{"key":"10_CR17","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: Proceedings of 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), pp. 29\u201337. IEEE Computer Society (2001)"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Wechler, W.: Universal Algebra for Computer Scientists. EATCS Monographs on Theoretical Computer Science, vol. 25. Springer, Cham (1992). https:\/\/doi.org\/10.1007\/978-3-642-76771-5","DOI":"10.1007\/978-3-642-76771-5"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-51074-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,2]],"date-time":"2022-07-02T21:33:37Z","timestamp":1656797617000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-51074-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030510732","9783030510749"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-51074-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"24 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ijcar2020.org\/","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":"150","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":"46","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":"31% - 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.03","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":"7.38","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11 system descriptions are also included. The conference was held virtually due to the COVID-19 pandemic.","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)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}