{"entities":{"Q2776809":{"pageid":2787547,"ns":120,"title":"Item:Q2776809","lastrevid":79572710,"modified":"2026-05-06T14:14:06Z","type":"item","id":"Q2776809","labels":{"en":{"language":"en","value":"Investigation on fragments of first order branching temporal logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1716766"}},"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":"Q2776809$23F13F00-2237-4CBE-890D-74B5738F20BC","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c69e18a237a828bf5021a70830f48f969f0d8386","datavalue":{"value":"1002.03016","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2776809$FA988FC3-B8F4-4066-943A-AC5EC7CFB05B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"70b479ab481d7ee1dcf779ab78c0b800106fa990","datavalue":{"value":{"entity-type":"item","numeric-id":167897,"id":"Q167897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2776809$3D489087-A7F8-4B15-A44D-7988A38390C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fcc31d8ba926152915a2d85bf90621c795d9f87c","datavalue":{"value":{"entity-type":"item","numeric-id":272304,"id":"Q272304"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2776809$082640C7-9C9F-4AED-8444-A8B4A1F0EA14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b7d0b58753731a5e52ea28d86170a3c6030e8f12","datavalue":{"value":{"entity-type":"item","numeric-id":835122,"id":"Q835122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2776809$E8115739-AF60-405D-B3D0-BADC34878737","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8ba0e16ec554a6a916fa7a31c1f3db10e36701a3","datavalue":{"value":{"time":"+2003-01-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2776809$B73517C2-8F5C-4EB9-9444-1FD7EAE8ABA7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e2244b32b83bf71a9c045223e635ab074452b389","datavalue":{"value":"03B44","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2776809$54DD995F-9A1F-4436-B77E-388A78959BDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"407654cf92f0702e03297e7fe541e25fa3f13c2d","datavalue":{"value":"03B25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2776809$44B58F48-0ADA-47D3-A413-9BFEA545C22B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2776809$8948904A-79BC-46D1-A394-9E6BC7311B45","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6ff50b231ba6ee70056caadb96d308c364d4e4c4","datavalue":{"value":"1716766","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2776809$E0576D82-226E-4453-99C2-90D84EB3ACDC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d7337af9f6bce53f4e5d1b336dd21d8919f47685","datavalue":{"value":"first-order branching temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q2776809$C94E2BBF-CFA4-4B92-A114-63FAC92F8DF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7c4978f2c4d263ef258ed0ffc576a325d510c4d8","datavalue":{"value":"axiomatization","type":"string"},"datatype":"string"},"type":"statement","id":"Q2776809$434CE49B-BD9A-49B0-89F4-62F2DF0F1D25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"15452eb31222caeb5fe592af73d040953a20cacf","datavalue":{"value":"FOCTL","type":"string"},"datatype":"string"},"type":"statement","id":"Q2776809$617FBD8C-2B7A-4D0D-A5BA-F36C37C6D022","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":"Q2776809$232EE777-ECA2-478F-8911-A4C4F1ED0715","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":"Q2776809$4D0A19E0-720A-4472-B063-140F80FD43EF","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":"Q2776809$F143C286-4D68-408C-9799-7FA8DCA7160E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"75393cc69a6235702aa0f9a4e7ebe9664b39cba5","datavalue":{"value":"W2050125564","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2776809$87D942A3-05CF-42C0-BA37-8E0B4F6B9250","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8bc0da1e1d1da2c5f69f11a2002cbe4bed5cb516","datavalue":{"value":"10.1002/1521-3870(200201)48:1%3C51::AID-MALQ51%3E3.0.CO;2-S","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2776809$51C1033B-50BA-49B5-B158-23953D0BFC3E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"dfc0bee17787117787c553e0561a5e8aae2a85be","datavalue":{"value":"https://doi.org/10.1002/1521-3870(200201)48:1%3C51::aid-malq51%3E3.0.co;2-s","type":"string"},"datatype":"url"},"type":"statement","id":"Q2776809$5CB3CB55-6D3E-4DC6-9B76-A4AFD6EEE251","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4c7f908f849214ee074ec35f82fa61624b29ca3d","datavalue":{"value":{"text":"Investigation on fragments of first order branching temporal logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2776809$60D2B1B9-0665-43C2-ADAD-35FFB25B9001","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"68cefe03c91c7bc1481d1ede29225e2a54af1e4c","datavalue":{"value":{"entity-type":"item","numeric-id":6561648,"id":"Q6561648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2776809$C89A66A9-5F86-487B-9410-1A320B5F2BF3","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a52472c3b04cdbf99ce8d7b56612eedc0464d0f7","datavalue":{"value":"Various fragments of first-order computational tree logic (\\textbf{FOCTL}) are investigated. The fragment of the logic with only the operator \\textbf{F} (sometimes in the future) is not axiomatizable. This is shown by a possible embedding of arithmetic into it. The proof can be extended to first-order linear time logic. It is also proved that the logic with the past operator \\textbf{H} (always in the past) is not axiomatizable as well. The proof is done by showing that the set of valid formulae of \\(\\mathbf{FOCTL}_{\\mathbf H}\\) is \\(\\Pi^0_2\\)-complete. The only axiomatizable fragment is the one with the next operator (\\textbf{X}).","type":"string"},"datatype":"string"},"type":"statement","id":"Q2776809$F2C2285D-5831-4B2E-9C13-D16B51C6515A","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"773908fafc294c05eb3467ec5d713b5469e8b7b3","datavalue":{"value":{"entity-type":"item","numeric-id":590927,"id":"Q590927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2776809$24BED85D-916A-4F5B-89E6-F53B7956D440","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"41c1e56272e89723df8b5c41e8c5c2cea135c272","datavalue":{"value":{"entity-type":"item","numeric-id":2856051,"id":"Q2856051"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"37b74955bdaef10a5260a9e2862631b8101c7492","datavalue":{"value":{"amount":"+0.8080614805221558","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":"Q2776809$71FD856C-9F17-416E-8E46-B625B2FCABDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a72ea4bea2ca32c16557917415d30c835acde50a","datavalue":{"value":{"entity-type":"item","numeric-id":4929426,"id":"Q4929426"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9568f44f176b4d3690c3f6c3d17ddd76603d3796","datavalue":{"value":{"amount":"+0.8009942770004272","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":"Q2776809$13008E24-42EA-4D16-A383-309A64B228B2","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":"7549d29338afe20485192f411390d8ef538b0ae2","datavalue":{"value":{"amount":"+0.7998395562171936","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":"Q2776809$23018875-1051-4248-AA99-57F6E31D4C6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8c4749c931588c31648c97654758bf0cdfb3dc96","datavalue":{"value":{"entity-type":"item","numeric-id":1591203,"id":"Q1591203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2765aad171e8e21b3fa453aa8b26698d9cb40b4b","datavalue":{"value":{"amount":"+0.7886289954185486","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":"Q2776809$7D576A52-3220-4B69-80D9-DB6268C38007","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":"f6e6c40ed269fc37e8e8b3d295086484c29cf585","datavalue":{"value":{"amount":"+0.7803337574005127","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":"Q2776809$624CCB3F-7F71-45D4-A6D2-49F7B5C2101A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Investigation on fragments of first order branching temporal logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Investigation_on_fragments_of_first_order_branching_temporal_logic"}}}}}