{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:47:53Z","timestamp":1725490073382},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540003151"},{"type":"electronic","value":"9783540362807"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-36280-0_19","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T07:16:50Z","timestamp":1187248610000},"page":"276-290","source":"Crossref","is-referenced-by-count":13,"title":["Calculating Church-Rosser Proofs in Kleene Algebra"],"prefix":"10.1007","author":[{"given":"Georg","family":"Struth","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,12,16]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial. The B-Book. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"19_CR2","unstructured":"H. P. Barendregt. The Lambda Calculus. Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1984."},{"key":"19_CR3","unstructured":"S. L. Bloom and Z. \u00c9sik. Iteration Theories. EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1991."},{"key":"19_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/10722010_4","volume-title":"Separation and reduction","author":"E. Cohen","year":"2000","unstructured":"E. Cohen. Separation and reduction. In R. Backhouse and J. N. Oliveira, editors, Proc. of Mathematics of Program Construction, 5th International Conference, MPC 2000, volume 1837 of LNCS, pages 45\u201359. Springer-Verlag, 2000."},{"key":"19_CR5","unstructured":"J. H. Conway. Regular Algebra and Finite State Machines. Chapman and Hall, 1971."},{"key":"19_CR6","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/S0304-3975(99)00079-1","volume":"230","author":"S. Crvenkovi\u010d","year":"2000","unstructured":"S. Crvenkovi\u010d, I. Dolinka, and Z. \u00c9sik. The variety of Kleene algebras with conversion in not finitely based. Theoretical Computer Science, 230:235\u2013245, 2000.","journal-title":"Theoretical Computer Science"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"V. Diekert and G. Rozenberg, editors. The Book of Traces. World Scientific, 1995.","DOI":"10.1142\/2563"},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0304-3975(96)00154-5","volume":"179","author":"H. Doornbos","year":"1997","unstructured":"H. Doornbos, R. C. Backhouse, and J. van der Woude. A calculation approach to mathematical induction. Theoretical Computer Science, 179:103\u2013135, 1997.","journal-title":"Theoretical Computer Science"},{"key":"19_CR9","unstructured":"S. Eilenberg. Automata, Languages and Machines, volume A. Academic Press, 1974."},{"key":"19_CR10","unstructured":"P. Freyd and A. Scedrov. Categories, Allegories. North-Holland, 1990."},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. MIT Press, 2000.","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"19_CR12","doi-asserted-by":"publisher","first-page":"1155","DOI":"10.1137\/0215084","volume":"15","author":"J.-P. Jouannaud","year":"1986","unstructured":"J.-P. Jouannaud and H. Kirchner. Completion of a set of rules modulo a set of equations. SIAM J. Comput., 15:1155\u20131194, 1986.","journal-title":"SIAM J. Comput."},{"issue":"2","key":"19_CR13","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D. Kozen","year":"1994","unstructured":"D. Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation, 110(2):366\u2013390, 1994.","journal-title":"Information and Computation"},{"key":"19_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/3-540-61042-1_35","volume-title":"Kleene algebra with tests and commutativity conditions","author":"D. Kozen","year":"1996","unstructured":"D. Kozen. Kleene algebra with tests and commutativity conditions. In T. Margaria and B. Steffen, editors, Proc. of TACAS\u201996, volume 1055 of LNCS, pages 14\u201333. Springer-Verlag, 1996."},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"D. Kozen and M.-C. Patron. Certification of compiler optimizations using Kleene algebra with tests. In J. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau, C. Palmadessi, L.-M. Pereira, V. Sagiv, and P.-J. Stuckey, editors, 1st International Conference on Computational Logic (CL2000), volume 1861 of LNAI, pages 568\u2013582. Springer-Verlag, 2001.","DOI":"10.1007\/3-540-44957-4_38"},{"key":"19_CR16","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1006\/jsco.1996.0053","volume":"22","author":"J. Levy","year":"1996","unstructured":"J. Levy and J. Agust\u00ed. Bi-rewrite systems. J. Symbolic Comput., 22:279\u2013314, 1996.","journal-title":"J. Symbolic Comput."},{"issue":"3\u20134","key":"19_CR17","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1023\/A:1006294005493","volume":"23","author":"J. McKinna","year":"1999","unstructured":"J. McKinna and R. Pollack. Some lambda calculus and type theory formalized. J. Automated Reasoning, 23(3\u20134):373\u2013409, 1999.","journal-title":"J. Automated Reasoning"},{"issue":"1","key":"19_CR18","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1023\/A:1006496715975","volume":"26","author":"T. Nipkow","year":"2001","unstructured":"T. Nipkow. More Church-Rosser proofs (in Isabelle\/HOL). J. Automated Reasoning, 26(1):51\u201366, 2001.","journal-title":"J. Automated Reasoning"},{"key":"19_CR19","first-page":"120","volume":"16","author":"V. N. Redko","year":"1964","unstructured":"V. N. Redko. On defining relations for the algebra of regular events. Ukrainian Mathematical Journal, 16:120\u2013126, 1964.","journal-title":"Ukrainian Mathematical Journal"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"G. W. Schmidt and T. Str\u00f6hlein. Relations and Graphs: Discrete Mathematics for Computer Scientists. EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1993.","DOI":"10.1007\/978-3-642-77968-8"},{"issue":"3","key":"19_CR21","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1145\/44483.44484","volume":"35","author":"N. Shankar","year":"1988","unstructured":"N. Shankar. A mechanical proof of the Church-Rosser theorem. Journal of the ACM, 35(3):475\u2013522, 1988.","journal-title":"Journal of the ACM"},{"key":"19_CR22","unstructured":"J. M. Spivey. Understanding Z. Cambrigde University Press, 1988."},{"key":"19_CR23","unstructured":"G. Struth. Canonical Transformations in Algebra, Universal Algebra and Logic. PhD thesis, Institut f\u00fcr Informatik, Universit\u00e4t des Saarlandes, 1998."},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"G. Struth. Church-Rosser proofs in Kleene algebra and allegories. Technical Report 146, Institut f\u00fcr Informatik, Albert-Ludiwigs-Universit\u00e4t Freiburg, 2001. http:\/\/www.informatik.uni-freiburg.de\/~struth\/publications.html .","DOI":"10.1007\/3-540-36280-0_19"},{"key":"19_CR25","unstructured":"G. Struth. Isabelle-specification and proofs of Church-Rosser theorems. http:\/\/www.informatik.uni-freiburg.de\/~struth\/publications.html , 2001."},{"issue":"1","key":"19_CR26","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1006\/inco.1995.1057","volume":"118","author":"M. Takahashi","year":"1995","unstructured":"M. Takahashi. parellel reductions in \u21cc-calculi. Information and Computation, 118(1):120\u2013127, 1995.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Relational Methods in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36280-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T04:06:18Z","timestamp":1556769978000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36280-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540003151","9783540362807"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-36280-0_19","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}