{"entities":{"Q2228437":{"pageid":2239180,"ns":120,"title":"Item:Q2228437","lastrevid":82672667,"modified":"2026-05-06T21:27:54Z","type":"item","id":"Q2228437","labels":{"en":{"language":"en","value":"Loop-type sequent calculi for temporal logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7311961"}},"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":"Q2228437$A29807FE-BC99-45B8-9138-DA351017CF2A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"878ac5487b48c51dd3e9fb750198ae04953ca1c7","datavalue":{"value":{"text":"Loop-type sequent calculi for temporal logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2228437$1A37F85D-C7F2-4065-AB76-95DD01367770","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6cf38020945a088c8c97919177c0930f36a0ef1c","datavalue":{"value":"1462.03012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2228437$0D9B82AA-BE74-4EFA-B7E1-E0C578FC4D84","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3b417081ff3600658a3025bfda3ebccf222d36d2","datavalue":{"value":{"entity-type":"item","numeric-id":174447,"id":"Q174447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$0D8053DB-4115-4C54-BF36-1EBF7DCD3A5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6c87b5aca574eeb1372d986f8806fd69f2d77ca3","datavalue":{"value":{"entity-type":"item","numeric-id":1245696,"id":"Q1245696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$483331B9-86B2-4D40-904E-5FBE40AF5925","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8b2613cf584ec54a9fbe1b2955f9ceb90b88bb35","datavalue":{"value":{"entity-type":"item","numeric-id":2106880,"id":"Q2106880"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$086944EA-A4A6-4ABC-ABAC-E42398575E55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9e7860b5f5f8e3f51d43313692926606ec1d28de","datavalue":{"value":{"entity-type":"item","numeric-id":1344879,"id":"Q1344879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$21B364B3-426E-49E1-86D6-53AA10A47224","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$BDF9A078-2343-445C-830E-121711C2893E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"103ae1223110bc14f3808579ff7835e1b3e9dfe2","datavalue":{"value":{"time":"+2021-02-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2228437$A7CA48E3-7C89-493F-BFEC-B3CA32615FFE","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"e976494278400049ff8dc5b1ffe3ec2a464a47c9","datavalue":{"value":"Loop-type sequent calculi were first considered in [\\textit{P. Wolper}, Log. Anal., Nouv. S\u00e9r. 28, 119--136 (1985; Zbl 0585.03008)]. observing that some global constraints (\\textit{loops}) must be detected on branches to identify a tree as a proof. This approach uses loops not only for closing failed proof trees as in standard cases but also for playing the role of axioms. The loop-type sequent calculi for \\(\\mathbf{BDI}\\) (Beliefs, Desires, Intentions) logic based on \\(\\mathbf{CTL}\\) were presened in [\\textit{N. Naoyuki} et al., Electron. Notes Theor. Comput. Sci. 70, No. 5, 140--152 (2002; Zbl 1270.68286)]. Loop-type sequent calculi for temporal, mutual belief and dynamic logics were considered in [\\textit{A. Pliu\u0161kevi\u010dien\u0117}, Liet. Mat. Rink. 41, 413--420 (2001; Zbl 1043.03516); \\textit{R. Pliu\u0161kevi\u010dius}, Lect. Notes Comput. Sci. 711, 640--649 (1993; Zbl 0925.03107); Lect. Notes Comput. Sci. 713, 289--300 (1993; Zbl 0793.03014); J. Math. Sci., New York 87, No. 1, 1 (1995; Zbl 0928.03021); translation from Zap. Nauchn. Semin. POMI 220, 123--144 (1995); Lect. Notes Comput. Sci. 2083, 107--120 (2001; Zbl 0988.03018); \\textit{R. Pliu\u0161kevi\u010dius} and \\textit{A. Pliu\u0161kevi\u010dien\u0117}, Lect. Notes Comput. Sci. 3900, 112--128 (2006; Zbl 1235.03050); Lect. Notes Comput. Sci. 735, 299--311 (1993); J. Autom. Reason. 13, 391--407 (1994)].  The principal objective in this paper is to give a loop-type sequent calculus \\(\\mathbf{G}_{\\mathrm{L}}\\mathbf{T}\\) for propositional linear temporal logic (PLTL) with temporal operators \\textit{next} \\(\\bigcirc\\)\\ and \\textit{henceforth always} \\(\\square\\), denoted by \\(\\mathrm{PLTL}^{n,a}\\), which is shown to be sound and complete. The sequent calculus \\(\\mathbf{G}_{\\mathrm{L} }\\mathbf{T}^{\\mathcal{U}}\\)\\ for \\(\\mathrm{PLTL}^{n,u}\\) obtained from \\(\\mathrm{PLTL}^{n,a}\\) by adding the temporal operator \\textit{until} is also considered.  Construction of sound and complete cut-free sequent calculi for \\(\\mathrm{PLTL}\\)\\ is utmost problematic, which has to do with the induction principle \\[ \\left( \\phi\\wedge\\square\\left( \\phi\\supset\\bigcirc\\phi\\right) \\right) \\supset\\square\\phi \\] Some considerations on cut-free sequent calculi for PLTL in the literature go as follows:  \\begin{itemize} \\item Infinitary sequent calculi with the \\(\\omega\\)-type induction rule \\[ \\begin{array} [c]{c} \\underline{\\Gamma\\rightarrow\\Delta,\\phi\\quad\\Gamma\\rightarrow\\Delta ,\\bigcirc\\phi\\quad\\dots\\quad\\Gamma\\rightarrow\\Delta,\\overset{n}{\\overbrace {\\bigcirc\\dots\\bigcirc}}\\phi\\quad\\dots}\\\\ \\Gamma\\rightarrow\\Delta,\\square\\phi \\end{array} \\left( \\rightarrow\\square_{\\omega}\\right) \\] were considered in [\\textit{G. Sundholm}, Theoria 43, 47--51 (1977; Zbl 0364.02011); Bull. Sect. Logic, Pol. Acad. Sci. 6, 70--73 (1977; Zbl 0403.03011)].  \\item Calculi with an invariant-like rule \\[ \\begin{array} [c]{c} \\underline{\\Gamma\\rightarrow\\Delta,I\\quad I\\rightarrow\\bigcirc I\\quad I\\rightarrow\\phi}\\\\ \\Gamma\\rightarrow\\Delta,\\square\\phi \\end{array} \\left( \\rightarrow\\square_{\\mathrm{I}}\\right) \\] were considered in [\\textit{B. Paech}, Lect. Notes Comput. Sci. 385, 240--253 (1989; Zbl 0712.03015)].  \\item [\\textit{M. Baaz} et al., Theor. Comput. Sci. 160, No. 1--2, 241--270 (1996; Zbl 0872.68171)] gave a cut-free calculus \\(\\mathbf{LB}\\) even for the first-order temporal logic with the weak induction principle \\[ \\left( \\phi\\wedge\\bigcirc\\square\\phi\\right) \\supset\\square\\phi \\] in place of the above full one. \\end{itemize}","type":"string"},"datatype":"string"},"type":"statement","id":"Q2228437$FBD4254E-1D93-431E-A30B-C35ACAABB0CE","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"50a4d88aaef452ee91d36bc895e7495d5ed6f713","datavalue":{"value":{"entity-type":"item","numeric-id":195143,"id":"Q195143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$4F031772-B59C-4F33-A354-58DECB8D4D2D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2228437$7F33F52F-05C7-41D3-82AD-8D3709E5E16A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d971f250f4b60bd91da7e9350568180af141e6af","datavalue":{"value":"03F03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2228437$7408648E-FD8E-4311-917D-783124BD65B2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"df88063d94e52eba36673b7ba99971b498d0d878","datavalue":{"value":"7311961","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2228437$9C4D3365-FD82-44DD-B3F2-49F497A2080A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2228437$18F6BD90-16C4-4960-A7B6-227B861B444F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2228437$43AF200E-8880-4E23-94BC-1416E4B4176F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a12d2237c0e4999011ee3946ec86d62072efb0f","datavalue":{"value":"derivation loops","type":"string"},"datatype":"string"},"type":"statement","id":"Q2228437$49713514-FB0E-497F-8F08-6976343D3B3B","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":"Q2228437$DB75160E-C576-4359-8269-32FD647ED415","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":"Q2228437$83DACD8A-7226-490E-96B7-C71E216CCFA5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b34c1f2114d93bbb8c6527b08246bc9516b390fd","datavalue":{"value":"https://doi.org/10.1007/s10817-020-09544-1","type":"string"},"datatype":"url"},"type":"statement","id":"Q2228437$4CD72A77-4F82-4864-BDD7-21B3355F6FFF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1f3ae80b132cacd92901a1b8b20074971e9fa221","datavalue":{"value":"W3006128537","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2228437$667C2532-D32F-4B05-AA95-3D8D74ECE59A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5408abb7ea427203ed438e8c0f4c155f1b865110","datavalue":{"value":{"entity-type":"item","numeric-id":5144634,"id":"Q5144634"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$FC810D88-370C-491A-98FF-3DB6D4A2286C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5cf19aa5ea210e41d59bb8f90e4269a2b0cbd50","datavalue":{"value":{"entity-type":"item","numeric-id":5082322,"id":"Q5082322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$77E30920-C7D5-4A14-8773-5DF775CE7645","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9ce02a475c71cc224d5f8cd28d7ab233b8d7b87","datavalue":{"value":{"entity-type":"item","numeric-id":1350524,"id":"Q1350524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$BA687E0B-F1CD-4B9D-96E5-CAB41A6FD652","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9fa9bd4a85c4c49445e39f562d8e5bf96db06519","datavalue":{"value":{"entity-type":"item","numeric-id":941433,"id":"Q941433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$0916D23E-1B50-4EAD-8D00-3D1D080E908A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b6e6bfa9fd1705edeafb2d476da08243926866f","datavalue":{"value":{"entity-type":"item","numeric-id":549180,"id":"Q549180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$33218DFC-4D4D-4FC1-92D8-0867D8347809","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5fbb75377fe28d9c4d5cb2672ca813a70b1a4094","datavalue":{"value":{"entity-type":"item","numeric-id":5385992,"id":"Q5385992"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$FA8A383D-90C9-4D7E-84B2-A888EBDA5154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f667935027a91d887eedfcc3c126d63ce54c15e","datavalue":{"value":{"entity-type":"item","numeric-id":2805273,"id":"Q2805273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$CE013EC9-A0D3-41DA-8165-E2DD76F36A38","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2791adf62fcd6917e0cfb6ca40d21416a8677a76","datavalue":{"value":{"entity-type":"item","numeric-id":5738910,"id":"Q5738910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$E97A0287-AD54-47AF-950D-72303D3405EE","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":"Q2228437$B3C0EF81-D7CA-4E8E-98BD-7C521E151BD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a70813035aa185769f33e98f1023764183e39c20","datavalue":{"value":{"entity-type":"item","numeric-id":5221853,"id":"Q5221853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$5FC20DC9-2674-4BD4-A899-78C0B2B9F6FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27eccfbbbede2a21c5d645307bcefa275e190922","datavalue":{"value":{"entity-type":"item","numeric-id":1254991,"id":"Q1254991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$8013ADB2-05F7-4317-A0DA-E37D2310A7A8","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":"Q2228437$7BD98A13-7895-47A0-BB26-05929AA50821","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd0c46b78181b52be7702f67ba52bb0c241f2c15","datavalue":{"value":{"entity-type":"item","numeric-id":4809714,"id":"Q4809714"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$434AD180-F583-4DCC-A75C-A27AC187AB5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"71e0c6f1c44c0d31cf2a29eb9f5117ac9e36ddcd","datavalue":{"value":{"entity-type":"item","numeric-id":4260367,"id":"Q4260367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$92A85C9A-E0E2-422A-9835-AE754A38A7C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e318768b2e675028aa324fb9bff0b760bb3244e7","datavalue":{"value":{"entity-type":"item","numeric-id":4282615,"id":"Q4282615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$90789FF4-C22A-4499-8A1D-269F80928C33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f95f1f131a2b4fa8bf7f37db5dd3c9e79bb45533","datavalue":{"value":{"entity-type":"item","numeric-id":1344880,"id":"Q1344880"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$5025937F-C0D0-44DC-8BE5-A40FE70A710F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4d63feab56f1a778a90af4695d45c7b560031ff","datavalue":{"value":{"entity-type":"item","numeric-id":4539601,"id":"Q4539601"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$B43E8353-0C62-4D10-8361-C37B936D89DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49877b525d285b4bc1efb9610fa008c62bc20805","datavalue":{"value":{"entity-type":"item","numeric-id":3623966,"id":"Q3623966"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$186551CA-885F-44B5-AF57-BBA119A12D30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7c3e6815cd921fc7767de9db6783bde242a686c","datavalue":{"value":{"entity-type":"item","numeric-id":4143279,"id":"Q4143279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$AC45F840-FF66-452E-903B-CD30946DFABA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d196616e4eb342d663326ece2a055a654cb8ec4e","datavalue":{"value":{"entity-type":"item","numeric-id":4138711,"id":"Q4138711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$7948CF23-BD89-449E-A975-8D94905FDCD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea3235163a762cb44bb2b482cf48af6fc69f890c","datavalue":{"value":{"entity-type":"item","numeric-id":3897033,"id":"Q3897033"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$16F4E105-8A6C-464E-B53E-DAE4CBC65820","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"034d7339259808ce2c0fbe8cdb5235bcf1f5f4c6","datavalue":{"value":{"entity-type":"item","numeric-id":3710510,"id":"Q3710510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2228437$9289AEA3-585E-427A-B35A-3F4FD2A198C3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"85aa8ad0e5b95524ac2ed8b6cd9198c229582701","datavalue":{"value":"10.1007/S10817-020-09544-1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2228437$037FCDD8-08BB-43AF-8EDE-D2934E26441F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"835be840976d82e0e3e69203203f8f9f3386ef08","datavalue":{"value":{"entity-type":"item","numeric-id":2799620,"id":"Q2799620"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5b8b95a71c9faf07daa97e029ae277b1ae6dbc6f","datavalue":{"value":{"amount":"+0.8909388184547424","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":"Q2228437$E366D040-D0F2-48F9-8FE9-20CBAAED39FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4015da87dfac8abdd8c4cbd3c6ffc4e2945f61d0","datavalue":{"value":{"entity-type":"item","numeric-id":2791889,"id":"Q2791889"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6319ca8052cf043b8f4e50e67475bd2df59a876d","datavalue":{"value":{"amount":"+0.8481943011283875","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":"Q2228437$959F2EBD-AE3C-4D29-AAB9-165ECFD1F523","rank":"normal"},{"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":"808572b863055b5ba528554a1dbc05454c2877a2","datavalue":{"value":{"amount":"+0.8365098237991333","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":"Q2228437$07958362-7DAA-4E43-99C4-5E3FE8B5E621","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"30e5ee5f4227ed63fd2fad30b7785213d7f4733f","datavalue":{"value":{"entity-type":"item","numeric-id":2577594,"id":"Q2577594"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e0f586cfcf27927afd4bf8a7a2a22169ba25ab9f","datavalue":{"value":{"amount":"+0.8344386219978333","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":"Q2228437$A42C09B7-8055-4CA8-9FA8-17B7F2D33B6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cf8e57288b7308066f880abd3e2816d45846c866","datavalue":{"value":{"entity-type":"item","numeric-id":5942197,"id":"Q5942197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"13a526c33b262384c6a90ac5a79674ae80c1c5f9","datavalue":{"value":{"amount":"+0.8135507702827454","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":"Q2228437$5BEA1ABF-CA16-4C03-B1F6-CA7BBAE5AB0C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Loop-type sequent calculi for temporal logic","badges":[]}}}}}