{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T07:43:17Z","timestamp":1790667797387,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540735946","type":"print"},{"value":"9783540735953","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_19","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T05:31:33Z","timestamp":1188451893000},"page":"279-294","source":"Crossref","is-referenced-by-count":37,"title":["Automated Reasoning in Kleene Algebra"],"prefix":"10.1007","author":[{"given":"Peter","family":"H\u00f6fner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"19_CR1","unstructured":"http:\/\/www.dcs.shef.ac.uk\/~georg\/ka"},{"key":"19_CR2","unstructured":"Prover9 and Mace4. \n                    \n                      http:\/\/www.cs.unm.edu\/~mccune\/mace4"},{"issue":"1-2","key":"19_CR3","doi-asserted-by":"publisher","first-page":"9","DOI":"10.3166\/jancl.16.9-33","volume":"16","author":"K. Aboul-Hosn","year":"2006","unstructured":"Aboul-Hosn, K., Kozen, D.: KAT-ML: An interactive theorem prover for Kleene algebra with tests. Journal of Applied Non-Classical Logics\u00a016(1-2), 9\u201333 (2006)","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/3-540-16780-3_76","volume-title":"8th International Conference on Automated Deduction","author":"L. Bachmair","year":"1986","unstructured":"Bachmair, L., Dershowitz, N.: Commutation, transformation, and termination. In: Siekmann, J.H. (ed.) 8th International Conference on Automated Deduction. LNCS, vol.\u00a0230, pp. 5\u201320. Springer, Heidelberg (1986)"},{"key":"19_CR5","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"P. Blackburn","year":"2001","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/10722010_4","volume-title":"Mathematics of Program Construction","author":"E. Cohen","year":"2000","unstructured":"Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 45\u201359. Springer, Heidelberg (2000)"},{"key":"19_CR7","volume-title":"Regular Algebra and Finite Machines","author":"J.H. Conway","year":"1971","unstructured":"Conway, J.H.: Regular Algebra and Finite Machines. Chapman & Hall, Sydney (1971)"},{"issue":"3","key":"19_CR8","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1093\/jigpal\/8.3.265","volume":"8","author":"H. Nivelle De","year":"2000","unstructured":"De Nivelle, H., Schmidt, R.A., Hustadt, U.: Resolution-based methods for modal logics. Logic Journal of the IGPL\u00a08(3), 265\u2013292 (2000)","journal-title":"Logic Journal of the IGPL"},{"issue":"4","key":"19_CR9","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1145\/1183278.1183285","volume":"7","author":"J. Desharnais","year":"2006","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Computational Logic\u00a07(4), 798\u2013833 (2006)","journal-title":"ACM Trans. Computational Logic"},{"key":"19_CR10","first-page":"87","volume-title":"3rd IEEE workshop on Visual Languages and Formal Methods (VLFM 2004), ENTCS","author":"M. Ebert","year":"2005","unstructured":"Ebert, M., Struth, G.: Diagram chase in relational system development. In: Minas, M. (ed.) 3rd IEEE workshop on Visual Languages and Formal Methods (VLFM 2004), ENTCS, vol.\u00a0127, pp. 87\u2013105. Elsevier, Amsterdam (2005)"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"112","DOI":"10.1007\/978-3-540-24771-5_10","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"T. Ehm","year":"2004","unstructured":"Ehm, T., M\u00f6ller, B., Struth, G.: Kleene modules. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) Relational and Kleene-Algebraic Methods in Computer Science. LNCS, vol.\u00a03051, pp. 112\u2013123. Springer, Heidelberg (2004)"},{"key":"19_CR12","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"19_CR13","unstructured":"H\u00f6fner, P., Struth, G.: Can refinement be automated? Technical Report CS-07-08, Department of Computer Science, University of Sheffield (2007)"},{"key":"19_CR14","unstructured":"Jipsen, P.: Personal communication"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","first-page":"179","volume-title":"Relational and Kleene-Algebraic Methods in Computer Science","author":"W. Kahl","year":"2004","unstructured":"Kahl, W.: Calculational relation-algebraic proofs in Isabelle\/Isar. In: Berghammer, R., M\u00f6ller, B., Struth, G. (eds.) Relational and Kleene-Algebraic Methods in Computer Science. LNCS, vol.\u00a03051, pp. 179\u2013190. Springer, Heidelberg (2004)"},{"issue":"2","key":"19_CR16","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1006\/inco.1994.1037","volume":"110","author":"D. Kozen","year":"1994","unstructured":"Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation\u00a0110(2), 366\u2013390 (1994)","journal-title":"Information and Computation"},{"issue":"1","key":"19_CR17","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/343369.343378","volume":"1","author":"D. Kozen","year":"2000","unstructured":"Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans. Computational Logic\u00a01(1), 60\u201376 (2000)","journal-title":"ACM Trans. Computational Logic"},{"key":"19_CR18","volume-title":"The Temporal Logic of Reactive and Concurrent Systems\u2014Specification","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems\u2014Specification. Springer, Heidelberg (1991)"},{"issue":"2","key":"19_CR19","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/j.tcs.2005.09.069","volume":"351","author":"B. M\u00f6ller","year":"2006","unstructured":"M\u00f6ller, B., Struth, G.: Algebras of modal operators and partial correctness. Theoretical Computer Science\u00a0351(2), 221\u2013239 (2006)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"19_CR20","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1023\/A:1006496715975","volume":"26","author":"T. Nipkow","year":"2001","unstructured":"Nipkow, T.: More Church-Rosser proofs (in Isabelle\/HOL). J. Automated Reasoning\u00a026(1), 51\u201366 (2001)","journal-title":"J. Automated Reasoning"},{"key":"19_CR21","doi-asserted-by":"publisher","first-page":"1403","DOI":"10.1016\/B978-044450813-3\/50023-0","volume-title":"Handbook of Automated Reasoning, ch. 21","author":"H.J. Ohlbach","year":"2001","unstructured":"Ohlbach, H.J., Nonnengart, A., de Rijke, M., Gabbay, D.: Encoding Two-Valued Nonclassical Logics in Classic Logic. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 21, pp. 1403\u20131485. Elsevier, Amsterdam (2001)"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/3-540-36280-0_19","volume-title":"Relational Methods in Computer Science","author":"G. Struth","year":"2002","unstructured":"Struth, G.: Calculating Church-Rosser proofs in Kleene algebra. In: de Swart, H. (ed.) RelMiCS 2001. LNCS, vol.\u00a02561, pp. 276\u2013290. Springer, Heidelberg (2002)"},{"issue":"2","key":"19_CR23","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.jlap.2005.04.001","volume":"66","author":"G. Struth","year":"2006","unstructured":"Struth, G.: Abstract abstract reduction. Journal of Logic and Algebraic Programming\u00a066(2), 239\u2013270 (2006)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"19_CR24","volume-title":"Term Rewriting Systems","year":"2003","unstructured":"Terese (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)"},{"issue":"3","key":"19_CR25","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1017\/S0960129598002540","volume":"8","author":"B. Karger von","year":"1998","unstructured":"von Karger, B.: Temporal algebra. Mathematical Structures in Computer Science\u00a08(3), 277\u2013320 (1998)","journal-title":"Mathematical Structures in Computer Science"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T05:53:02Z","timestamp":1619502782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}