{"entities":{"Q1591203":{"pageid":1601943,"ns":120,"title":"Item:Q1591203","lastrevid":67935996,"modified":"2026-04-12T20:20:36Z","type":"item","id":"Q1591203","labels":{"en":{"language":"en","value":"Decidable fragments of first-order temporal logics"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1546600"}},"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":"Q1591203$B2E2D2DA-F63F-47BF-83E7-D8401F36CD5D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"92e12d7295f5b89e7bcefb649744e030861d7cc3","datavalue":{"value":{"text":"Decidable fragments of first-order temporal logics","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1591203$1F75FF6D-E702-45AB-BB9B-ED8DF830AAB6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ae6a84c2ea4c3b11e5c787c66c0cfcc8a3491090","datavalue":{"value":"0999.03015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1591203$5FD656C1-1BEF-49DE-BA03-BB355D99EE89","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ae18720d5672fa7335ee23e764dc8aff0ec5a2df","datavalue":{"value":"10.1016/S0168-0072(00)00018-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1591203$EB9E9EBB-CB8A-4222-BE98-086D133CD2E2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"76722ee993ef1bba5eff4ce8b9dbe5e1d07862be","datavalue":{"value":{"entity-type":"item","numeric-id":239516,"id":"Q239516"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$8724E145-DEB9-49F8-8B75-CC2C53ACCFF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dba48006b5c8e496f7eee02dd0edb814c74265c9","datavalue":{"value":{"entity-type":"item","numeric-id":912841,"id":"Q912841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$389CC530-7FE0-49BC-A1D0-D12355BF5A1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6a400f63fb65fdbb9cd5ac7576d054d4b1a7834c","datavalue":{"value":{"entity-type":"item","numeric-id":1181481,"id":"Q1181481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$76D9FEE0-57DC-46AF-86AC-88BD24469EC2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$0C39BE49-D668-4913-ABE2-DAFA21FAF5A1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ecfb7a4bc3532872a5df039a2c083f1e58c22460","datavalue":{"value":{"time":"+2002-11-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1591203$38A09538-36FB-4F76-9669-298851A1E687","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"86d013cdc7e11d116fe2ddc8b8187bce538f3198","datavalue":{"value":"First-order temporal logic extends ordinary first-order logic by the binary temporal operators \\({\\mathcal S}\\) (since) and \\({\\mathcal U}\\) (until). The logic is interpreted using a strict linear order \\((W,<)\\) and for each \\(w\\in W\\) a first-order structure \\(I(w)\\) where the underlying domain of the \\(I(w)\\) as well as the interpretations of constants are the same for each \\(w\\). The linear order \\(W\\) models the flow of time; \\(I(w)\\) varying with \\(w\\) reflects the idea that meanings of predicates may change over time. Given \\(w\\in W\\) and a formula \\(\\phi\\) with parameters from \\(D\\), one writes \\(w\\models \\phi\\) to mean that \\(\\phi\\) is valid ``at time'' \\(w\\). One has in particular \\(w\\models \\phi{\\mathcal U}\\psi\\) iff there is \\(v>w\\) such that \\(v\\models \\phi\\) and \\(u\\models \\psi\\) for each \\(w<u<v\\). Likewise, \\(w\\models \\phi{\\mathcal S}\\psi\\) iff there is \\(v<w\\) such that \\(v\\models \\phi\\) and \\(u\\models \\psi\\) for each \\(v<u<w\\). For example, \\(\\diamondsuit\\phi := \\top{\\mathcal U}\\phi\\) expresses that \\(\\phi\\) holds at some later time, i.e., eventually, whereas \\(\\square\\phi:=\\neg\\diamondsuit\\neg\\phi\\) expresses that \\(\\phi\\) holds at all later times, i.e., henceforth. Unfortunately, already the monadic fragment (only unary predicate symbols) as well as the 2-variable fragments (formulas contain at most two distinct variables) are not even recursively enumerable, i.e., there does not exist a recursive axiomatisation of the formulas that are true for some interpretation. This is proved by reduction to the recurrent tiling problem for \\({\\mathbf N}\\times {\\mathbf N}\\). The situation does not change if one restricts attention to interpretation in finite domains (but over infinite time, e.g., \\(W=({\\mathbf N},<))\\). Notice that the corresponding fragments of pure first-order logic are decidable. The contribution of the paper is that decidability of satisfiability can be regained if a) one restricts the purely first-order part to a decidable fragment and b) one allows at most one free variable in subformulas of temporal operators. For instance, the Barcan formula \\(\\exists x\\diamondsuit\\phi \\Leftrightarrow\\diamondsuit\\exists x\\phi\\) belongs to this fragment. This result is all the more interesting as the considered fragments do not enjoy the finite model property, i.e., there are formulas that are satisfiable (over \\((\\mathbf N,<)\\)) in models with infinite domain only; a case in point is the formula \\(\\square\\exists x(P(x)\\wedge\\neg(\\top {\\mathcal S}P(x)))\\) expressing that at any time \\(P\\) contains an element that was not there before (or in the authors' words: ``at every moment someone's starting to get old''). The proof of the decidability result proceeds using finitary descriptions of models (``quasimodels'') in which (the possibly infinite, see above) set of domain elements is replaced by a finite set of types, i.e., deductively closed sets of formulas in one free variable. The existence of quasimodels can be expressed in monadic second-order logic which is decidable by standard results of B\u00fcchi and Rabin.","type":"string"},"datatype":"string"},"type":"statement","id":"Q1591203$EF7A3452-8CFF-4822-8A88-9386815C8D3C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1591203$27D28DAD-DA07-4ECD-9BBC-FE4399F070C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1591203$E4C8D189-6CC3-4119-9993-8886D1DB66A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bf2726c5c2109371cc10358eaa69bc4df711caf7","datavalue":{"value":"68P15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1591203$ED04518C-2A47-481D-9522-A7B8A952634A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1591203$3D21C7BA-8095-4820-AE0A-521D7AB266D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"0c6e71133293256880be082f6af9aa793c57d433","datavalue":{"value":"68T30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1591203$B478C1D4-99BF-4038-8BBC-5B98297888BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a27f9f06d965be24ec50f61065e06d2029a566a7","datavalue":{"value":"03D35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1591203$D1DC58A5-A05A-4AC9-BA1B-CAEF48844873","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"757ace50bc0154ba5df34baff2839a6ec6d7f56a","datavalue":{"value":"1546600","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1591203$5045243B-BD8F-4C87-BFEF-19210084DFC3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4a1a1b4de2f6601636779c475343b36943870036","datavalue":{"value":"first-order temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1591203$0C080471-3B3D-41C9-9AE0-64ADB7116E14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1f8a8aa46d7a10c167f5cc47c4db94d00d884835","datavalue":{"value":"temporal databases","type":"string"},"datatype":"string"},"type":"statement","id":"Q1591203$54CA8834-2220-4422-A153-7C753334A887","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5006a9920f4095d0164c81800402e769b3f84a37","datavalue":{"value":"classical decision problem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1591203$D92C3BF2-8078-45B9-98B8-0534AAEDA277","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5033d3ae012d6c81208806815167a477d503a7c9","datavalue":{"value":"decidable fragments","type":"string"},"datatype":"string"},"type":"statement","id":"Q1591203$F43DEB97-C089-41FD-95E7-E0E37786D8AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"48fe5da30f2000a910dd1a06f280ea2b3174328d","datavalue":{"value":"decidability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1591203$E6F07222-719C-4E97-AE89-DD1A9BB39BAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a813fd0e4aef1fda5e8e7d4b77b02104337d96e6","datavalue":{"value":"undecidability","type":"string"},"datatype":"string"},"type":"statement","id":"Q1591203$8FD9B000-6B53-481E-9395-A1E81F57C31A","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":"Q1591203$28EFC12C-A966-4E36-98DD-FB1B5C25659F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"a49b20b1506647b1c87e6ed6310fb943dc6407f8","datavalue":{"value":{"entity-type":"item","numeric-id":1267082,"id":"Q1267082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$2A777D93-66E4-4BD6-82E1-2FBA36D1C9C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37e804d7aea2d1418057c94d927a03053fdf3435","datavalue":{"value":{"entity-type":"item","numeric-id":1601879,"id":"Q1601879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$61EC60A7-BD71-4D10-BB61-1DA8653547E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"570f9bb6e8727d3e369d07dcbff78755f5d7d468","datavalue":{"value":{"entity-type":"item","numeric-id":4868227,"id":"Q4868227"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$0D9D5229-F078-4DE2-8DF3-666CF288D8DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af4555c0d89e243a8a9351cedc1b4ffbfceace09","datavalue":{"value":{"entity-type":"item","numeric-id":5691140,"id":"Q5691140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$12FE7574-136F-494E-B446-113B0CB6C9E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06c411f40bd3fed70a734570dda325013084ac01","datavalue":{"value":{"entity-type":"item","numeric-id":5525343,"id":"Q5525343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$1A2AA392-7BF1-42D4-9671-7C0D304DFD9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"156138aef606bd7a7128a417f2c9b76b54fcbdfd","datavalue":{"value":{"entity-type":"item","numeric-id":1062669,"id":"Q1062669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$CF114207-F129-48E0-AD16-2F6667125AF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f344c7647a8246af45d15b042fc218567fc7a105","datavalue":{"value":{"entity-type":"item","numeric-id":4518442,"id":"Q4518442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$92EE2364-D559-4AAC-A8BB-BF9FCDBC6919","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e6d22c4f0f18fa0a8fa8a72b3aa3dd8f4f8c3a4","datavalue":{"value":{"entity-type":"item","numeric-id":1908342,"id":"Q1908342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$B18473FB-5E59-4152-848E-BFBFC6B73B10","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":"Q1591203$D432BD66-CDF1-458A-BF95-5DF5B925CFE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9f21257d8b20ccfecd3db595afbc8b2e1a0a737","datavalue":{"value":{"entity-type":"item","numeric-id":3835817,"id":"Q3835817"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$004B813E-9F7A-4C44-A519-01D1234B4659","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c17739bb71064dd8907ad80486b9d1ae9f0d4818","datavalue":{"value":{"entity-type":"item","numeric-id":2753192,"id":"Q2753192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$7C91CDC8-CDFE-4F2A-8298-196462E222CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b45af815584b281446704023f9f4c0865a4d4836","datavalue":{"value":{"entity-type":"item","numeric-id":4380448,"id":"Q4380448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$1CC3DE31-171A-4984-BECE-138A2B6E76C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"204f2846aa5f6dcc7929ed3391d28e2c9bd41326","datavalue":{"value":{"entity-type":"item","numeric-id":4342097,"id":"Q4342097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$C3849532-FC6B-4ECF-9E10-95039A0EDA8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c81c210aa51b53d004ca3564c20b46519be31e0","datavalue":{"value":{"entity-type":"item","numeric-id":4948538,"id":"Q4948538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$9794F889-EFB4-44ED-BEE1-747C2D6D3A05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1ef8e66aa90dfea81a83d36a53a90523adf29c22","datavalue":{"value":{"entity-type":"item","numeric-id":5567842,"id":"Q5567842"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$EACE46E3-7C56-494E-ACB7-136614BD49BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2152d089e8bc395eda60d52092b293f6b7e60d9","datavalue":{"value":{"entity-type":"item","numeric-id":4145760,"id":"Q4145760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$282D1EA3-F9B9-4154-B25F-0C6E41CA6F8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"967fb55b31b6e02bb24043a438b43c2e3c9e09dc","datavalue":{"value":{"entity-type":"item","numeric-id":4003410,"id":"Q4003410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$CF08B597-A6F1-42CE-804E-A7E9CCFBE71F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a73cb08d2241c15801016c9f2e93aa3828b1dd0","datavalue":{"value":{"entity-type":"item","numeric-id":5686019,"id":"Q5686019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$9348A883-71F1-41B3-BE76-B3B072A16E3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b54f7383e1361db9b7d8d635e3974eec1f15734d","datavalue":{"value":{"entity-type":"item","numeric-id":5536269,"id":"Q5536269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$45573F59-D68A-46EF-B137-7704C8ED4AAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"09dc0d5696d284e011b1160682f6fe6cbc5590fe","datavalue":{"value":{"entity-type":"item","numeric-id":4275689,"id":"Q4275689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$AE26E42E-6E0A-4498-A6D0-7F439513DAF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"edf96fd313efea8fcdd4baf3f82e7012dac99f22","datavalue":{"value":{"entity-type":"item","numeric-id":4110975,"id":"Q4110975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$D6EB1035-A1FC-429D-A987-592414002CFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f11e8548165a301d01a241362bcf1efce79d1f4b","datavalue":{"value":{"entity-type":"item","numeric-id":3746875,"id":"Q3746875"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$ECC38440-F17C-40AA-80C3-8ABACFF9DFC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b476279f9ef74fddb27272ad70ec34f0a4ec2a74","datavalue":{"value":{"entity-type":"item","numeric-id":5625141,"id":"Q5625141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$20AF1714-3C78-44C2-B62D-CC04F05F718B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4eb1d29f17f0fc309f325c3539d6d1791acef1b6","datavalue":{"value":{"entity-type":"item","numeric-id":2563451,"id":"Q2563451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$6D44E1D2-9BD9-4FB1-AEF1-3D8B7C21C778","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"534730d39bf1b2fb7e127c00d7c04e03699b9f80","datavalue":{"value":{"entity-type":"item","numeric-id":3949052,"id":"Q3949052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$7E1B2F2E-0F93-4158-9D77-64D57ABD1411","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"057befa3c9831a656354bf37a072a4972b35ed11","datavalue":{"value":{"entity-type":"item","numeric-id":1144955,"id":"Q1144955"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$46894C8B-F2D7-472E-AE6A-8C1B5E4C3C5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19bc50e2f4d2cceaac2ab96d0b4ab028848b7d4b","datavalue":{"value":{"entity-type":"item","numeric-id":4023900,"id":"Q4023900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$DB4B11DA-9E76-4C98-8BD5-529F0EF2BEF6","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":"Q1591203$8074801B-6229-4AE6-A30E-02D91E49DD4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1d9456d9b3e59e143f5e55b694b92114428f6e73","datavalue":{"value":{"entity-type":"item","numeric-id":1123184,"id":"Q1123184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$B97EB5A2-2614-4C1A-9429-B53754CFC2ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48e851c5380a2b1703132dffe3ce2f30a1f0b9e3","datavalue":{"value":{"entity-type":"item","numeric-id":2782498,"id":"Q2782498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$89DD7866-10A8-4DC3-8803-C19D608A3C09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"651d669f2b6e600c429f900f8a2c3a0056756db9","datavalue":{"value":{"entity-type":"item","numeric-id":2758067,"id":"Q2758067"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1591203$50E731D1-F22A-465E-A20F-CB5D9B32AF2E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7cd9a10fad6ac37e785df99a01759f9a14523506","datavalue":{"value":"https://doi.org/10.1016/s0168-0072(00)00018-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q1591203$12CE47D9-7AF2-4B5B-A271-E8BB256D3534","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a8364ae2e8e4324ac9a9fca53ffe85c3b82c4923","datavalue":{"value":"W2045554431","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1591203$0FAE3BA9-0095-4564-943F-E03ABFA22C2B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c493d075083faff0a7bd192dc11dfbb8af6d49b5","datavalue":{"value":{"entity-type":"item","numeric-id":1863828,"id":"Q1863828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1255f06b243ba2ab1d926bca6a193376c6c192e1","datavalue":{"value":{"amount":"+0.8368101716041565","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":"Q1591203$36FFB072-4FC6-4E82-976B-15593A0BC6CF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2ecfe897fd42087dbb77e7e02edb6a256aae0e03","datavalue":{"value":{"entity-type":"item","numeric-id":2996150,"id":"Q2996150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"796cacee9d282ee708b911d0738de285593b2267","datavalue":{"value":{"amount":"+0.832421600818634","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":"Q1591203$3F130A2C-DE5B-4BE5-B5DC-639677C60290","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3a6aca9a5039fba5f216bd8e6614355e9eea4c82","datavalue":{"value":{"entity-type":"item","numeric-id":4275689,"id":"Q4275689"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ab0f29cf5b252b8c14755a6fb49755ed1628080","datavalue":{"value":{"amount":"+0.8270795941352844","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":"Q1591203$1DD14F1A-B640-4A0F-97D8-C2AA8817A62A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"545d1c23e039802d3560269622daef18098c5313","datavalue":{"value":{"entity-type":"item","numeric-id":1849866,"id":"Q1849866"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3499bf03cf4c58cfa407172f57653059e5160293","datavalue":{"value":{"amount":"+0.8255660533905029","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":"Q1591203$BE8AFFEB-70C1-43E3-9F83-6FD4D8E0D5D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"214ff23f3b1d9be776a390d653a618fd8e0d2f03","datavalue":{"value":{"entity-type":"item","numeric-id":2958532,"id":"Q2958532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b2484d2a695f33f29dcad152521734de0fb96cc5","datavalue":{"value":{"amount":"+0.8227440118789673","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":"Q1591203$DEC40691-051A-4284-AB07-8AB9FF25FF53","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Decidable fragments of first-order temporal logics","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Decidable_fragments_of_first-order_temporal_logics"}}}}}