{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,7,6]],"date-time":"2022-07-06T07:33:56Z","timestamp":1657092836560},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2019,2,1]],"date-time":"2019-02-01T00:00:00Z","timestamp":1548979200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Syst Sci Complex"],"published-print":{"date-parts":[[2019,2]]},"DOI":"10.1007\/s11424-019-8377-8","type":"journal-article","created":{"date-parts":[[2019,2,14]],"date-time":"2019-02-14T00:53:25Z","timestamp":1550105605000},"page":"317-355","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Conditional Congruence Closure over Uninterpreted and Interpreted Symbols"],"prefix":"10.1007","volume":"32","author":[{"given":"Deepak","family":"Kapur","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,2,14]]},"reference":[{"key":"8377_CR1","volume-title":"Dept. of Computer Science, Cornell Univ.","author":"D Kozen","year":"1976","unstructured":"Kozen D, Complexity of Finitely Presented Algebras, Technical Report TR 76\u2013294, Dept. of Computer Science, Cornell Univ., Ithaca, NY, 1976."},{"issue":"4","key":"8377_CR2","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"P J Downey","year":"1980","unstructured":"Downey P J, Sethi R, and Tarjan R E, Variations on the common subexpression problem, JACM, 1980, 27(4): 758\u2013771.","journal-title":"JACM"},{"issue":"7","key":"8377_CR3","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"R E Shostak","year":"1978","unstructured":"Shostak R E, An algorithm for reasoning about equality, Communications of ACM, 1978, 21(7): 583\u2013585.","journal-title":"Communications of ACM"},{"issue":"2","key":"8377_CR4","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G Nelson","year":"1980","unstructured":"Nelson G and Oppen D C, Fast decision procedures based on congruence closure, JACM, 1980, 27(2): 356\u2013364.","journal-title":"JACM"},{"key":"8377_CR5","first-page":"771","volume-title":"Proc. Automated Deduction - CADE 11, LNAI 607","author":"D Craigen","year":"1992","unstructured":"Craigen D, Kromodimoelijo S, Meisels I, et al., Eves system description, Proc. Automated Deduction - CADE 11, LNAI 607, Ed. Kapur, Springer Verlag, 1992, 771\u2013775."},{"key":"8377_CR6","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-61474-5_64","volume-title":"Proc. Computer Aided Verification (CAV)","author":"D Kapur","year":"1996","unstructured":"Kapur D and Subramaniam M, Mechanically verifying a family of multiplier circuits, Proc. Computer Aided Verification (CAV), New Jersey, Springer LNCS 1102 (Eds. by Alur R and Henzinger T A), 1996, 135\u2013146."},{"issue":"2","key":"8377_CR7","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/0898-1221(94)00218-A","volume":"29","author":"D Kapur","year":"1995","unstructured":"Kapur D and Zhang H, An overview of rewrite rule laboratory (RRL), Computers and Math. with Applications, 1995, 29(2): 91\u2013114.","journal-title":"Computers and Math. with Applications"},{"key":"8377_CR8","first-page":"363","volume-title":"Proc. Third International Workshop on Conditional Term Rewriting Systems","author":"H Zhang","year":"1992","unstructured":"Zhang H, Implementing contextual rewriting, Proc. Third International Workshop on Conditional Term Rewriting Systems, Springer LNCS 656 (Eds. by Remy J L and Rusinowitch M), 1992, 363\u2013377."},{"issue":"11","key":"8377_CR9","doi-asserted-by":"publisher","first-page":"1212","DOI":"10.1016\/j.jsc.2010.06.005","volume":"45","author":"A Rybalchenko","year":"2010","unstructured":"Rybalchenko A and Sofronie-Stokkermans V, Constraint solving for interpolation, J. Symb. Comput., 2010, 45(11): 1212\u20131233.","journal-title":"J. Symb. Comput."},{"issue":"2","key":"8377_CR10","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/S0747-7171(87)80067-6","volume":"4","author":"J H Gallier","year":"1987","unstructured":"Gallier J H, Fast algorithms for testing unatisfiability of ground Horn clauses with equations, J. Symb. Comput., 1987, 4(2): 233\u2013254.","journal-title":"J. Symb. Comput."},{"issue":"3","key":"8377_CR11","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"W F Dowling","year":"1984","unstructured":"Dowling W F and Gallier J H, Linear-time algorithms for testing the satisfiability of propositional Horn formulae, J. Log. Program., 1984, 1(3): 267\u2013284.","journal-title":"J. Log. Program."},{"key":"8377_CR12","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/3-540-62950-5_59","volume-title":"Proc. Rewriting Techniques and Applications, 8th Intl. Conf. (RTA-97)","author":"D Kapur","year":"1997","unstructured":"Kapur D, Shostak\u2019s congruence closure as completion, Proc. Rewriting Techniques and Applications, 8th Intl. Conf. (RTA-97), (Ed. by Comon H) Sitges, Spain, Springer LNCS 1231, June, 1997, 23\u201337."},{"key":"8377_CR13","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F Baader","year":"1998","unstructured":"Baader F and Nipkow T, Term Rewriting and All That, Cambridge University Press, Cambridge, 1998."},{"key":"8377_CR14","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"R E Tarjan","year":"1975","unstructured":"Tarjan R E, Efficiency of a good but not linear set union algorithm, Journal of ACM, 1975, 22: 215\u2013225.","journal-title":"Journal of ACM"},{"issue":"5","key":"8377_CR15","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1145\/364099.364331","volume":"7","author":"B A Galler","year":"1964","unstructured":"Galler B A and Fisher M J, An improved equivalence algorithm, C. ACM, 1964, 7(5): 301\u2013303.","journal-title":"C. ACM"},{"key":"8377_CR16","volume-title":"Second Revised Version, Courant Institute of Mathematical Sciences","author":"J Cocke","year":"1970","unstructured":"Cocke J and Schwartz J T, Programming Languages and Their Compilers: Preliminary Notes, Second Revised Version, Courant Institute of Mathematical Sciences, NY, 1970."},{"issue":"4","key":"8377_CR17","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 and Oliveras A, Fast congruence closure and extensions, Information and Computation, 2007, 205(4): 557\u2013580.","journal-title":"Information and Computation"},{"issue":"2","key":"8377_CR18","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1145\/322248.322251","volume":"28","author":"G E Peterson","year":"1981","unstructured":"Peterson G E and Stickel M E, Complete set of reductions for some equational theories, J. ACM, 1981, 28(2): 233\u2013264.","journal-title":"J. ACM"},{"key":"8377_CR19","first-page":"1","volume-title":"Proc. 9th Intl. Conf. on Automated Deduction (CADE)","author":"H Zhang","year":"1988","unstructured":"Zhang H and Kapur D, First order theorem proving using conditional rewrite rules, Proc. 9th Intl. Conf. on Automated Deduction (CADE), Springer LNCS 310, (Eds. by Lusk E W and Overbeek R A), Argonne, USA, May, 1988, 1\u201320."},{"key":"8377_CR20","first-page":"462","volume-title":"Proc. Automated Deduction \u2014 CADE 12, LNAI 607","author":"L Bachmair","year":"1992","unstructured":"Bachmair L, Ganzinger H, Lynch C, et al., Basic paramodulation and superposition, Proc. Automated Deduction \u2014 CADE 12, LNAI 607 (Ed. by Kapur), Springer Verlag, 1992, 462\u2013476."},{"issue":"4","key":"8377_CR21","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J P Jouannaud","year":"1986","unstructured":"Jouannaud J P and Kirchner H, Completion of a set of rules modulo a set of equations, SIAM J. of Computing, 1986, 15(4): 1155\u20131194.","journal-title":"SIAM J. of Computing"},{"key":"8377_CR22","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D Knuth","year":"1970","unstructured":"Knuth D and Bendix P, Simple word problems in universal algebras, Computational Problems in Abstract Algebra (Ed. by Leech), Pergamon Press, 1970, 263\u2013297."},{"key":"8377_CR23","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000009518.26415.49","volume-title":"Abstract Congruence Closure","author":"L Bachmair","year":"2003","unstructured":"Bachmair L, Tiwari A, and Vigneron L, Abstract Congruence Closure, Springer-Verlag, New York, 2003."},{"key":"8377_CR24","first-page":"267","volume-title":"Proc. 18th ICALP, LNCS 510","author":"N Dershowitz","year":"1991","unstructured":"Dershowitz N, Canonical sets of Horn clauses, Proc. 18th ICALP, LNCS 510, 1991, 267\u2013278."},{"key":"8377_CR25","first-page":"39","volume-title":"Ganzinger Festchrift, LNCS 7797","author":"M P Bonacina","year":"2013","unstructured":"Bonacina M P and Dershowitz N, Canonical ground Horn theories, Ganzinger Festchrift, LNCS 7797, 2013, 39\u201369."},{"key":"8377_CR26","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/3-540-61511-3_107","volume-title":"Proc. Automated Deduction - CADE 13, LNAI 1104","author":"D Cyrluk","year":"1996","unstructured":"Cyrluk D, Lincoln P, and Shankar N, On Shostak\u2019s decision procedures for combination of theories, Proc. Automated Deduction - CADE 13, LNAI 1104 (Eds. by McRobbie and Slaney), Springer Verlag, 1996, 463\u2013477."},{"key":"8377_CR27","volume-title":"Proc. Dagstuhl Seminar 17371\u2013Deduction beyond First-order Logic","author":"D Kapur","year":"2017","unstructured":"Kapur D, Efficient Interpolant generation algorithms based on quantifier elimination: EUF, Octagons,..., Proc. Dagstuhl Seminar 17371\u2013Deduction beyond First-order Logic, Wadern, Germany, Sep. 2017, A journal version is under preparation; a draft can be obtained from the author."},{"key":"8377_CR28","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/10720084_16","volume-title":"Proc. Frontiers of Combining Systems, Third International Workshop (FroCoS)","author":"L Bachmair","year":"2000","unstructured":"Bachmair L, Ramakrishnan I V, Tiwari A, et al., Congruence closure modulo associativity and commutativity, Proc. Frontiers of Combining Systems, Third International Workshop (FroCoS), Nancy, France, 2000, 245\u2013259."},{"key":"8377_CR29","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-53904-2_115","volume-title":"Proc. 4th Intl. Conf. on Rewriting Techniques and Applications (RTA)","author":"P Narendran","year":"1991","unstructured":"Narendran P and Rusinowitch M, Any ground associative-commutative theory has a finite canonical rewrite system, Proc. 4th Intl. Conf. on Rewriting Techniques and Applications (RTA), LNCS 488, Springer, 1991, 423\u2013434."},{"key":"8377_CR30","first-page":"345","volume-title":"Proc. First International Conference on Rewriting Techniques and Applications (RTA-85), Dijon, France","author":"A Kandri-Rody","year":"1985","unstructured":"Kandri-Rody A, Kapur D, and Narendran P, An ideal-theoretic approach for word problems and unification problems over commutative algebras, Proc. First International Conference on Rewriting Techniques and Applications (RTA-85), Dijon, France (Eds. by Jouannaud and Musser), Springer LNCS 202, May 1985, 345\u2013364."},{"issue":"11","key":"8377_CR31","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10817-014-9314-0","volume":"54","author":"M P Bonacina","year":"2015","unstructured":"Bonacina M P and Johansson M, On interpolation in automated theorem proving, J. Autom. Reasoning, 2015, 54(11): 69\u201397.","journal-title":"J. Autom. Reasoning"},{"key":"8377_CR32","first-page":"193","volume-title":"Proc. 17th European Symposium on Programming","author":"S Gulwani","year":"2008","unstructured":"Gulwani S and Musuvathi M, Cover algorithms and their combination, Proc. 17th European Symposium on Programming, ESOP 2008, Springer LNCS, 2008, 193\u2013207."},{"key":"8377_CR33","volume-title":"Canonical forms in the finitely presented algebras","author":"P Le Chenadec","year":"1983","unstructured":"Le Chenadec P, Canonical forms in the finitely presented algebras, Ph.D. Thesis, U. of Paris 11, 1983."},{"key":"8377_CR34","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0898-1221(81)90115-2","volume":"7","author":"A M Ballantyne","year":"1981","unstructured":"Ballantyne A M and Lankford D, New decision algorithms for finitely presented commutative semigroups, Computers and Mathematics Applications, 1981, 7: 159\u2013165.","journal-title":"Computers and Mathematics Applications"}],"container-title":["Journal of Systems Science and Complexity"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11424-019-8377-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11424-019-8377-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11424-019-8377-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,13]],"date-time":"2020-02-13T19:07:28Z","timestamp":1581620848000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11424-019-8377-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,2]]}},"alternative-id":["8377"],"URL":"https:\/\/doi.org\/10.1007\/s11424-019-8377-8","relation":{},"ISSN":["1009-6124","1559-7067"],"issn-type":[{"value":"1009-6124","type":"print"},{"value":"1559-7067","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,2]]},"assertion":[{"value":"11 October 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 December 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 February 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}