{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:39:51Z","timestamp":1725518391373},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-71070-7_29","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T09:56:30Z","timestamp":1220003790000},"page":"327-331","source":"Crossref","is-referenced-by-count":0,"title":["Canonicity!"],"prefix":"10.1007","author":[{"given":"Nachum","family":"Dershowitz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/174652.174655","volume":"41","author":"L. Bachmair","year":"1994","unstructured":"Bachmair, L., Dershowitz, N.: Equational inference, canonical proofs, and proof orderings. Journal of the ACM\u00a041, 236\u2013276 (1994), \n                      \n                        http:\/\/www.cs.tau.ac.il\/~nachum\/papers\/jacm-report.pdf\n                      \n                      \n                     [viewed May 22, 2008]","journal-title":"Journal of the ACM"},{"key":"29_CR2","first-page":"315","volume":"6","author":"K. Bertet","year":"2004","unstructured":"Bertet, K., Nebut, M.: Efficient algorithms on the Moore family associated to an implicational system. Discrete Mathematics and Theoretical Computer Science\u00a06, 315\u2013338 (2004)","journal-title":"Discrete Mathematics and Theoretical Computer Science"},{"key":"29_CR3","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1145\/1182613.1182619","volume":"8","author":"M.P. Bonacina","year":"2007","unstructured":"Bonacina, M.P., Dershowitz, N.: Abstract canonical inference. ACM Transactions on Computational Logic\u00a08, 180\u2013208 (2007), \n                      \n                        http:\/\/tocl.acm.org\/accepted\/240bonacina.pdf\n                      \n                      \n                     [viewed May 22, 2008]","journal-title":"ACM Transactions on Computational Logic"},{"key":"29_CR4","unstructured":"Bonacina, M.P., Dershowitz, N.: Canonical ground Horn theories. Research Report 49\/2007, Dipartimento di Informatica, Universit\u00e0 degli Studi di Verona (2007), \n                      \n                        http:\/\/profs.sci.univr.it\/~bonacina\/papers\/TR2007HornCanonicity.pdf\n                      \n                      \n                     [viewed May 22, 2008]"},{"key":"29_CR5","series-title":"LNAI","first-page":"380","volume-title":"Proc. of the Fourth International Joint Conference on Automated Reasoning (IJCAR)","author":"M.P. Bonacina","year":"2008","unstructured":"Bonacina, M.P., Dershowitz, N.: Canonical inference for implicational systems. In: Proc. of the Fourth International Joint Conference on Automated Reasoning (IJCAR). LNCS (LNAI), vol.\u00a05195, pp. 380\u2013397. Springer, Heidelberg (2008), \n                      \n                        http:\/\/www.cs.tau.ac.il\/~nachum\/papers\/CanonicalImplicational.pdf"},{"key":"29_CR6","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/0304-3975(94)00187-N","volume":"146","author":"M.P. Bonacina","year":"1995","unstructured":"Bonacina, M.P., Hsiang, J.: Towards a foundation of completion procedures as semidecision procedures. Theoretical Computer Science\u00a0146, 199\u2013242 (1995)","journal-title":"Theoretical Computer Science"},{"key":"29_CR7","unstructured":"Buchberger, B.: Ein Algorithmus zum auffinden der Basiselemente des Restklassenringes nach einem nulldimensionalen Polynomideal. PhD thesis, Univ. Innsbruck, Austria (1965)"},{"key":"29_CR8","unstructured":"Burel, G.: Syst\u00e8mes canoniques abstraits: Application \u00e0 la d\u00e9duction naturelle et \u00e0 la compl\u00e9tion. Master\u2019s thesis, Universit\u00e9 Denis Diderot \u2013 Paris 7 (2005), \n                      \n                        http:\/\/www.loria.fr\/~burel\/download\/Burel_Master.pdf\n                      \n                      \n                     [viewed May 22, 2008]"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/11780274_26","volume-title":"Algebra, Meaning, and Computation","author":"G. Burel","year":"2006","unstructured":"Burel, G., Kirchner, C.: Completion is an instance of abstract canonical system inference. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol.\u00a04060, pp. 497\u2013520. Springer, Heidelberg (2006), \n                      \n                        http:\/\/www.loria.fr\/~burel\/download\/bk4jag.pdf\n                      \n                      \n                     [viewed May 22, 2008]"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-540-72734-7_9","volume-title":"Proc. of the Symposium on Logical Foundations of Computer Science (LFCS)","author":"G. Burel","year":"2007","unstructured":"Burel, G., Kirchner, C.: Cut elimination in deduction modulo by abstract completion. In: Artemov, S., Nerode, A. (eds.) Proc. of the Symposium on Logical Foundations of Computer Science (LFCS). LNCS, pp. 115\u2013131. Springer, Heidelberg (2007)"},{"key":"29_CR11","unstructured":"Burel, G., Kirchner, C.: Regaining cut admissibility in deduction modulo using abstract completion (submitted) [viewed May 22, 2008], \n                      \n                        http:\/\/www.loria.fr\/~burel\/download\/gencomp_ic.pdf"},{"key":"29_CR12","unstructured":"Butler, G., Lankford, D.S.: Experiments with computer implementations of procedures which often derive decision algorithms for the word problem in abstract algebras. Memo MTP-7, Department of Mathematics, Louisiana Tech. University, Ruston, LA (1980)"},{"key":"29_CR13","unstructured":"Dershowitz, N.: Canonicity. In: Proc. of the Fourth International Workshop on First-Order Theorem Proving (FTP 2003). Electronic Notes in Theoretical Computer Science, vol.\u00a086, pp. 120\u2013132 (2003), \n                      \n                        http:\/\/www.cs.tau.ac.il\/~nachum\/papers\/canonicity.pdf\n                      \n                      \n                     [viewed May 22, 2008]"},{"key":"29_CR14","first-page":"65","volume-title":"Proc. of the Eighteenth IEEE Symposium on Logic in Computer Science","author":"N. Dershowitz","year":"2003","unstructured":"Dershowitz, N., Kirchner, C.: Abstract saturation-based inference. In: Proc. of the Eighteenth IEEE Symposium on Logic in Computer Science, June 2003, pp. 65\u201374. IEEE Press, Los Alamitos (2003), \n                      \n                        http:\/\/www.cs.tau.ac.il\/~nachum\/papers\/lics2003-final.pdf\n                      \n                      \n                     [viewed May 22, 2008]"},{"key":"29_CR15","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.tcs.2006.03.012","volume":"357","author":"N. Dershowitz","year":"2006","unstructured":"Dershowitz, N., Kirchner, C.: Abstract canonical presentations. Theoretical Computer Science\u00a0357, 53\u201369 (2006), \n                      \n                        http:\/\/www.cs.tau.ac.il\/nachum\/papers\/AbstractCanonicalPresentations.pdf\n                      \n                      \n                     [viewed May 22, 2008]","journal-title":"Theoretical Computer Science"},{"key":"29_CR16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/138027.138032","volume":"40","author":"J. Gallier","year":"1993","unstructured":"Gallier, J., Narendran, P., Plaisted, D., Raatz, S., Snyder, W.: An algorithm for finding canonical sets of ground rewrite rules in polynomial time. J. of the Association of Computing Machinery\u00a040, 1\u201316 (1993)","journal-title":"J. of the Association of Computing Machinery"},{"key":"29_CR17","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/0022-0000(81)90002-7","volume":"23","author":"G. Huet","year":"1981","unstructured":"Huet, G.: A complete proof of correctness of the Knuth\u2013Bendix completion algorithm. Journal of Computer and System Sciences\u00a023, 11\u201321 (1981)","journal-title":"Journal of Computer and System Sciences"},{"key":"29_CR18","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: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970)"},{"key":"29_CR19","unstructured":"Lankford, D.S.: Canonical inference. Memo ATP-32, Automatic Theorem Proving Project, University of Texas, Austin, TX (1975)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_29.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:36:31Z","timestamp":1620016591000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540710691","9783540710707"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}