{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T21:57:39Z","timestamp":1747173459971,"version":"3.40.5"},"reference-count":29,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2024,3,4]],"date-time":"2024-03-04T00:00:00Z","timestamp":1709510400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2024,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We show that Kozen and Tiuryn\u2019s substructural logic of partial correctness <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000045_inline1.png\"\/><jats:tex-math>\n$\\mathsf{S}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> embeds into the equational theory of Kleene algebra with domain, <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000045_inline2.png\"\/><jats:tex-math>\n$\\mathsf{KAD}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>. We provide an implicational formulation of <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000045_inline3.png\"\/><jats:tex-math>\n$\\mathsf{KAD}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> which sets <jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129524000045_inline4.png\"\/><jats:tex-math>\n$\\mathsf{S}$\n<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula> in the context of implicational extensions of Kleene algebra.<\/jats:p>","DOI":"10.1017\/s0960129524000045","type":"journal-article","created":{"date-parts":[[2024,3,4]],"date-time":"2024-03-04T04:22:03Z","timestamp":1709526123000},"page":"645-660","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Implicational Kleene algebra with domain and the substructural logic of partial correctness"],"prefix":"10.1017","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1942-7982","authenticated-orcid":false,"given":"Igor","family":"Sedl\u00e1r","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2024,3,4]]},"reference":[{"key":"#cr-split#-S0960129524000045_ref5.1","doi-asserted-by":"crossref","unstructured":"Desharnais, J. and Struth, G. (2011). Internal axioms for domain semirings. Science of Computer Programming 76","DOI":"10.1016\/j.scico.2010.05.007"},{"key":"#cr-split#-S0960129524000045_ref5.2","unstructured":"(3) 181-203. Special issue on the Mathematics of Program Construction (MPC 2008)."},{"key":"S0960129524000045_ref6","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","article-title":"Propositional dynamic logic of regular programs","volume":"18","author":"Fischer","year":"1979","journal-title":"Journal of Computer and System Sciences"},{"key":"S0960129524000045_ref4","doi-asserted-by":"crossref","first-page":"798","DOI":"10.1145\/1183278.1183285","article-title":"Kleene algebra with domain","volume":"7","author":"Desharnais","year":"2006","journal-title":"ACM Transactions on Computational Logic"},{"key":"S0960129524000045_ref2","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1093\/logcom\/exl036","article-title":"On action logic: equational theories of action algebras","volume":"17","author":"Buszkowski","year":"2006","journal-title":"Journal of Logic and Computation"},{"key":"S0960129524000045_ref9","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"Harel","year":"2000"},{"key":"S0960129524000045_ref21","first-page":"295","article-title":"An infinitary sequent system for the equational theory of *-continuous action lattices","volume":"78","author":"Palka","year":"2007","journal-title":"Fundamenta Informaticae"},{"volume-title":"Exploring Logical Dynamics","year":"1996","author":"van Benthem","key":"S0960129524000045_ref27"},{"key":"S0960129524000045_ref20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3445810","article-title":"Action logic is undecidable","volume":"22","author":"Kuznetsov","year":"2021","journal-title":"ACM Transactions on Computational Logic"},{"key":"S0960129524000045_ref12","unstructured":"Kanazawa, M. (1993). Completeness and decidability of the mixed style of inference with composition. In: Dekker, P. and Stokhof, M. (eds.) Proceedings of the Ninth Amsterdam Colloquium, 377\u2013390."},{"key":"S0960129524000045_ref19","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1145\/772062.772066","article-title":"Substructural logic and partial correctness","volume":"4","author":"Kozen","year":"2003","journal-title":"ACM Transactions on Computational Logic"},{"key":"S0960129524000045_ref3","unstructured":"Cohen, E. , Kozen, D. and Smith, F. (1996). The complexity of Kleene algebra with tests. Technical Report TR96-1598, Computer Science Department, Cornell University."},{"volume-title":"Residuated Lattices: An Algebraic Glimpse at Substructural Logics","year":"2007","author":"Galatos","key":"S0960129524000045_ref7"},{"key":"S0960129524000045_ref13","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1006\/inco.1994.1037","article-title":"A completeness theorem for Kleene algebras and the algebra of regular events","volume":"110","author":"Kozen","year":"1994","journal-title":"Information and Computation"},{"key":"S0960129524000045_ref15","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1145\/256167.256195","article-title":"Kleene algebra with tests","volume":"19","author":"Kozen","year":"1997","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"S0960129524000045_ref16","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1006\/inco.2001.2960","article-title":"On the complexity of reasoning in Kleene algebra","volume":"179","author":"Kozen","year":"2002","journal-title":"Information and Computation"},{"key":"S0960129524000045_ref8","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/BF00628304","article-title":"Dynamic predicate logic","volume":"14","author":"Groenendijk","year":"1991","journal-title":"Linguistics and Philosophy"},{"year":"2023","author":"Sedl\u00e1r","key":"S0960129524000045_ref24"},{"key":"S0960129524000045_ref11","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/B:STUD.0000032089.54776.63","article-title":"From semirings to residuated Kleene lattices","volume":"76","author":"Jipsen","year":"2004","journal-title":"Studia Logica"},{"key":"S0960129524000045_ref28","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1023\/A:1008219821036","article-title":"An update on \u201cmight\u201d","volume":"6","author":"van der Does","year":"1997","journal-title":"Journal of Logic, Language and Information"},{"year":"2022","author":"Sedl\u00e1r","key":"S0960129524000045_ref25"},{"key":"S0960129524000045_ref10","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1023\/A:1008271805106","article-title":"An equational axiomatization of dynamic negation and relational composition","volume":"6","author":"Hollenberg","year":"1997","journal-title":"Journal of Logic, Language and Information"},{"volume-title":"An Introduction to Substrucutral Logics","year":"2000","author":"Restall","key":"S0960129524000045_ref23"},{"key":"S0960129524000045_ref22","doi-asserted-by":"crossref","unstructured":"Pratt, V. (1991). Action logic and pure induction. In: Logics in AI. European Workshop JELIA\u201990, Amsterdam, the Netherlands, September 10\u201314, 1990. Proceedings, Berlin etc., Springer-Verlag, 97\u2013120.","DOI":"10.1007\/BFb0018436"},{"key":"S0960129524000045_ref14","doi-asserted-by":"crossref","first-page":"78","DOI":"10.7551\/mitpress\/4286.003.0007","volume-title":"Logic and Information Flow","author":"Kozen","year":"1994"},{"key":"S0960129524000045_ref17","first-page":"117","article-title":"Automata on guarded strings and applications","volume":"24","author":"Kozen","year":"2003","journal-title":"Mat\u00e9matica Contempor\u00e2nea"},{"key":"S0960129524000045_ref26","doi-asserted-by":"crossref","unstructured":"van Benthem, J. (1995). Logic and the flow of information. In: Prawitz, D. , Skyrms, B. and Westerst\u00e1hl, D. (eds.) Logic, Methodology and Philosophy of Science IX, Studies in Logic and the Foundations of Mathematics, vol. 134, Elsevier, Amsterdam, 693\u2013724.","DOI":"10.1016\/S0049-237X(06)80070-4"},{"first-page":"244","year":"1997","author":"Kozen","key":"S0960129524000045_ref18"},{"key":"S0960129524000045_ref1","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/s10849-011-9152-y","article-title":"Sequential dynamic logic","volume":"21","author":"Bochman","year":"2012","journal-title":"Journal of Logic, Language and Information"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129524000045","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,22]],"date-time":"2024-11-22T08:31:09Z","timestamp":1732264269000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129524000045\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,3,4]]},"references-count":29,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2024,8]]}},"alternative-id":["S0960129524000045"],"URL":"https:\/\/doi.org\/10.1017\/s0960129524000045","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2024,3,4]]},"assertion":[{"value":"\u00a9 The Author(s), 2024. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}