{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T07:06:42Z","timestamp":1760080002561,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,7,5]],"date-time":"2016-07-05T00:00:00Z","timestamp":1467676800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,7,5]]},"DOI":"10.1145\/2933575.2933598","type":"proceedings-article","created":{"date-parts":[[2016,10,14]],"date-time":"2016-10-14T13:34:47Z","timestamp":1476452087000},"page":"377-386","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Towards Completeness via Proof Search in the Linear Time \u03bc-calculus"],"prefix":"10.1145","author":[{"given":"Amina","family":"Doumane","sequence":"first","affiliation":[{"name":"PPS, IRIF, CNRS & Universit\u00e9 Paris Diderot"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Baelde","sequence":"additional","affiliation":[{"name":"LSV, ENS Cachan & CNRS, Universit\u00e9 Paris-Saclay"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lucca","family":"Hirschi","sequence":"additional","affiliation":[{"name":"LSV, ENS Cachan & CNRS, Universit\u00e9 Paris-Saclay"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexis","family":"Saurin","sequence":"additional","affiliation":[{"name":"PPS, IRIF, CNRS & Universit\u00e9 Paris Diderot"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,7,5]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2071368.2071370"},{"key":"e_1_3_2_1_2_1","series-title":"LNCS","first-page":"98","volume-title":"F. M. auf der Heide and B","author":"Bradfield J. C.","year":"1996","unstructured":"J. C. Bradfield , J. Esparza , and A. Mader . An effective tableau system for the linear time μ-calculus . In F. M. auf der Heide and B . Monien, editors, ICALP 96, volume 1099 of LNCS , pages 98 -- 109 . Springer , 1996 . ISBN 3-540-61440-0. doi: 10.1007\/3-540-61440-0 120. 10.1007\/3-540-61440-0 J. C. Bradfield, J. Esparza, and A. Mader. An effective tableau system for the linear time μ-calculus. In F. M. auf der Heide and B. Monien, editors, ICALP 96, volume 1099 of LNCS, pages 98--109. Springer, 1996. ISBN 3-540-61440-0. doi: 10.1007\/3-540-61440-0 120."},{"key":"e_1_3_2_1_3_1","unstructured":"J.\n      Brotherston\n     and \n      N.\n      Gorogiannis\n  . \n  Cyclic abduction of inductively defined safety and termination preconditions\n  . In M. M\u00fcller-Olm and H. Seidl editors SAS \n  2014\n  . Proceedings volume \n  8723\n   of \n  LNCS pages \n  68\n  --\n  84\n  . \n  Springer 2014. ISBN 978-3-319-10935-0.  J. Brotherston and N. Gorogiannis. Cyclic abduction of inductively defined safety and termination preconditions. In M. M\u00fcller-Olm and H. Seidl editors SAS 2014. Proceedings volume 8723 of LNCS pages 68--84. Springer 2014. ISBN 978-3-319-10935-0."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exq052"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_11"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11944836_26"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2933598"},{"key":"e_1_3_2_1_8_1","unstructured":"J.\n      Fortier\n     and \n      L.\n      Santocanale\n  . \n  Cuts for circular proofs: semantics and cut-elimination\n  . In S. R. D. Rocca editor CSL'13 volume \n  23\n   of \n  LIPIcs pages \n  248\n  --\n  262\n  . Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik 2013\n  . \n  ISBN\n   978-3-939897-60-6.  J. Fortier and L. Santocanale. Cuts for circular proofs: semantics and cut-elimination. In S. R. D. Rocca editor CSL'13 volume 23 of LIPIcs pages 248--262. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik 2013. ISBN 978-3-939897-60-6."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata Logics, and Infinite Games: A Guide to Current Research","author":"Gr\u00e4del E.","year":"2002","unstructured":"E. Gr\u00e4del , W. Thomas , and T. Wilke , editors . Automata Logics, and Infinite Games: A Guide to Current Research . Springer-Verlag New York, Inc. , New York, NY, USA , 2002 . ISBN 3-540-00388-6. E. Gr\u00e4del, W. Thomas, and T. Wilke, editors. Automata Logics, and Infinite Games: A Guide to Current Research. Springer-Verlag New York, Inc., New York, NY, USA, 2002. ISBN 3-540-00388-6."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"D.\n      Janin\n     and \n      I.\n      Walukiewicz\n  . \n  Automata for the modal mu-calculus and related results\n  . In J. Wiedermann and P. H\u00e1jek editors MFCS'95 volume \n  969\n   of \n  LNCS pages \n  552\n  --\n  562\n  . \n  Springer 1995\n  . ISBN 3-540-60246-1. doi: 10.1007\/3-540-60246-1 160.     10.1007\/3-540-60246-1\nD. Janin and I. Walukiewicz. Automata for the modal mu-calculus and related results. In J. Wiedermann and P. H\u00e1jek editors MFCS'95 volume 969 of LNCS pages 552--562. Springer 1995. ISBN 3-540-60246-1. doi: 10.1007\/3-540-60246-1 160.","DOI":"10.1007\/3-540-60246-1"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70575-8_59"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"R.\n      Kaivola\n    .\n  Axiomatising linear time mu-calculus\n  . In I. Lee and S. A. Smolka editors CONCUR'95 Proceedings volume \n  962\n   of \n  LNCS pages \n  423\n  --\n  437\n  . \n  Springer 1995\n  . ISBN 3-540-60218-6. doi: 10.1007\/3-540-60218-6 32.     10.1007\/3-540-60218-6\nR. Kaivola. Axiomatising linear time mu-calculus. In I. Lee and S. A. Smolka editors CONCUR'95 Proceedings volume 962 of LNCS pages 423--437. Springer 1995. ISBN 3-540-60218-6. doi: 10.1007\/3-540-60218-6 32.","DOI":"10.1007\/3-540-60218-6"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_6"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2006.28"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/129712.129739"},{"key":"e_1_3_2_1_18_1","unstructured":"L.\n      Santocanale\n    .\n  A calculus of circular proofs and its categorical semantics\n  . In M. Nielsen and U. Engberg editors FOSSACS'02 volume \n  2303\n   of \n  LNCS pages \n  357\n  --\n  371\n  . \n  Springer 2002\n  . ISBN 3-540-43366-X.   L. Santocanale. A calculus of circular proofs and its categorical semantics. In M. Nielsen and U. Engberg editors FOSSACS'02 volume 2303 of LNCS pages 357--371. Springer 2002. ISBN 3-540-43366-X."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90110-4"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90031-X"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287593"},{"key":"e_1_3_2_1_22_1","first-page":"14 7050","volume-title":"LICS'95","author":"Walukiewicz I.","year":"1995","unstructured":"I. Walukiewicz . Completeness of Kozen's axiomatisation of the propositional mu-calculus . In LICS'95 , pages 14 -- 24 . IEEE Computer Society , 1995 . ISBN 0-8186- 7050 - 7059 . I. Walukiewicz. Completeness of Kozen's axiomatisation of the propositional mu-calculus. In LICS'95, pages 14--24. IEEE Computer Society, 1995. ISBN 0-8186-7050-9."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2836"}],"event":{"name":"LICS '16: 31st Annual ACM\/IEEE Symposium on Logic in Computer Science","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"],"location":"New York NY USA","acronym":"LICS '16"},"container-title":["Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2933575.2933598","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2933575.2933598","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:56:03Z","timestamp":1750222563000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2933575.2933598"}},"subtitle":["The case of B\u00fcchi inclusions"],"short-title":[],"issued":{"date-parts":[[2016,7,5]]},"references-count":22,"alternative-id":["10.1145\/2933575.2933598","10.1145\/2933575"],"URL":"https:\/\/doi.org\/10.1145\/2933575.2933598","relation":{},"subject":[],"published":{"date-parts":[[2016,7,5]]},"assertion":[{"value":"2016-07-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}