{"entities":{"Q760793":{"pageid":762642,"ns":120,"title":"Item:Q760793","lastrevid":64170540,"modified":"2026-04-11T18:06:54Z","type":"item","id":"Q760793","labels":{"en":{"language":"en","value":"A completeness theorem for dynamic logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3885300"}},"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":"Q760793$94F7A9F7-D7C9-4158-A439-CD3C2472D108","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c5837df31da2de3f6775f2d535d14a24d5549b68","datavalue":{"value":{"text":"A completeness theorem for dynamic logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q760793$BAB0C746-1D2A-4540-9013-91B0E4F51CA9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b82a13a93d7994803f81f0ecee3516a4b1635145","datavalue":{"value":"0555.68012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q760793$96FFD108-3D7B-4915-A2A7-F0AAD04E2194","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ee4e70b5a3726ad737c6aa92da85e135ebf1b133","datavalue":{"value":{"entity-type":"item","numeric-id":247008,"id":"Q247008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q760793$D570E1D8-505C-4C19-A073-884AF996DC31","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":"Q760793$481FD55D-6C9D-4F6C-8036-86234EA585BA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3c94df5c9af0ede578c52141befd29044de13172","datavalue":{"value":{"time":"+1985-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":"Q760793$3242DAAB-70DB-4244-9478-D424BFA7AD04","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"307c4502e752fbc52fc6f6e267faf881e9a522a2","datavalue":{"value":"The celebrated method of \\textit{R. W. Floyd} [Proc. Symp. Appl. Math. 19, 19-32 (1967; Zbl 0189.502)] and \\textit{C. A. R. Hoare} [Commun. ACM 12, 576-580 (1969; Zbl 0179.231)] makes use of inductive assertions for proving partial correctness of programs. There are partially correct programs which fail to have adequate inductive assertions [see, e.g., \\textit{H. Andr\u00e9ka}, \\textit{I. N\u00e9meti} and \\textit{I. Sain}, Lect. Notes Comput. Sci. 118, 162-171 (1981; Zbl 0481.68035)], but this paper shows that this can be remedied by giving an alternative definition for the run of a program.","type":"string"},"datatype":"string"},"type":"statement","id":"Q760793$A1BB42E3-8F5B-4D9C-B705-7A61861E0695","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":"Q760793$AA011520-FE1A-45CE-8464-F33DC338ABD6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q760793$57D13AFB-4AD2-49F7-A015-7D21072220D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q760793$774C9063-2CBA-46CD-8E67-CC4C24DE6B93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q760793$D38B6E25-98FE-48AF-BB15-E010C8732406","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b2c86b4c11779e42d9ae98b8631d6c22cd4328f2","datavalue":{"value":"3885300","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q760793$FC8E23D0-52D9-4E2F-82B0-08DB31F9286B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2a014d734bf51d13082b763d49735a3af1ce1c55","datavalue":{"value":"Floyd-Hoare method","type":"string"},"datatype":"string"},"type":"statement","id":"Q760793$E38FAAF7-6F8A-4EF7-A054-6340131E5B56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"120651316a0505db449221e2a59731e8297a7415","datavalue":{"value":"inductive assertions","type":"string"},"datatype":"string"},"type":"statement","id":"Q760793$7D3F61CB-A85D-410F-B4AE-33F3638B25D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"24c0946ca1c7cece261e7cb3d3e9af5ea3b79649","datavalue":{"value":"partial correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q760793$92198E44-C75D-49EF-8508-B849DED72E98","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":"Q760793$D4366931-DE3D-4C77-A34D-823DE9EB8F27","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ac1278eae77f26fd6c39069c6c11cfe7c3e27661","datavalue":{"value":"https://doi.org/10.1305/ndjfl/1093870760","type":"string"},"datatype":"url"},"type":"statement","id":"Q760793$E7EAB47D-9446-4974-B521-FE22D50EFE7F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"14fbdb2105bcfda743a4b94633308fbd2772890e","datavalue":{"value":"W2001982768","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q760793$C2318F9C-8726-4DAA-88AC-6490061598C7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1210c786e7db6af829da7502306f7aeb3eb12f79","datavalue":{"value":"10.1305/NDJFL/1093870760","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q760793$F5391DE4-8FFD-4BA4-B62D-02FFE6344517","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7bcfbe2ac44a0dcc2f5957fdd3687861fdc199a5","datavalue":{"value":{"entity-type":"item","numeric-id":3617722,"id":"Q3617722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dfc47c372e144e204a77d448c94d638976f450ff","datavalue":{"value":{"amount":"+0.8379455804824829","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":"Q760793$44F4AA3C-8A97-4D32-8594-B46472DCD446","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a84e644170331a6a9485b207c047e686cd4d5525","datavalue":{"value":{"entity-type":"item","numeric-id":3826528,"id":"Q3826528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2970a448bcfb708bf8440aaf461dbafef602cd2a","datavalue":{"value":{"amount":"+0.8245704770088196","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":"Q760793$AC333933-1D15-4D0F-8E94-724CC271477B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81ba4920e4cd0070412225e45f447d2a5d262358","datavalue":{"value":{"entity-type":"item","numeric-id":3337453,"id":"Q3337453"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"abd0772b8fffde48e7c25fe460f8460e24cc3065","datavalue":{"value":{"amount":"+0.8164849877357483","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":"Q760793$E02BE6F8-AB65-4460-808B-F107F184AB54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ebb5c56932ff269ab571dbc7900d427089f6827c","datavalue":{"value":{"entity-type":"item","numeric-id":5308458,"id":"Q5308458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f891026782301d26c19cfdff8c4db907e0a40f21","datavalue":{"value":{"amount":"+0.8082206845283508","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":"Q760793$68651EEC-3060-41A4-990F-8A815FB26226","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"06b4dbc68b06bc8ecd04f5d1802c7e4cf586f269","datavalue":{"value":{"entity-type":"item","numeric-id":1110500,"id":"Q1110500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9649cef6fcd9a1cb2f8eba772202ed29252a160b","datavalue":{"value":{"amount":"+0.8049429655075073","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":"Q760793$16969C0C-0673-4907-8DCD-8FB1A33D9D09","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A completeness theorem for dynamic logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_completeness_theorem_for_dynamic_logic"}}}}}