{"entities":{"Q580955":{"pageid":582722,"ns":120,"title":"Item:Q580955","lastrevid":62924595,"modified":"2026-04-11T09:01:07Z","type":"item","id":"Q580955","labels":{"en":{"language":"en","value":"Total correctness in nonstandard logics of programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4018356"}},"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":"Q580955$B1DFA60F-0DAA-4E0C-B64D-009E4D4FAF05","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7680dc7a40f143c6d7281ca9fdfebbd288e75899","datavalue":{"value":{"text":"Total correctness in nonstandard logics of programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q580955$E0BA6B7D-58FB-4B2F-879A-C4791DD59BC6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"13f67efd5f5851754d74d3f353c26a1db47f8c42","datavalue":{"value":"0626.68008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q580955$A7C5E4C5-9D67-48D8-BEE7-C5E287B5D722","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"abb9c8dc8b6c24b780141814ed3380df2e338c7d","datavalue":{"value":"10.1016/0304-3975(87)90118-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q580955$FD67927C-FFB3-44EF-8CF1-0B506D8DAF96","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":"Q580955$4EA3F130-4CAA-411F-86C9-E9350B12410A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$4C703D53-D329-4670-8C7C-39638FCC5EF9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5ae48c61eed19d1e1e1f33f9255d5b329362d064","datavalue":{"value":{"time":"+1987-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":"Q580955$2907730F-05E7-4E1D-9909-00579218443A","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a93cb5b37b646e664977c8cff8b57bd32dee63e8","datavalue":{"value":"We show that termination is a first-order notion if approached via nonstandard logics of programs (NLP). We give explicit first-order characterizations of the program-verifying power of the well-known Mann- Cooper method for proving total correctness assertions (tca's). Similar characterization is given to the intermittent assertions method (w.r.t. tca's). A comparison of the tca-proving powers of distinguished methods (or logics of programs) is also attempted. We also show that NLP provided new methods which are strictly stronger than the Mann-Cooper method. In the end we turn to partial correctness issues related to the main body of the paper.","type":"string"},"datatype":"string"},"type":"statement","id":"Q580955$A934853D-79E9-4425-B30E-211E8B1DA00B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q580955$2B641485-6C8A-4A63-82FF-8DEF819CB893","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5c349c9325637490ac4069a00cd28f8659c1853c","datavalue":{"value":"4018356","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q580955$30BC1B38-B39B-4591-BA22-EC4A3BE95ADF","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4befa4ca20f2beabcfa09e8a92ae13c21cb4934a","datavalue":{"value":"termination","type":"string"},"datatype":"string"},"type":"statement","id":"Q580955$0CF31461-7532-4B30-A93E-B72DEC87A0D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b41ca3ff680462309afbd8ae6c121a3cf318dbb0","datavalue":{"value":"Mann-Cooper method for proving total correctness assertions","type":"string"},"datatype":"string"},"type":"statement","id":"Q580955$FF06BC44-C7C7-46A3-B08E-D78873130803","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4088ea78fedba65777215c3cc3346ea54dbf328c","datavalue":{"value":"intermittent assertions method","type":"string"},"datatype":"string"},"type":"statement","id":"Q580955$A7BDA9B5-6BCC-4C60-B1F1-22E699293E86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"24c0946ca1c7cece261e7cb3d3e9af5ea3b79649","datavalue":{"value":"partial correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q580955$91AFA23B-EBD0-4EEC-90FF-766AD8B3B820","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":"Q580955$7A999498-4DBE-449F-9B14-CEA65408B3C1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"24d7709efb3a122e87437d08dfbd1c29b2458835","datavalue":{"value":"https://doi.org/10.1016/0304-3975(87)90118-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q580955$15144661-0441-495B-BCBE-9ABCC803FE7A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"26f8fb73a43b8be08326769abd22ba821a8caf2a","datavalue":{"value":"W2015731361","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q580955$5518ADA6-97E0-492B-A769-13F7D6EB2BD1","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"fb041c142f8f3b9d02136ea04003c55bffb62e8d","datavalue":{"value":{"entity-type":"item","numeric-id":3309036,"id":"Q3309036"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$8DD98A6B-1E26-451F-8AF1-C7F290CD9EB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a28056ed53ef07a9d6632c6440711fd2b65f1640","datavalue":{"value":{"entity-type":"item","numeric-id":1159461,"id":"Q1159461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$FD45A822-CA03-4C80-8630-A583A8A0605D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19265f999b20cea182763ae6835a9a83234c03e1","datavalue":{"value":{"entity-type":"item","numeric-id":3939224,"id":"Q3939224"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$536AF062-EE8D-4098-AD44-A9C46FF22250","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d346d8485da0bc889f787fa277d331b616d4df2","datavalue":{"value":{"entity-type":"item","numeric-id":4054648,"id":"Q4054648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$D1AE87FD-8DE8-47EA-B05D-4C84AEDC3CD0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"264d5f802e0cf300ca5e5622dde1fd3d1d2ce45d","datavalue":{"value":{"entity-type":"item","numeric-id":5184385,"id":"Q5184385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$171CB048-0F31-4F93-9E60-8C19E9839C80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a4735154d50c08d584a8e28202802fa9d661654","datavalue":{"value":{"entity-type":"item","numeric-id":5679729,"id":"Q5679729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$431E544B-D03E-4BFB-826C-69DBB67EE6AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3b21e90a23a5672c558c84dfaa27ce2856c251a","datavalue":{"value":{"entity-type":"item","numeric-id":1162355,"id":"Q1162355"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$58741928-3848-439E-9E51-4A84D041BCD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7325afe239c801675ff5fbd404331d1656338d02","datavalue":{"value":{"entity-type":"item","numeric-id":760793,"id":"Q760793"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$8F6E7BD8-C491-44CF-B57B-37F58300E1B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1820c23955b4fdf05c16f6b7b19650e00ca1b28","datavalue":{"value":{"entity-type":"item","numeric-id":3960106,"id":"Q3960106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$07B1AA8B-70C4-456E-8705-04F18FB8B8A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9178378ae59b37fa519432d09b89f67083d636e5","datavalue":{"value":{"entity-type":"item","numeric-id":1822934,"id":"Q1822934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$3646A2D8-9566-4131-B011-9289E2A47A76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5f83c85c3c55b3dfc7804518e3d46331adb457c","datavalue":{"value":{"entity-type":"item","numeric-id":4726228,"id":"Q4726228"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$0C28C453-DA7E-41FD-BD73-3B76CCE67066","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f993ba5688ff98e9d0f8aae94e7a7a3a69e0c63","datavalue":{"value":{"entity-type":"item","numeric-id":1087866,"id":"Q1087866"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$C41BCE2D-0061-4BF7-8F9D-95503C3AE800","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"678f6c25497d4da339fb86fb797a401000099017","datavalue":{"value":{"entity-type":"item","numeric-id":4095834,"id":"Q4095834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$B6DA35B7-8017-4235-8EA0-1A69CF0A8C78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"914ef8719678eb4ee59028ba65b4741c8aa1bc8e","datavalue":{"value":{"entity-type":"item","numeric-id":4124327,"id":"Q4124327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$8C5BCD03-E771-4ABA-BF22-0665F1F15AFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b5d86b3b2e305f22a4acc54ca3b563db317be7a","datavalue":{"value":{"entity-type":"item","numeric-id":4190096,"id":"Q4190096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$5338904C-4F29-4AFC-A37B-3E7DE81D8E4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56485b9a4814bcf88c5da509c43cc487af1d7b47","datavalue":{"value":{"entity-type":"item","numeric-id":4144164,"id":"Q4144164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$0D9C70DE-4380-4C23-911F-47C9CC767F67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9378587a1115a0250a2395ebd434016b1bcd6dd","datavalue":{"value":{"entity-type":"item","numeric-id":4124795,"id":"Q4124795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$519B63AF-0A92-4FE0-B612-445A206FA795","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a7a3316329cfce249f69c13171c2ebaf3fd06f7","datavalue":{"value":{"entity-type":"item","numeric-id":3956390,"id":"Q3956390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$DB2475AE-519D-47CF-B7B1-93126C3E5254","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3ae2b43295e8f75713cc545a37c2780fa87a9c2","datavalue":{"value":{"entity-type":"item","numeric-id":1077159,"id":"Q1077159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$79DDFAC4-3A97-4BDB-B2CD-9040354C7177","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dfd4648d7865256acc81280168b5f250fc7289f5","datavalue":{"value":{"entity-type":"item","numeric-id":3744163,"id":"Q3744163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$F7D0B6EA-2C82-47CB-819B-EA23CD79C7F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"396fe5b9e8ccbc7dc1473c86accd716c3e50cd58","datavalue":{"value":{"entity-type":"item","numeric-id":3896482,"id":"Q3896482"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$937DF35D-889F-4B2A-ABBF-D94EA2B642E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ac09f0ca0f36729a8d14fbaa62e0e06b4e8b2c85","datavalue":{"value":{"entity-type":"item","numeric-id":3345770,"id":"Q3345770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$849231B6-BD13-4975-B183-2361EC5A11D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa88669227141db71dbbde7111e0cc29dbacbe07","datavalue":{"value":{"entity-type":"item","numeric-id":801661,"id":"Q801661"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$D7DE2688-FB27-4369-A651-689E02545F9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e388df98ffb3c87da06916b2ebf7f79e5efbed6","datavalue":{"value":{"entity-type":"item","numeric-id":910396,"id":"Q910396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$705FDB42-A72F-49EB-AD1C-1BF9E5EBDF07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"178206957f1ef7c0cd7065687539a80ddab0dcef","datavalue":{"value":{"entity-type":"item","numeric-id":3698302,"id":"Q3698302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$501B3939-CB20-45F4-880D-4FBF6136BD7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a1fa5d6f6c733523cd9ea7f235a2f6db60ee340","datavalue":{"value":{"entity-type":"item","numeric-id":3956920,"id":"Q3956920"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$AEA7BEF9-79A3-4490-9EF8-D9FC400F1EED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3c8db71b50348191b2d5879444039396cdc4a9c","datavalue":{"value":{"entity-type":"item","numeric-id":3678651,"id":"Q3678651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q580955$35519041-7660-43B8-870A-64005AF20A21","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"462ccb45add6f04c6de72dbc62e31a4ff085e986","datavalue":{"value":{"entity-type":"item","numeric-id":3325017,"id":"Q3325017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"556e8410a81bf6cc5ec57cbcd993a9b9345dc985","datavalue":{"value":{"amount":"+0.8876769542694092","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":"Q580955$D4096CB4-A9F7-4AA5-8E0A-51E924C2AE83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f1b2e59a3f1876b90ce4d0afbef5379583249040","datavalue":{"value":{"entity-type":"item","numeric-id":1077159,"id":"Q1077159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d1ab14a875d99e793df11ffef61e20cde482610b","datavalue":{"value":{"amount":"+0.82457035779953","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":"Q580955$BBACF055-0ECE-44A7-9185-77610E501D61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b9357f030428601ed694758b55100476237598b8","datavalue":{"value":{"entity-type":"item","numeric-id":3765226,"id":"Q3765226"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"735cb2edeb912757eb754b43666c324c2c393896","datavalue":{"value":{"amount":"+0.8016931414604187","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":"Q580955$09C61F87-F03A-4476-966A-A5F320B8EAD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f5298fdb8d2e6fd341daa55f0b2ca154afdcfd29","datavalue":{"value":{"entity-type":"item","numeric-id":3696492,"id":"Q3696492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"89e6d61b23da1cae13429b8f831b32951d0a738d","datavalue":{"value":{"amount":"+0.7946812510490417","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":"Q580955$784720C8-B3E5-44EC-B13D-825E14476F88","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":"ceeb82d7549a4a9c43eab848ed64340c49863692","datavalue":{"value":{"amount":"+0.7901516556739807","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":"Q580955$8FCA8EDD-713D-4559-ADDA-BA4CB07A33AC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Total correctness in nonstandard logics of programs","badges":[]}}}}}