{"entities":{"Q794426":{"pageid":796274,"ns":120,"title":"Item:Q794426","lastrevid":64387689,"modified":"2026-04-11T19:31:15Z","type":"item","id":"Q794426","labels":{"en":{"language":"en","value":"Two theorems about the completeness of Hoare's logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3860375"}},"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":"Q794426$6CE5EF3E-50CB-4CD8-8726-8E20B76E31D2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fa23900651ccfb51718b0854ce67d2b2f5a79460","datavalue":{"value":{"text":"Two theorems about the completeness of Hoare's logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q794426$7A03DA38-1D9B-477D-9B2C-78EE06052155","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c74edbe5a9eced5b554189963a725af4a5e852f3","datavalue":{"value":"0541.68008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q794426$76FCD65F-A723-434E-A400-DD77FFE508B7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f70931ef750307cfdaa7ff6d42c34d1c2ff11ef0","datavalue":{"value":"10.1016/0020-0190(82)90095-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q794426$A4917E58-C885-4F4B-9BF6-E3AD89BB21BA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0c7e064d8bf44e919533bcd03f615423e66998fc","datavalue":{"value":{"entity-type":"item","numeric-id":549206,"id":"Q549206"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$F9FDFEA0-276D-4C85-A60D-E1B8C58A795F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"78ed6c5ce1e65f91c49ded91114a6800dd345a5d","datavalue":{"value":{"entity-type":"item","numeric-id":190306,"id":"Q190306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$27BA12D8-0233-486E-BBB6-04D40E8DCF37","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"52fa7d44b58d0511cb8993765bd916aef86052d8","datavalue":{"value":{"entity-type":"item","numeric-id":63092,"id":"Q63092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$D881F8D3-82A8-4ADF-A54B-1FF84270B547","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"47f57cd36df9e30d446df3867dc3917e4ea74654","datavalue":{"value":{"time":"+1982-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":"Q794426$691476F2-F33F-4E5D-929C-91AF0BAC2F8A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"044cb5d8916272da1ead72995bc02c7ac38be7da","datavalue":{"value":"This paper continues a series of papers of these authors on Hoare's logic and its proof theory. The issue that is addressed here is the genericity of Hoare's logic among all possible logics for partial correctness of while-programs. The results of this paper indicate that, in some sense, Hoare's logic is generic. The main result is as follows. Let (\\(\\Sigma\\),E) be some axiomatic specification, where \\(\\Sigma\\) is a finite signature and E is a set of axiom written in \\(L(\\Sigma)\\), the first-order language over \\(\\Sigma\\). If this specification has only infinite models, then it can be extended to a specification \\((\\Sigma ',E'),\\) i.e., \\(\\Sigma \\subseteq \\Sigma '\\) and \\(E\\subseteq E',\\) such that Hoare's logic is complete for partial correctness of while-programs over \\((\\Sigma ',E').\\) Furthermore, this extension is conservative both for first-order assertions and partial correctness assertions. That is, if \\(\\phi\\) is an assertion over \\(\\Sigma\\), and \\(\\phi\\) is true in all models of \\((\\Sigma ',E'),\\) then \\(\\phi\\) is true in all models of (\\(\\Sigma\\),E).","type":"string"},"datatype":"string"},"type":"statement","id":"Q794426$BB28EEF3-1E6B-402F-A742-7D9AB1DA2DC4","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q794426$069D8DCE-E8FB-46EA-8E9A-36A9C464CAED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q794426$CFE429E9-AD0F-4D61-9343-AFBB31741B03","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q794426$2A9074DD-1FC1-433C-BAE6-95D1A31D975C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9a98e1009cfe2d3ddd76f1c200856a5f38c5ab51","datavalue":{"value":"3860375","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q794426$3A654082-3986-4FD5-8ABA-DD0B86D2F02C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"158732d194a22169613049278f78b9fb482635ab","datavalue":{"value":"data type specifications","type":"string"},"datatype":"string"},"type":"statement","id":"Q794426$3FEBC637-F430-4226-BF2B-15E974CB09C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7b27366d5110501fbbf12e0924f51e7e73007fd0","datavalue":{"value":"refinements","type":"string"},"datatype":"string"},"type":"statement","id":"Q794426$712BB660-6595-45E5-9CAB-B5177AD78035","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6816fdf79dd11ac09d9af4886c02baab03d2cf9","datavalue":{"value":"completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q794426$4402154D-3041-4CCF-8822-026E7616A403","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7090cb2b2cefa03cee6b50a67ca057c086ad0f00","datavalue":{"value":"Peano arithmetic","type":"string"},"datatype":"string"},"type":"statement","id":"Q794426$CCAB6D12-932E-4503-806D-445EF83B3A56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c1e397bb1fe2346f2d830e122392d0b56774261d","datavalue":{"value":"strongest post condition","type":"string"},"datatype":"string"},"type":"statement","id":"Q794426$8A072BFF-AAC0-4B89-8898-531F940455A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a6ca3089f4a9c1f132e8f874f7fe0c6338d24ce7","datavalue":{"value":"Hoare's logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q794426$CEFB237E-08F3-4BBC-AB7E-F6AB23988922","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"83d5dcaa7aef3dc9ddc3eab92a7db35d53442c07","datavalue":{"value":"proof theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q794426$43747D88-90D0-4399-AB26-722767DE9062","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"92c6235562dc0eab11f092f0fd132bb65aa6d603","datavalue":{"value":"genericity","type":"string"},"datatype":"string"},"type":"statement","id":"Q794426$AAA5C351-022F-4BC7-9413-AF0A4CAAFF6F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6f6f5e21df80ad471474ec5ace8fdae126c95b37","datavalue":{"value":"partial correctness of while-programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q794426$07A65273-5ADF-493F-9B57-5267C8FD8916","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":"Q794426$C79E7002-0DE7-4758-B611-C84F15D29E2D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"35c9ce3faaa2c456b678972ce153d4bdf7ebebd2","datavalue":{"value":"https://doi.org/10.1016/0020-0190(82)90095-3","type":"string"},"datatype":"url"},"type":"statement","id":"Q794426$8A598756-2A86-4AEC-81E8-89ECEFB321DA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ce5990774693bad304d1f177fbc6fc0ddf5178db","datavalue":{"value":"W2019193580","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q794426$ADC6E0BA-A14B-439E-82BD-1716D3B13809","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3bc80122c3248b7370a66f915205122d19550f7","datavalue":{"value":{"entity-type":"item","numeric-id":3925144,"id":"Q3925144"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$EA438E07-A23D-4112-8795-83ABA7AF9FB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb12b188658ef9d46086882edec316113d94d7af","datavalue":{"value":{"entity-type":"item","numeric-id":3899466,"id":"Q3899466"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$2EB45A60-5B8E-4C0B-AB1F-577A6EB5FF35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4fc01beee0576bea6ea525779afa0e96e85c3165","datavalue":{"value":{"entity-type":"item","numeric-id":1158948,"id":"Q1158948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$86763E62-DB50-4260-856C-E31338601F54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de75c77cd108e2e05612b188e992ab7d56d3f44f","datavalue":{"value":{"entity-type":"item","numeric-id":3327706,"id":"Q3327706"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$3B56835A-84C9-4EA7-A420-9BD20EDA94DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5d6971c4054c6c2a549c4d4d04e54db2a8ed162","datavalue":{"value":{"entity-type":"item","numeric-id":1163369,"id":"Q1163369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$608DEF53-57BF-4DED-AF8E-6137FE86EE39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1295064b6ab47d21c7f067c44bf7ec955502d749","datavalue":{"value":{"entity-type":"item","numeric-id":3917477,"id":"Q3917477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$D0A13DA6-AC00-4698-AFA4-B09DA20ADED2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b401c9729a3a79ad3a6e76290465f59cc90ad74","datavalue":{"value":{"entity-type":"item","numeric-id":3878740,"id":"Q3878740"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$B541D7AB-3D8E-4D9C-B2B8-E1C52BA5B053","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"271435b73e7162645c02aeae8f7365e9fe6491de","datavalue":{"value":{"entity-type":"item","numeric-id":4741695,"id":"Q4741695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$4E79C44C-9ACC-4AEB-B3CE-FCDBFB130072","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"46da8ffdf2274c14640d6bc2876b88d285c9ab54","datavalue":{"value":{"entity-type":"item","numeric-id":3904041,"id":"Q3904041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$1BBE0CBD-A772-4DBB-934F-96CF40E806C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e2c71c26bf7e075dc23cee40b3135f1af13e67a2","datavalue":{"value":{"entity-type":"item","numeric-id":4151703,"id":"Q4151703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$6D57CB76-ADAF-48E5-AEEB-5EB66B163793","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac3af2a5d6d90fc35dbcdf27c89fba0731ef592c","datavalue":{"value":{"entity-type":"item","numeric-id":1233308,"id":"Q1233308"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$BBEBA3E3-2A22-4B0B-98E9-FC8649B9E0B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$76A1E969-BDE3-46DA-87ED-253045719A1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9635365b0780328d7ae22bc69b462e7144999d03","datavalue":{"value":{"entity-type":"item","numeric-id":5573961,"id":"Q5573961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q794426$AFC303EF-210F-4064-B03D-DAEA1D3BCD18","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f6be2716a73939a8ef5f5bd209f6b1fa11bcbaa2","datavalue":{"value":{"entity-type":"item","numeric-id":800082,"id":"Q800082"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ded73b8823f7ef1f647c16b326504a6e4abf6f7a","datavalue":{"value":{"amount":"+0.8838227391242981","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":"Q794426$4BB657EB-25FE-4037-8AAC-CCED37961BD2","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":"0219b75e48b19fe07171348a8f623969c0f233c2","datavalue":{"value":{"amount":"+0.8716151714324951","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":"Q794426$62EF5EAA-12E7-42A9-A30A-1F2356F1A0C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b033de07e3d56708ecacab644c5d61e90a196357","datavalue":{"value":{"entity-type":"item","numeric-id":3711743,"id":"Q3711743"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"71d0e75739a71828e4eb00c5476a2f7e5a09f93b","datavalue":{"value":{"amount":"+0.8510651588439941","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":"Q794426$5EFB522C-9AF3-4DA7-88EE-A8D153684CA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"672d995dd3428eb07ed30b7429a38292a5821170","datavalue":{"value":{"entity-type":"item","numeric-id":3763566,"id":"Q3763566"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6994b6e5ead8f3bb4cb2eadac5b1dfcc6996a57d","datavalue":{"value":{"amount":"+0.8428801894187927","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":"Q794426$11F22441-5216-408D-B73D-421F2A3F04FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c0ae49cf223900108061449596843f5e829fbcd7","datavalue":{"value":{"entity-type":"item","numeric-id":3327706,"id":"Q3327706"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"096754b367c329f418b90f205a544a390e9108c1","datavalue":{"value":{"amount":"+0.8408878445625305","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":"Q794426$1C6088DA-1AAA-4E96-9C41-B8341C0439F6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Two theorems about the completeness of Hoare's logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Two_theorems_about_the_completeness_of_Hoare%27s_logic"}}}}}