{"entities":{"Q454366":{"pageid":456133,"ns":120,"title":"Item:Q454366","lastrevid":62027886,"modified":"2026-04-11T03:17:54Z","type":"item","id":"Q454366","labels":{"en":{"language":"en","value":"Effective cut-elimination for a fragment of modal mu-calculus"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6088846"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q454366$4E1980B4-5453-4FA4-B984-17DE3C23FCEB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"20abba666055496b038ec6e47be0d25c736648fd","datavalue":{"value":{"text":"Effective cut-elimination for a fragment of modal mu-calculus","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q454366$32AB8F6F-664B-436D-811B-9A6AFA1CD383","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a266e36f5320ff17b38253638d274a926f5a4fea","datavalue":{"value":"1254.03110","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q454366$0121A1B0-753B-4019-A2F0-97545AA5F8D1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"739bb59f926e46bf270e3affee77bc2ef6969661","datavalue":{"value":{"entity-type":"item","numeric-id":454365,"id":"Q454365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q454366$DEAB7FC7-DBF4-418E-A88B-1D81D79183CC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e34236ca73b92c6ee0bc17431d03c3537a7f0792","datavalue":{"value":{"entity-type":"item","numeric-id":195358,"id":"Q195358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q454366$C1B73ABE-2664-4BA2-B087-8276CA79F16F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9ce482458de9f4ace900fbb372ae38b12a79d36f","datavalue":{"value":{"time":"+2012-10-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q454366$0907A726-2C91-45F0-87CD-A06B920F30C1","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"ec9117de5521aa1b95381d6858bf21a19ab9d44c","datavalue":{"value":"The mu-calculus is an extension of temporal logic for transition systems with added fixpoint operators which appeared particularly useful for specification and verification of temporal properties. An infinitary system adequate for the whole mu-calculus was proved cut-free in a non-constructive way by \\textit{G. J\u00e4ger}, \\textit{M. Kretz} and \\textit{T. Studer} in [J. Log. Algebr. Program. 76, No. 2, 270--292 (2008; Zbl 1156.68013)]. A constructive proof of cut elimination for the fragment of mu-calculus, called \\(\\mathrm{M}_1\\), with non-iterated fixpoints and omega-rule was offered by \\textit{W. Buchholz} in [Arch. Math. Logic 40, No. 4, 255--272 (2001; Zbl 1007.03051)], but only for positive formulas. In this paper, G. Mints provides another constructive proof of cut elimination for \\(\\mathrm{M}_1\\) which improves Buchholz's result in two ways. First, it is not restricted to proofs of positive formulas. Second, the omega-rule is only an intermediate tool for obtaining a cut-free calculus.  In order to remove cut from \\(\\mathrm{M}_1\\), the system \\(\\mathrm{M}^\\prime\\) is introduced, which is cut-free but uses instead of the (finitary) rule (ind) of \\(\\mathrm{M}_1\\) some infinitary rule. Next, the auxiliary system \\(\\mathrm{M}^\\Omega \\) is introduced which adds to \\(\\mathrm{M}^\\prime\\) two omega-rules and a form of cut. It is shown that every derivation in \\(\\mathrm{M}_1\\) is transformed into a derivation in \\(\\mathrm{M}^\\Omega \\), and every derivation in \\(\\mathrm{M}^\\Omega \\) is transformed into a derivation in \\(\\mathrm{M}^\\prime\\). Although this result by itself does not imply cut admissibility for \\(\\mathrm{M}_1\\), there are simple sufficient conditions satisfied by Mints's proof which recovers provability in the finitary system from provability in the infinitary one. As a result, cut admissibility for \\(\\mathrm{M}_1\\) follows.  The text is rather dense and technical, hence the reader not acquainted with the mu-calculus should first consult some introductory paper, e.g., \\textit{J. Bradfield} and \\textit{C. Stirling}'s survey in [``Modal mu-calculus'', in: Handbook of modal logic. Amsterdam: Elsevier. 721--756 (2007; Zbl 1114.03001)].","type":"string"},"datatype":"string"},"type":"statement","id":"Q454366$C809EFA1-1C7B-494F-A1A0-49EE448304CD","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"2e7f704932fd75b813eb7e18ce6ce9f1d9ea52bf","datavalue":{"value":{"entity-type":"item","numeric-id":477583,"id":"Q477583"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q454366$0A4096D9-61DE-49A7-ACF1-DDCF6655E689","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q454366$C1474533-E3C2-46F0-A7C1-E9CF5A9DA44B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q454366$1222F760-D332-4A4C-A0E0-7430B3373B3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q454366$DAFA4364-55EA-4271-A79B-C90665B71D49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q454366$0B7819A7-2897-45D9-BB6C-E3EF3E445620","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3e5cc5445c08fc21892a438f4689b600501be433","datavalue":{"value":"6088846","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q454366$748C4B7D-C389-4B27-AE0B-85AFDE95E0BD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b462f38abee80906c2d768906563204d6d43dfc5","datavalue":{"value":"modal mu-calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q454366$014D16BE-01B6-449B-B8B4-DA3365E80287","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dcfc1bc00c58245854e787073d98b7cbed7ce1ba","datavalue":{"value":"cut elimination","type":"string"},"datatype":"string"},"type":"statement","id":"Q454366$F6A62AC7-DE72-49CF-B9A3-6F81D87EFC48","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q454366$456AEFBF-F7B0-444F-8D4A-DB4303DAFCEF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"607c785f8f00b244c8fd0c0e960429accfb2ceb1","datavalue":{"value":"https://doi.org/10.1007/s11225-012-9378-y","type":"string"},"datatype":"url"},"type":"statement","id":"Q454366$045E0632-170F-4FAA-8B32-52E133F4F1FD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fb687ad88c201b688f26739b7135c8c331818bbf","datavalue":{"value":"W2032188971","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q454366$333E28D7-D039-49BF-AAF7-2AC25C79F952","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8d8c566f2b6cb83f15f6eabe2b8d19b7b1d0849d","datavalue":{"value":{"entity-type":"item","numeric-id":1024553,"id":"Q1024553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q454366$6D571C19-24E7-4940-B0E3-998EF3920490","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47c20063395d481d6afd6b6ba37dc0e8e042800c","datavalue":{"value":{"entity-type":"item","numeric-id":5944050,"id":"Q5944050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q454366$26AEDD4F-44A8-4EB3-AD0B-AA95508C8FA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8fdccfda11550d45acc47f56197ada4ccfbb45d6","datavalue":{"value":{"entity-type":"item","numeric-id":1942334,"id":"Q1942334"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q454366$223EF9FE-9BB3-45BD-A42F-8AB8600B5225","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e4809d0a3f36eea3885a973affe8141566cc9e5","datavalue":{"value":{"entity-type":"item","numeric-id":941442,"id":"Q941442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q454366$09C5C38C-369D-4171-8122-F367EE9F6FB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54f1ad840706c682b0fedd77190bd24d7fda2981","datavalue":{"value":{"entity-type":"item","numeric-id":1117213,"id":"Q1117213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q454366$5B6F5CD3-C840-4FF6-B326-591FA43E2546","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c28a63282ca167f0cd2363a2eb3aacead415893c","datavalue":{"value":{"entity-type":"item","numeric-id":283132,"id":"Q283132"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q454366$B10A2F21-4603-4CAE-8E20-F6461670F47A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9c760059e7dedbb8b7864d59fb746fef23ead35","datavalue":{"value":{"entity-type":"item","numeric-id":930618,"id":"Q930618"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q454366$E19023FB-9C74-4215-8762-6FE4110476FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b01f3c9efa192a49157794cc5646843be5e89451","datavalue":{"value":{"entity-type":"item","numeric-id":1086559,"id":"Q1086559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q454366$F41D9D61-74A6-4AF1-9B31-A016A265CA21","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"25a75b6e07f180afd4d326b84a06463cacfab5b3","datavalue":{"value":"10.1007/S11225-012-9378-Y","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q454366$B43F1E75-83BF-48B4-AA42-49CF5E0B240D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d0eeff4fcb3147d0d0c1af2751fa430db8bf734","datavalue":{"value":{"entity-type":"item","numeric-id":1942334,"id":"Q1942334"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b8aec9ec432e1e35287159ae739922bfd0d4833c","datavalue":{"value":{"amount":"+0.8772148","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q454366$D8F2DE13-1545-466A-B9B9-6EAE12F16CB5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0d0253b67ddf18866525d7f7981c346aab2b76dc","datavalue":{"value":{"entity-type":"item","numeric-id":2142090,"id":"Q2142090"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"80d6bff83f2a304a871726c93fcbe5776a7dd1bd","datavalue":{"value":{"amount":"+0.82585967","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q454366$EC8876F5-1546-490C-BB18-57928BB1D274","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ab8cc3ba85a7bfbc723b79ca15f082559c7e3c6","datavalue":{"value":{"entity-type":"item","numeric-id":1005937,"id":"Q1005937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7b53b85d5f23321d10e8d3269c0e613577d106a","datavalue":{"value":{"amount":"+0.8237423","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q454366$91CC25AC-3584-4761-8C6D-84BFEFD71EED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"02cda41305cc32a73f956d4c667e6a100a369e94","datavalue":{"value":{"entity-type":"item","numeric-id":4417913,"id":"Q4417913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"61eb66d9b17cc59bf28a52dd8a2e446c4ce369a4","datavalue":{"value":{"amount":"+0.81215787","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q454366$A3B0F5B6-AFE2-4B8C-AD25-55E8D311C464","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ced5cf362612d739247ae3bb9153bb0331ee7774","datavalue":{"value":{"entity-type":"item","numeric-id":2368950,"id":"Q2368950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb8861331841e769867aa7c86a66540482c9f38f","datavalue":{"value":{"amount":"+0.8121288","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q454366$76D60747-18EF-4ACA-964D-65565D1A182F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14396cd9bd793a2ddf8fa5ff64e5c9589086b357","datavalue":{"value":{"entity-type":"item","numeric-id":5941205,"id":"Q5941205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3766be38b9427590b6cdd371ff874c69e3728269","datavalue":{"value":{"amount":"+0.8085016","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q454366$4F9EF656-34CD-4DBC-9818-58EF3A8D97AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b2eb87392f68ef7607d5fd6657bd3271e995e8f3","datavalue":{"value":{"entity-type":"item","numeric-id":5854738,"id":"Q5854738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"63a0d1a8777b6c1ce12a4a9debd6156bed35ade1","datavalue":{"value":{"amount":"+0.8053075","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q454366$C7D2CB8C-0A7F-4A96-A565-3563AC6CFDE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0095654446119627593dfe20de7d001e2b3bc950","datavalue":{"value":{"entity-type":"item","numeric-id":5144634,"id":"Q5144634"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f16f51bcac76498fb387738c43ce2644fe673546","datavalue":{"value":{"amount":"+0.80186415","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q454366$6FBA077E-0916-4FDA-906D-B85B34C2BE73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ae9852e8d95d730f31c9ebe1fe54edf140479337","datavalue":{"value":{"entity-type":"item","numeric-id":5705921,"id":"Q5705921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fe7558c4b7da78859d58bcaa511ba0df58a7667d","datavalue":{"value":{"amount":"+0.80083036","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q454366$2857738A-9C27-4A1B-8F6C-79D0165FEBE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"00c43934d2945ef672b6cea401b1a238256d0828","datavalue":{"value":{"entity-type":"item","numeric-id":4484479,"id":"Q4484479"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b10756f06a21e7be44a612d3e8a1cda41f440ce3","datavalue":{"value":{"amount":"+0.798831","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q454366$E5F5861D-0C73-4E35-A727-0A4A5EDAC957","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Effective cut-elimination for a fragment of modal mu-calculus","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Effective_cut-elimination_for_a_fragment_of_modal_mu-calculus"}}}}}