{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:13:22Z","timestamp":1725491602078},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540752905"},{"type":"electronic","value":"9783540752929"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75292-9_30","type":"book-chapter","created":{"date-parts":[[2007,9,11]],"date-time":"2007-09-11T10:43:07Z","timestamp":1189507387000},"page":"440-454","source":"Crossref","is-referenced-by-count":0,"title":["Building Extended Canonizers by Graph-Based Deduction"],"prefix":"10.1007","author":[{"given":"Silvio","family":"Ranise","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christelle","family":"Scharff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"30_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11559306_4","volume-title":"Frontiers of Combining Systems","author":"A. Armando","year":"2005","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal. In: Gramlich, B. (ed.) Frontiers of Combining Systems. LNCS (LNAI), vol.\u00a03717, Springer, Heidelberg (2005)"},{"issue":"2","key":"30_CR2","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. J. of Information and Computation\u00a0183(2), 140\u2013164 (2003)","journal-title":"J. of Information and Computation"},{"key":"30_CR3","doi-asserted-by":"crossref","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)"},{"issue":"2","key":"30_CR4","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/B:JARS.0000009518.26415.49","volume":"31","author":"L. Bachmair","year":"2003","unstructured":"Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. J. of Automated Reasoning\u00a031(2), 129\u2013168 (2003)","journal-title":"J. of Automated Reasoning"},{"issue":"1-2","key":"30_CR5","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/j.ic.2004.11.001","volume":"199","author":"S. Conchon","year":"2005","unstructured":"Conchon, S., Kristic, S.: Canonization for disjoint unions of theories. Information and Computation\u00a0199(1-2), 87\u2013106 (2005)","journal-title":"Information and Computation"},{"issue":"4","key":"30_CR6","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J. Jouannaud","year":"1986","unstructured":"Jouannaud, J., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. on Computing\u00a015(4), 1155\u20131194 (1986)","journal-title":"SIAM J. on Computing"},{"key":"30_CR7","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D.E. Knuth","year":"1970","unstructured":"Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970)"},{"issue":"1","key":"30_CR8","first-page":"1","volume":"2","author":"C. Lynch","year":"1998","unstructured":"Lynch, C., Strogova, P.: SOUR graphs for efficient completion. Journal of Discrete Mathematics and Theoretical Computer Science\u00a02(1), 1\u201325 (1998)","journal-title":"Journal of Discrete Mathematics and Theoretical Computer Science"},{"issue":"2","key":"30_CR9","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"C.G. Nelson","year":"1980","unstructured":"Nelson, C.G., Oppen, D.C.: Fast Decision Procedures based on Congruence Closure. Journal of the ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the ACM"},{"issue":"2","key":"30_CR10","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"C.G. Nelson","year":"1979","unstructured":"Nelson, C.G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"issue":"3","key":"30_CR11","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/322203.322204","volume":"27","author":"D.C. Oppen","year":"1980","unstructured":"Oppen, D.C.: Reasoning About Recursively Defined Data Structures. J. ACM\u00a027(3), 403\u2013411 (1980)","journal-title":"J. ACM"},{"issue":"1-2","key":"30_CR12","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S0747-7171(08)80131-9","volume":"11","author":"M. Rusinowitch","year":"1991","unstructured":"Rusinowitch, M.: Theorem-proving with resolution and superposition. J. Symb. Comput.\u00a011(1-2), 21\u201349 (1991)","journal-title":"J. Symb. Comput."},{"key":"30_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1007\/978-3-540-31862-0_27","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"S. Ranise","year":"2005","unstructured":"Ranise, S., Ringeissen, C., Tran, D.: Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol.\u00a03407, pp. 372\u2013386. Springer, Heidelberg (2005)"},{"issue":"6","key":"30_CR14","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1109\/MIS.2006.117","volume":"21","author":"S. Ranise","year":"2006","unstructured":"Ranise, S., Tinelli, C.: Satisfiability Modulo Theories. IEEE Magazine on Intelligent Systems\u00a021(6), 71\u201381 (2006)","journal-title":"IEEE Magazine on Intelligent Systems"},{"key":"30_CR15","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1109\/LICS.2001.932479","volume-title":"Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science","author":"H. Ruess","year":"2001","unstructured":"Ruess, H., Shankar, N.: Deconstructing Shostak. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, pp. 19\u201328. IEEE Computer Society, Los Alamitos (2001)"},{"key":"30_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-3-540-30210-0_10","volume-title":"Artificial Intelligence and Symbolic Computation","author":"C. Scharff","year":"2004","unstructured":"Scharff, C., Bachmair, L.: On the Combination of Congruence Closure and Completion. In: Buchberger, B., Campbell, J.A. (eds.) AISC 2004. LNCS (LNAI), vol.\u00a03249, pp. 103\u2013117. Springer, Heidelberg (2004)"},{"key":"30_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding Combinations of Theories. Journal of the ACM\u00a031, 1\u201312 (1984)","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75292-9_30.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:59:00Z","timestamp":1619521140000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75292-9_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540752905","9783540752929"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75292-9_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}