{"entities":{"Q941433":{"pageid":943281,"ns":120,"title":"Item:Q941433","lastrevid":65576100,"modified":"2026-04-12T03:33:08Z","type":"item","id":"Q941433","labels":{"en":{"language":"en","value":"Cut-free sequent systems for temporal logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5318672"}},"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":"Q941433$5A0FE4E7-CC3C-4E05-9338-9644769ECC25","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"118e4cd917f497e0d43b8f190899ce47be780607","datavalue":{"value":{"text":"Cut-free sequent systems for temporal logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q941433$6805627D-8179-4B2A-956F-97ABB4F164A1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"42a91fb758c7eb7139d66d275b93561e06e9d433","datavalue":{"value":"1151.03009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q941433$04F96F37-E104-4671-9545-9F1A61C265C9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1a4b8e93464bd8436b70044ab37bdd425a7513d2","datavalue":{"value":{"entity-type":"item","numeric-id":714716,"id":"Q714716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$5C43ACD2-FCEC-4D97-ABC4-50A4B209B85E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0e9395c4897e056d54eaef255c0b18eeb46bea27","datavalue":{"value":{"entity-type":"item","numeric-id":386036,"id":"Q386036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$11B22D6A-43AF-4CA8-A16D-7E799F93C49C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"786ecb874cd758b218aa4cf99a475aee0b3588ed","datavalue":{"value":{"entity-type":"item","numeric-id":175862,"id":"Q175862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$34FA49C1-3E78-4B28-AE55-2D541C764700","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"69a3b8af869e2bcb147113fe194666e3284a9607","datavalue":{"value":{"time":"+2008-09-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":"Q941433$005DF7E6-1930-43B2-8965-542DB17DB3F0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7a00ba7c62cb3175dc1d2c495fbf9a46ed60f766","datavalue":{"value":"https://boris.unibe.ch/37186/1/bl08.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q941433$46C5507B-E949-48E7-B4D6-738DA83EA392","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"7eb6b0bed52a819080c43adebf8146330ba4de46","datavalue":{"value":"The paper develops finitary cut-free, invariant-free, weakening-free, and contraction-free sequent calculi for the propositional temporal logics LTL and CTL, using the earlier developed idea of focus games [see, e.g., \\textit{M. Lange} and \\textit{C. Stirling}, J. Log. Comput. 12, No.~4, 623--639 (2002; Zbl 1001.68077)]. In the case of linear time all rules are invertible. The systems are based on annotating fixpoint formulas with a history, an approach which has also been used in game-theoretic characterisations of these logics.","type":"string"},"datatype":"string"},"type":"statement","id":"Q941433$0291C87F-1505-42A1-8B46-DF4A1A72142D","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"57ad727308120c2d3a49a9849dfa008e9ce3bebc","datavalue":{"value":{"entity-type":"item","numeric-id":703859,"id":"Q703859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$3DCFA5E0-6520-41A8-B5BD-F74931FD1C6F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q941433$C7BDDDCC-08E9-4FF3-9093-6AEA7C66E1F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q941433$5C7B706B-4279-4D26-B048-2C789635085C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q941433$27E2E53C-2CD3-4647-B46F-1CF828B702D0","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0fd33332b86f672c7908eec0129c4e435ee84dbb","datavalue":{"value":"5318672","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q941433$43B52ADA-5AA5-493D-898B-C518FBD82305","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q941433$43F4AC2B-80D4-483B-8879-EC5C5F765C4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"85a839a7ba93b7be8ef2a01122562abb5ca55aa9","datavalue":{"value":"LTL","type":"string"},"datatype":"string"},"type":"statement","id":"Q941433$9CA84A40-F012-4B44-A7E6-9F4BF533631C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"af948ab56df44408fff2ba197f928e63c9954960","datavalue":{"value":"CTL","type":"string"},"datatype":"string"},"type":"statement","id":"Q941433$1EC96FC2-F52B-4649-BDF8-6DD8F0073E45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4c8e2875f94b547e8e51d4354560d57f874f7e1c","datavalue":{"value":"cut-free sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q941433$C542E897-7699-48D6-87F8-36808207BDCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6940f661c8875088ebaa9c7f1489dacb1c19755","datavalue":{"value":"focus games","type":"string"},"datatype":"string"},"type":"statement","id":"Q941433$A8A2E2D7-354C-48CF-87C1-53FF91E2309D","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f1dd593caa76171727c63057fe580e976fa16cf5","datavalue":{"value":{"entity-type":"item","numeric-id":23931,"id":"Q23931"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$BB9CD44C-D8FF-465D-AAAD-AC4EC35B037E","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":"Q941433$4A22E028-907A-49F1-AB5C-4ECDB57BF188","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"97a666bc3fdbe4c93a60ea9af127a28b1906f44f","datavalue":{"value":"W2047456744","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q941433$7CCC83A0-3CA5-4149-A23B-7ABC2A41A22C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"120c8e41431895a309f8ef32cac52a772f33d796","datavalue":{"value":{"entity-type":"item","numeric-id":4385542,"id":"Q4385542"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$15020CE4-00AB-4CF4-9C31-CE6CBEF36E25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2990e15db3ec1299bacd39e760b2d345098c103a","datavalue":{"value":{"entity-type":"item","numeric-id":4845472,"id":"Q4845472"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$36F8A690-6570-43F7-BA7D-3C52030C17B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47c57a1bc98a9d819c8c4b25347f0c45d96256b1","datavalue":{"value":{"entity-type":"item","numeric-id":1258296,"id":"Q1258296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$A7F7C73D-6769-4C7C-AA85-95A358BF245F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e79adceaea1e40b4cad7838a35b0a0fd442b58ac","datavalue":{"value":{"entity-type":"item","numeric-id":3608433,"id":"Q3608433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$30135F4E-3055-4C1D-B8E4-92D19942CF34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf1aae49eb6b5d7cf3c74c68e06df16ab076f84f","datavalue":{"value":{"entity-type":"item","numeric-id":2753601,"id":"Q2753601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$45E6C1AF-8AC1-4B4B-9419-0ABB7DDB112A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"40ff4e0a36ab923a095f0b7625ab7e6d8dd74391","datavalue":{"value":{"entity-type":"item","numeric-id":3665079,"id":"Q3665079"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$F5B6E0E1-5117-444A-A81D-E5D39460B2ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a52ffcc834194620943ec4a87fc97578b45281e4","datavalue":{"value":{"entity-type":"item","numeric-id":2506830,"id":"Q2506830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$82C777BD-0052-4A6A-AE06-4BAD366068E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc207fadc6ba9564432e7709593a9b3cf923d465","datavalue":{"value":{"entity-type":"item","numeric-id":2475436,"id":"Q2475436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$205096B5-74D8-4E97-8E7C-10DF28D97986","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4933c393e0df0da8bf72b1cf018c0c8fde2fe994","datavalue":{"value":{"entity-type":"item","numeric-id":3751561,"id":"Q3751561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$BA50A6CC-E044-488A-BF31-0DC52B7D5708","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f5a45904f81b6a39ede475e2e86ab18eb54c04e","datavalue":{"value":{"entity-type":"item","numeric-id":801893,"id":"Q801893"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$BBA62AB3-4B62-4F47-BB09-F34364A698BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4f4af750feffe07532baad6b022ff1a80c425c9","datavalue":{"value":{"entity-type":"item","numeric-id":5897298,"id":"Q5897298"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$73DB127D-3E56-4CFE-8C4F-6E3E0D94E2C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d55d9d717b6dd928ca51f3a56f3933f99738e0a9","datavalue":{"value":{"entity-type":"item","numeric-id":4444910,"id":"Q4444910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$9A09BA2F-E87F-45D0-9386-9DC398F52001","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d32fbb358fe8ff698056a464a35ad043a50a44f","datavalue":{"value":{"entity-type":"item","numeric-id":3496314,"id":"Q3496314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$ACA25F61-1377-4F61-8327-194A888BD512","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb6ef5633e12f6701b6cd89e68936d56c52dfab1","datavalue":{"value":{"entity-type":"item","numeric-id":4560364,"id":"Q4560364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$2AD67E92-B3FB-42C8-9010-28E43C210965","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7bf387cf6efa0c72efe979138deef219e19f92f0","datavalue":{"value":{"entity-type":"item","numeric-id":3838819,"id":"Q3838819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q941433$67161B62-833E-4474-9279-C8840BA3AD0D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5d3dc167063d0c963f7299d2c6cd9f9082db5703","datavalue":{"value":"10.1016/J.JLAP.2008.02.004","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q941433$7C0768FD-F4F0-4F98-BA67-8FA8509B9010","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2c5c7bd2dc2dc31f29989bd94d784e75dd94c366","datavalue":{"value":{"entity-type":"item","numeric-id":3608433,"id":"Q3608433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16ff3c1d0c24b42a0733b6347614fb238075e33b","datavalue":{"value":{"amount":"+0.8397984504699707","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q941433$292E4D98-2AD6-4B8D-8DB9-EF92AD77BA8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24cc7780ba43a8ea5c56365615a44d25e91d56cb","datavalue":{"value":{"entity-type":"item","numeric-id":1317905,"id":"Q1317905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"174e23a46c455a53cc213ce5b91ee38122bd1555","datavalue":{"value":{"amount":"+0.8252725005149841","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q941433$F667F03F-C919-461C-BACF-22BEA67D8F09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0f79eb5dfec092432cf602434e44477be294c9dc","datavalue":{"value":{"entity-type":"item","numeric-id":1762733,"id":"Q1762733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07c16cc0f0f2c054d3d49adc93a86738dc199add","datavalue":{"value":{"amount":"+0.8230763673782349","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q941433$09DCE0F2-1A63-4C3C-988C-A8CF285DFE75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e821d8d0a03f4a83fd0f9976fbfca3c4328866af","datavalue":{"value":{"entity-type":"item","numeric-id":2810015,"id":"Q2810015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f2ddc12ea9fd62d3bc90adfcf928cef4eeda3a72","datavalue":{"value":{"amount":"+0.8122340440750122","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q941433$BDDA832E-30A1-46C3-BFF8-1ED373D2592D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d66f0c96665b023d6c7d806c39d1dd834cb6011c","datavalue":{"value":{"entity-type":"item","numeric-id":3496314,"id":"Q3496314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2ceeb10fc4f15bc535dbbdd85b0cf0467f87555b","datavalue":{"value":{"amount":"+0.8075865507125854","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q941433$8C790F86-E0B7-4223-9E55-25D7D1AA24CE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Cut-free sequent systems for temporal logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Cut-free_sequent_systems_for_temporal_logic"}}}}}