{"entities":{"Q5930981":{"pageid":8107783,"ns":120,"title":"Item:Q5930981","lastrevid":47606002,"modified":"2026-01-02T05:07:34Z","type":"item","id":"Q5930981","labels":{"en":{"language":"en","value":"Proof-theoretical investigation of temporal logic with time gaps"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1592268"}},"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":"Q5930981$095D0AC1-591C-4A75-A863-D486594E03C5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f57fdbb89093ac6bc4a183df5a333a1a860e6324","datavalue":{"value":{"text":"Proof-theoretical investigation of temporal logic with time gaps","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5930981$20D71CE0-E0B8-4168-A8D4-C631C4B2CDA6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ee3d2280e924d1ebe642841e08aa556173697a40","datavalue":{"value":"0971.03021","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5930981$680C22F7-EFF2-4B89-9E61-470C7489D4BA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"eb9dca186c6f1c40bfb39c3ad6ae8b8d23303558","datavalue":{"value":"10.1007/BF02465129","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5930981$E5175A34-60C0-4E62-834F-F24611E1EB47","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":"Q5930981$A2C84B4D-451B-4D2B-A903-55A3352BF44B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6eae2a8f4ab11bae8edce7ff6ed79c3ee5c09211","datavalue":{"value":{"entity-type":"item","numeric-id":90731,"id":"Q90731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$75A2AB2C-00D6-48DA-9DC7-19AB5FC7E811","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9c942329286f61912919b34bd0734f5ee78c9108","datavalue":{"value":{"time":"+2001-10-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5930981$25FAFCE9-2EA0-4FB5-AF1F-CD8D6C9CEE72","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"37bdd87344b92a1a7bf7326a775227eab8b57381","datavalue":{"value":"A first-order intuitionistic temporal logic sequent calculus is considered, which is based on an intuitionistic version of the first-order sequent calculus LJ without structural rules, and endowed with extra rules for handling temporal operators, in the style of the system LB introduced by \\textit{M. Baaz, A. Leitsch} and \\textit{R. Zach} [Theor. Comput. Sci. 160, 241-270 (1996; Zbl 0872.68171)].    For the system introduced by the author, called LBJ, the invertibility of some of the rules is proved, together with the syntactic admissibility of the structural rules and the cut rule. Versions of Harrop's theorem and Craig's interpolation theorem are proved. Finally, a Gentzen midsequent theorem is proved for the weaker system obtained by removing the antecedent disjunction rule.","type":"string"},"datatype":"string"},"type":"statement","id":"Q5930981$977DEEE9-198F-495B-A87A-753FF3D96E1E","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"d9c7994377655925beca167212c6ec3527b954b5","datavalue":{"value":{"entity-type":"item","numeric-id":587084,"id":"Q587084"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$E56B690A-89AC-44D0-AA00-E25DAE7BC21A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5930981$CB87B3B9-D927-4EC3-A218-77EFA1900E11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5930981$BB5B90B9-ECAD-4431-9BA5-83112E18D96B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4dd3f79a8d1e8e2c1da30bfe1498f09072b3f32c","datavalue":{"value":"1592268","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5930981$9A4A8F54-E558-4D41-8CAC-DDA899FEF54A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42b0eb346b644a08931380c57b24adacf24e4344","datavalue":{"value":"temporal intuitionistic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5930981$A53795D5-94DF-4603-BEAA-92C756A6D477","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2c7d4aa0d3cf1745112ae7d594a2a5578f4e767f","datavalue":{"value":"sequent calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q5930981$1DB9C150-D112-41D7-B160-54B966B10CED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b847c47b7729e9922d06a7206e5661fcbeffcf8f","datavalue":{"value":"proof-theoretical methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q5930981$37C6DE08-CE81-4AA5-95FD-C156F1F409AB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c7c418bdd80155e7ed6c64506326d67cf77aabc4","datavalue":{"value":{"entity-type":"item","numeric-id":41427,"id":"Q41427"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$3683F5BC-92DE-490A-9AFB-786D6C63FEA7","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":"Q5930981$C5F5D1F6-0C52-4F9F-9DC4-0CA8F4E92656","rank":"normal"}],"P223":[{"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":"Q5930981$D90462AC-BD90-4932-BF23-E870ECAB2C8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe4c1ea89bc5854f421d3a6b161146d5aecefa12","datavalue":{"value":{"entity-type":"item","numeric-id":4032862,"id":"Q4032862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$6BCFD2CE-FA0F-44BA-8B5D-5C4FBFFD5CC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"178097464b46161ef715af2d3f5fe3978ea3aabf","datavalue":{"value":{"entity-type":"item","numeric-id":3754596,"id":"Q3754596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$B4B55642-CE9C-4636-ADC6-461EAC4C263F","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":"Q5930981$4D13930B-7000-4BC6-A40F-C445393DC3A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"74833c204341d9aa9ef14997fbac19d0e7da176d","datavalue":{"value":{"entity-type":"item","numeric-id":3749040,"id":"Q3749040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$3D4441E3-0C9F-435A-9D35-6446751C08EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4bb963f0dbfd28b3eb0930566966152abf270c19","datavalue":{"value":{"entity-type":"item","numeric-id":915718,"id":"Q915718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$B01A2559-9062-4E48-84EC-1704A7A2D28C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee2cf2a0dbdd01a7a4261488e61c1139b1e8ab5d","datavalue":{"value":{"entity-type":"item","numeric-id":3919674,"id":"Q3919674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$FEA899C4-D703-4955-8952-DF91DB361599","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"822dfb55932366576e9dce49d4c9ea942ce94d64","datavalue":{"value":{"entity-type":"item","numeric-id":4240680,"id":"Q4240680"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$4B2DA56D-BF9C-4BFD-A249-47E8575D789C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"002bf775feb17ae6b3e8d3218d33a914d2ea456c","datavalue":{"value":{"entity-type":"item","numeric-id":1835666,"id":"Q1835666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$333896F2-19AC-4E98-B914-3897F6A14BF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53e0c1a4e478a32752a62b530cc2a5255baa77dd","datavalue":{"value":{"entity-type":"item","numeric-id":1244216,"id":"Q1244216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$6915A95B-0BA4-44F0-8F39-9CD542C0BC07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a9a36e2a54d0bb700689b29105cdd4e811241336","datavalue":{"value":{"entity-type":"item","numeric-id":3256311,"id":"Q3256311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$C5BF38D0-D8E0-483F-9D9E-EFC183E9437F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c56abf17fe38c9d6f19bb07c76c7c037b3d964b6","datavalue":{"value":{"entity-type":"item","numeric-id":1102941,"id":"Q1102941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$89475A6F-5ED8-4F49-9C7F-C236D52BE5AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1aaa7c2a801938246bc5b9c35ae533855c08aea3","datavalue":{"value":{"entity-type":"item","numeric-id":1090673,"id":"Q1090673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$02AD8BA2-AA0A-4F72-9FA9-8196EA0FD0B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ee55ada81d31217cb0c473ae17b12345717ef0b","datavalue":{"value":{"entity-type":"item","numeric-id":3316619,"id":"Q3316619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$941C5B3C-3285-4C74-BCF9-2AAD316A2A6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e9916acae3c5f1fa2203775504b75059dc2c908","datavalue":{"value":{"entity-type":"item","numeric-id":5608767,"id":"Q5608767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$E92B40F4-E567-49CD-887D-C990C7202EF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26651eb44736bccdd9116d5c165190dd746d76fd","datavalue":{"value":{"entity-type":"item","numeric-id":750417,"id":"Q750417"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5930981$3BA78E9A-A57D-41A9-B518-D56D2C610C4F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"83d522737c03cf2810b6aff4aa4f7638204474fb","datavalue":{"value":{"entity-type":"item","numeric-id":2791888,"id":"Q2791888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"09fdc8e6f1045b9df998830635b47762558e9637","datavalue":{"value":{"amount":"+0.8525903224945068","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":"Q5930981$E1D96EDB-714B-42B5-8017-891950FA280E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"875fa713341ab6deee54c19ed4f3f12543a3d8d8","datavalue":{"value":{"entity-type":"item","numeric-id":5942192,"id":"Q5942192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"aa403374fb9b28d14ea5cf3a8e42e6ae68820cc1","datavalue":{"value":{"amount":"+0.848347008228302","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":"Q5930981$72D60303-067E-4E58-97B6-05B907329492","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bafe910588d152767c69ef431ee1cc5c3680e10b","datavalue":{"value":{"entity-type":"item","numeric-id":1873253,"id":"Q1873253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d196c6f521f94325a328d50dd4c4a294e2d9a070","datavalue":{"value":{"amount":"+0.8359767198562622","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":"Q5930981$E682160F-6BDF-43CC-8E72-6F4B2297CAF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14f99d9245cfcbdf2c1764188bde5f5ead0d0eb7","datavalue":{"value":{"entity-type":"item","numeric-id":1350524,"id":"Q1350524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7abbbd9bf665193ecbe97b7655c71b449acb69c9","datavalue":{"value":{"amount":"+0.8001036047935486","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":"Q5930981$07D9A8B8-DE0B-482E-934E-FD441CC389FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b663a6c139ea16efc2063eb91acece098f1a5fd","datavalue":{"value":{"entity-type":"item","numeric-id":3173797,"id":"Q3173797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"03dbbd0c18060b629bcabe35cd50ec9e0004c08e","datavalue":{"value":{"amount":"+0.7993808388710022","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":"Q5930981$DE370587-5638-4631-9517-2058179D4754","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5930981","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5930981"}}}}}