{"entities":{"Q910396":{"pageid":912244,"ns":120,"title":"Item:Q910396","lastrevid":65283006,"modified":"2026-04-12T01:31:55Z","type":"item","id":"Q910396","labels":{"en":{"language":"en","value":"An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4139720"}},"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":"Q910396$072FFB3C-F92F-464B-AB99-F914AA8F5ED7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c1090d5a97d1c8278fa8057a7ed9fa69371d60c8","datavalue":{"value":{"text":"An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q910396$4628BE37-D43F-4EBD-A43B-A9382E68795A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"61d525008476605108bbc6f06aba3f0a43a66f65","datavalue":{"value":"0696.03013","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q910396$8E4E592F-C0EF-49E5-8A97-85FC626020B2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6325d9f59cde8ebbdb24a9f950cab3fcef3decf6","datavalue":{"value":{"entity-type":"item","numeric-id":190248,"id":"Q190248"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q910396$EA90F0AA-E137-46A0-B016-FBBDEA7713C1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7211ad5ca16eb0d22cd0051fff3d0f3af254ceb6","datavalue":{"value":{"time":"+1989-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q910396$555A4EEB-F218-4451-8B5C-1A44AE7E163C","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"249889da91a4570e2c20fa467fcfaa11ca60eb40","datavalue":{"value":"A simpler and more direct proof of Csirmaz's model-theoretic characterization of Floyd-Hoare logic for nondeterministic programs is presented. As a spin-off, a straightforward proof of Leivant's characterization of this logic in terms of second-order logic is also given. Finally, a direct connection between Czirmaz's ``relational traces'' and ``time-models'' for nondeterministic programs is established.","type":"string"},"datatype":"string"},"type":"statement","id":"Q910396$E2F75E9A-2BA5-4BD6-8A02-5BDEE79A5990","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q910396$F840128D-5615-4040-8D71-EE519D63B84E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q910396$3596DAE3-52F9-41BF-93E0-CEFF3309A492","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4f2e3cadd2f390ad317a2d12955310d91bf6d21d","datavalue":{"value":"4139720","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q910396$C266D4D1-C717-4603-819E-C9CB72668991","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5d7bfc11de8cab95fd6af201970bd9d16d39bbd0","datavalue":{"value":"semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q910396$E82B37B8-4536-4E21-8370-7EA1689CA733","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c0f082d23ececda4495232af64202f592a5942f2","datavalue":{"value":"Floyd-Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q910396$60B8617E-A51C-4110-BCE5-A2062A6F16C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5e381b994a9c0ce3eb69287257f5288ebf06f2b7","datavalue":{"value":"nondeterministic programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q910396$A07AED67-A536-4354-9E5D-647D38A3AEAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5e01102226a676edcf182ed47a9896bd215db761","datavalue":{"value":"second-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q910396$3029261A-41F4-4B26-8FBF-38BB203A6E00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"50e22b7aa143ddad861eb3a40945fc6cdaede5e1","datavalue":{"value":"relational traces","type":"string"},"datatype":"string"},"type":"statement","id":"Q910396$98C96AA1-9104-4725-B174-79D52810C82D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8d59b19eea3397ff02e32c1a60233632f1e7d4c0","datavalue":{"value":"time-models","type":"string"},"datatype":"string"},"type":"statement","id":"Q910396$3B74F498-D2C9-4430-9421-7AE9B36665BC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e46a0c110e220042f8c25f69d7566fe58fbf25b7","datavalue":{"value":{"entity-type":"item","numeric-id":514567,"id":"Q514567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q910396$023D53A9-CB73-4A34-954B-66E82A5AF818","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"71c876594569243d8a46dba6a49cb7e4f79f826f","datavalue":{"value":{"entity-type":"item","numeric-id":375309,"id":"Q375309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q910396$5BF6A07D-709E-4EA3-A292-4EA2DA3EE2FE","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":"Q910396$5FF709B2-1C75-4845-B7DE-1FE96DDA18DC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6da2920b6a4d9a8f34f3af71327e991b97f8075f","datavalue":{"value":"https://doi.org/10.1305/ndjfl/1093635239","type":"string"},"datatype":"url"},"type":"statement","id":"Q910396$95D83137-8702-4CB8-99DB-3737424586D7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f21a050cf834544295697b5f4c21bcc5e0dfb155","datavalue":{"value":"W1972583224","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q910396$25D52F80-D50F-4E8F-A582-9E3E894BC573","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4e365861eaabf81c05e16d7f269e46e61dc692d9","datavalue":{"value":"10.1305/NDJFL/1093635239","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q910396$7754DD2B-C03C-43BC-8DF2-F859B8EB5D5B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7423c6b18bde8ebaa3ad7e0f0ef08b8ee7573835","datavalue":{"value":{"entity-type":"item","numeric-id":3814773,"id":"Q3814773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da46ce3d088189d97ee8ebcd621cc1f17e8f0ab7","datavalue":{"value":{"amount":"+0.823609471321106","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":"Q910396$3C3078F1-258C-4073-B5B4-734DB05B585B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7e62ffbc79872d6d9d9e1b33ea0221ff655d767","datavalue":{"value":{"entity-type":"item","numeric-id":3696488,"id":"Q3696488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b4aa9579e9abd66050bd4adf9ee2ab1bb98c28c","datavalue":{"value":{"amount":"+0.7973350882530212","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":"Q910396$A5A627C2-1C27-4E8E-8749-BF972979A3EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"564d497665b46c0c1d4a8904a118b7917bd17534","datavalue":{"value":{"entity-type":"item","numeric-id":1822934,"id":"Q1822934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"33463ee222621dfac056924f7fd549316428b2a4","datavalue":{"value":{"amount":"+0.7960305213928223","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":"Q910396$5B29DA9A-E529-4D71-9DF1-786FF8E3727E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7a6c2b5c7dbf2c0320ccb96a9147c3e9cb2fa32","datavalue":{"value":{"entity-type":"item","numeric-id":3348897,"id":"Q3348897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b32e628a97c6fae6e0b058c31016f1826adf1475","datavalue":{"value":{"amount":"+0.775263786315918","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":"Q910396$836825AA-F88C-45FB-80FE-13F7961DE739","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"747da4760684c4ae7c17554623ac1f638033033d","datavalue":{"value":{"entity-type":"item","numeric-id":671651,"id":"Q671651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"08f64997e853adfe0c16df46a05428b0a7927cbb","datavalue":{"value":{"amount":"+0.7701839208602905","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":"Q910396$E50ED13B-F453-483B-8623-823EE2F1E311","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An elementary proof for some semantic characterizations of nondeterministic Floyd-Hoare logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_elementary_proof_for_some_semantic_characterizations_of_nondeterministic_Floyd-Hoare_logic"}}}}}