{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:21:47Z","timestamp":1776316907876,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540705932","type":"print"},{"value":"9783540705949","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70594-9_19","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"360-387","source":"Crossref","is-referenced-by-count":11,"title":["Modal Semirings Revisited"],"prefix":"10.1007","author":[{"given":"Jules","family":"Desharnais","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Struth","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"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\/prover9"},{"key":"19_CR3","unstructured":"Waldmeister, \n                  \n                    http:\/\/www.waldmeister.org"},{"key":"19_CR4","unstructured":"Birkhoff, G.: Lattice Theory. Colloquium Publications, vol.\u00a025. American Mathematical Society (reprint, 1984)"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/11828563_8","volume-title":"Relations and Kleene Algebra in Computer Science","author":"J.-L. Carufel De","year":"2006","unstructured":"De Carufel, J.-L., Desharnais, J.: Demonic Algebra with Domain. In: Schmidt, R.A. (ed.) RelMiCS\/AKA 2006. LNCS, vol.\u00a04136, pp. 120\u2013134. Springer, Heidelberg (2006)"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Degen, W., Werner, J.M.: Towards intuitionistic dynamic logic. In: Proceedings of Studia Logica 2006. Logic and Logical Philosophy, vol.\u00a015, pp. 305\u2013324. Nicolaus Copernicus University Press (2007)","DOI":"10.12775\/LLP.2006.018"},{"key":"19_CR7","first-page":"647","volume-title":"IFIP TCS 2004","author":"J. Desharnais","year":"2004","unstructured":"Desharnais, J., M\u00f6ller, B., Struth, G.: Termination in modal Kleene algebra. In: L\u00e9vy, J.-J., Mayr, E.W., Mitchell, J.C. (eds.) IFIP TCS 2004, pp. 647\u2013660. Kluwer, Dordrecht (2004); Revised version: Algebraic Notions of Termination. Technical Report 2006-23, Institut f\u00fcr Informatik, Universit\u00e4t Augsburg (2006)"},{"issue":"4","key":"19_CR8","doi-asserted-by":"crossref","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_CR9","unstructured":"Desharnais, J., Struth, G.: Enabledness conditions for action systems, probabilistic systems, and processes. Technical Report CS-06-08, Department of Computer Science, University of Sheffield (2008)"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/978-3-540-27812-2_7","volume-title":"Theory Is Forever","author":"Z. \u00c9sik","year":"2004","unstructured":"\u00c9sik, Z., Kuich, W.: A Semiring-Semimodule Generalization of \u03c9-Context-Free Languages. In: Karhum\u00e4ki, J., Maurer, H., P\u0103un, G., Rozenberg, G. (eds.) Theory is Forever. LNCS, vol.\u00a03113, pp. 68\u201380. Springer, Heidelberg (2004)"},{"key":"19_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-540-73595-3_19","volume-title":"Automated Deduction \u2013 CADE-21","author":"P. H\u00f6fner","year":"2007","unstructured":"H\u00f6fner, P., Struth, G.: Automated Reasoning in Kleene Algebra. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 279\u2013294. Springer, Heidelberg (2007)"},{"key":"19_CR12","first-page":"197","volume":"201","author":"P. H\u00f6fner","year":"2008","unstructured":"H\u00f6fner, P., Struth, G.: Can refinement be automated? ENTCS\u00a0201, 197\u2013222 (2008)","journal-title":"ENTCS"},{"key":"19_CR13","volume-title":"Stone Spaces","author":"P.J. Johnstone","year":"1982","unstructured":"Johnstone, P.J.: Stone Spaces. Cambridge University Press, Cambridge (1982)"},{"key":"19_CR14","doi-asserted-by":"publisher","first-page":"891","DOI":"10.2307\/2372123","volume":"73","author":"B. J\u00f3nsson","year":"1951","unstructured":"J\u00f3nsson, B., Tarski, A.: Boolean algebras with operators, Part I. American Journal of Mathematics\u00a073, 891\u2013939 (1951)","journal-title":"American Journal of Mathematics"},{"issue":"2","key":"19_CR15","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":"3","key":"19_CR16","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1145\/256167.256195","volume":"19","author":"D. Kozen","year":"1997","unstructured":"Kozen, D.: Kleene algebra with tests. ACM Trans. Program. Lang. Syst.\u00a019(3), 427\u2013443 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"2","key":"19_CR17","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.jlap.2005.04.004","volume":"66","author":"H. Lei\u00df","year":"2006","unstructured":"Lei\u00df, H.: Kleene modules and linear languages. Journal of Logic and Algebraic Programming\u00a066(2), 185\u2013194 (2006)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/978-3-540-30124-0_24","volume-title":"Computer Science Logic","author":"P. Maier","year":"2004","unstructured":"Maier, P.: Intuitionistic LTL and a New Characterization of Safety and Liveness. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 295\u2013309. Springer, Heidelberg (2004)"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/11828563_20","volume-title":"Relations and Kleene Algebra in Computer Science","author":"A.K. McIver","year":"2006","unstructured":"McIver, A.K., Cohen, E., Morgan, C.C.: Using Probabilistic Kleene Algebra for Protocol Verification. In: Schmidt, R.A. (ed.) RelMiCS\/AKA 2006. LNCS, vol.\u00a04136, pp. 296\u2013310. Springer, Heidelberg (2006)"},{"issue":"2","key":"19_CR20","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"},{"key":"19_CR21","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10472-007-9051-8","volume":"49","author":"V. Sofronie-Stokkermans","year":"2007","unstructured":"Sofronie-Stokkermans, V.: Automated theorem proving by resolution in non-classical logics. Annals of Mathematics and Artificial Intelligence\u00a049, 221\u2013252 (2007)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/11783596_23","volume-title":"Mathematics of Program Construction","author":"K. Solin","year":"2006","unstructured":"Solin, K., von Wright, J.: Refinement Algebra with Operators for Enabledness and Termination. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol.\u00a04014, pp. 397\u2013415. Springer, Heidelberg (2006)"},{"key":"19_CR23","unstructured":"Struth, G.: Reasoning automatically about termination and refinement. In: S.\u00a0Ranise, editor, 6th International Workshop on First-Order Theorem Proving, Technical Report ULCS-07-018, Department of Computer Science, pp. 36\u201351. University of Liverpool (2007)"},{"issue":"1-2","key":"19_CR24","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.scico.2003.09.002","volume":"51","author":"J. Wright von","year":"2004","unstructured":"von Wright, J.: Towards a refinement algebra. Science of Computer Programming\u00a051(1-2), 23\u201345 (2004)","journal-title":"Science of Computer Programming"}],"container-title":["Lecture Notes in Computer Science","Mathematics of Program Construction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70594-9_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T04:24:02Z","timestamp":1620015842000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70594-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705932","9783540705949"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70594-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}