{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:04Z","timestamp":1753889764714,"version":"3.41.2"},"reference-count":13,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2005,12,21]],"date-time":"2005-12-21T00:00:00Z","timestamp":1135123200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"funder":[{"name":"National Science Foundation","award":["0105586"],"award-info":[{"award-number":["0105586"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Given a universal Horn formula of Kleene algebra with hypotheses of the form\nr = 0, it is already known that we can efficiently construct an equation which\nis valid if and only if the Horn formula is valid. This is an example of\n&lt;i&gt;elimination of hypotheses&lt;\/i&gt;, which is useful because the equational theory\nof Kleene algebra is decidable while the universal Horn theory is not. We show\nthat hypotheses of the form r = 0 can still be eliminated in the presence of\nother hypotheses. This lets us extend any technique for eliminating hypotheses\nto include hypotheses of the form r = 0.<\/jats:p>","DOI":"10.2168\/lmcs-1(3:4)2005","type":"journal-article","created":{"date-parts":[[2006,11,23]],"date-time":"2006-11-23T09:25:28Z","timestamp":1164273928000},"source":"Crossref","is-referenced-by-count":2,"title":["Modularizing the Elimination of r=0 in Kleene Algebra"],"prefix":"10.46298","volume":"Volume 1, Issue 3","author":[{"given":"Christopher","family":"Hardin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2005,12,21]]},"reference":[{"key":"10.2168\/LMCS-1(3:4)2005_BK02","unstructured":"Adam Barth and Dexter Kozen. Equational verification of cache blocking in LU decomposition using Kleene algebra with tests. Technical Report 2002-1865, Computer Science Department, Cornell University, June 2002."},{"key":"10.2168\/LMCS-1(3:4)2005_Coh94","unstructured":"Ernie Cohen. Hypotheses in Kleene algebra. Unpublished, 1994."},{"key":"10.2168\/LMCS-1(3:4)2005_ErnieCohenEmail","unstructured":"Ernie Cohen, 2003. Private communication. Ernie Cohen, Dexter Kozen, and Frederick Smith. The complexity of Kleene algebra with tests. Technical Report 96-1598, Computer Science Department, Cornell University, July 1996."},{"key":"10.2168\/LMCS-1(3:4)2005_Hard05thesis","unstructured":"Chris Hardin.The Horn Theory of Relational Kleene Algebra. PhD thesis, Cornell University, 2005."},{"key":"10.2168\/LMCS-1(3:4)2005_Hard05proof","doi-asserted-by":"crossref","unstructured":"Chris Hardin. Proof theory for Kleene algebra. InProc. of the 20th Symp. on Logic in Computer Science (LICS 2005), pages 290-299, Los Alamitos, CA, June 2005. IEEE.","DOI":"10.1109\/LICS.2005.37"},{"key":"10.2168\/LMCS-1(3:4)2005_HK02","unstructured":"Chris Hardin and Dexter Kozen. On the elimination of hypotheses in Kleene algebra with tests. Technical Report 2002-1879, Computer Science Department, Cornell University, October 2002."},{"key":"10.2168\/LMCS-1(3:4)2005_HK03","unstructured":"Chris Hardin and Dexter Kozen. On the complexity of the Horn theory of REL. Technical Report 2003-1896, Computer Science Department, Cornell University, May 2003."},{"key":"10.2168\/LMCS-1(3:4)2005_Koz91","doi-asserted-by":"crossref","unstructured":"Dexter Kozen.The Design and Analysis of Algorithms. Springer-Verlag, New York, 1991.","DOI":"10.1007\/978-1-4612-4400-4"},{"key":"10.2168\/LMCS-1(3:4)2005_Koz97","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1145\/256167.256195","author":"Dexter Kozen","year":"1997","journal-title":"Transactions on Programming Languages and Systems"},{"key":"10.2168\/LMCS-1(3:4)2005_Koz00","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343378"},{"key":"10.2168\/LMCS-1(3:4)2005_Koz02","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2960"},{"key":"10.2168\/LMCS-1(3:4)2005_KP00","doi-asserted-by":"crossref","unstructured":"Dexter Kozen and Maria-Cristina Patron. Certification of compiler optimizations using Kleene algebra with tests. In J. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau, C. Palamidessi, L. M. Pereira, Y. Sagiv, and P. J. Stuckey, editors,Proc. 1st Int. Conf. Computational Logic (CL2000), volume 1861 ofLecture Notes in Artificial Intelligence, pages 568-582, London, July 2000. Springer-Verlag.","DOI":"10.1007\/3-540-44957-4_38"},{"key":"10.2168\/LMCS-1(3:4)2005_KS96","doi-asserted-by":"crossref","unstructured":"Dexter Kozen and Frederick Smith. Kleene algebra with tests: completeness and decidability. In D. van Dalen and M. Bezem, editors,Proc. 10th Int. Workshop on Computer Science Logic (CSL'96), volume 1258 ofSpringer-Verlag Lecture Notes in Computer Science, pages 244-259, Utrecht, The Netherlands, September 1996.","DOI":"10.1007\/3-540-63172-0_43"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2264\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2264\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:11:07Z","timestamp":1681243867000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2264"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,12,21]]},"references-count":13,"URL":"https:\/\/doi.org\/10.2168\/lmcs-1(3:4)2005","relation":{"is-same-as":[{"id-type":"arxiv","id":"cs\/0511097","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.cs\/0511097","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2005,12,21]]},"article-number":"2264"}}