{"entities":{"Q5887528":{"pageid":7917078,"ns":120,"title":"Item:Q5887528","lastrevid":47837812,"modified":"2026-01-02T20:26:03Z","type":"item","id":"Q5887528","labels":{"en":{"language":"en","value":"Does \u201cN+1 times\u201d prove more programs correct than \u201cN times\u201d?"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7673912"}},"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":"Q5887528$9C285603-4F74-456E-8BB5-972000EEFB8C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d45c55e9be9e0e8f04616cfddf5b36ce88047bd4","datavalue":{"value":{"text":"Does \u201cN+1 times\u201d prove more programs correct than \u201cN times\u201d?","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5887528$4122B4FC-657F-4DC9-8A4D-36569512781D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f9928cdf0614f460d2d0788ab060b18ff6bd5ab9","datavalue":{"value":{"entity-type":"item","numeric-id":585345,"id":"Q585345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887528$6C228D90-A0ED-4CE1-B214-89923331F147","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887528$36CE224C-0F50-4EBA-8F92-50C7C87A3C61","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7b4034943b182da069de8768d6fd2310f3e13487","datavalue":{"value":{"time":"+2023-04-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5887528$067BDD3D-1243-45FA-9407-4846023A0198","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5887528$5C305452-FB54-4556-80E9-149605705949","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5887528$F680DD24-6B27-4976-991D-B2DE3C7FDACD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5052b97d5501a6c6f67849d382e0289e3221116e","datavalue":{"value":"7673912","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5887528$AD3082E2-BC42-4BD6-AB21-9B5F6A309340","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a4a6f11756e1720f07cda5a080ef0476786d909b","datavalue":{"value":"temporal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5887528$CE70D423-DDC2-4132-94B5-A081CFA34062","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3875c79fa835ac45a1818de05c1bd8b1020c938e","datavalue":{"value":"Kripke model","type":"string"},"datatype":"string"},"type":"statement","id":"Q5887528$782FA111-56A4-4400-AE0E-448EA265D59F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"48a9d57224b4c90795ed16b4505d8da2503b1dae","datavalue":{"value":"dynamic logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5887528$51590583-05C2-4832-A843-2F5A1A0BD99D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eb237a09b46e833dd2d743fa4519378a856a533f","datavalue":{"value":"verification system","type":"string"},"datatype":"string"},"type":"statement","id":"Q5887528$0D8D38B6-7E64-409B-A3DC-5D0D95DA5655","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4d36c324f36852e43a8f480f694cb389b570968","datavalue":{"value":"validity relation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5887528$DFD398F6-231F-46E9-B0E6-9C0D67066531","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":"Q5887528$3C627EE3-ABCE-4FE5-92EC-7CC0497ED04C","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":"Q5887528$2E3DBB14-FAE4-4A69-8189-29DF4E4C78BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1270f4d60a05bd67d01053664f9cb16ad0f1e99f","datavalue":{"value":{"entity-type":"item","numeric-id":1159460,"id":"Q1159460"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887528$CFB7CB3A-188A-459D-A982-18D2A0718280","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":"Q5887528$039A3E68-C60D-4AD9-A6B8-91761B254458","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"435685dee5593ba6d147dc9e9c9a48bc32ce19df","datavalue":{"value":{"entity-type":"item","numeric-id":5551122,"id":"Q5551122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887528$7BE7ED5D-9F43-4510-B2A7-D03A893568CC","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":"Q5887528$866EFAC2-0C20-4B2F-BA55-EDC9836371D9","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":"Q5887528$AE8D08A5-C652-4F72-809A-A2AC5A9A09EC","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":"Q5887528$08C53F18-51B6-4B65-B4BE-710C3976E5A0","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":"Q5887528$914C066A-23E9-4DBB-977A-51F0BAAEBC07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f8e3d5efcad955e9874c3cad0d3e003718384f33","datavalue":{"value":{"entity-type":"item","numeric-id":1143164,"id":"Q1143164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887528$4D5E901A-F338-4A48-A067-9B3B46809F50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"016c26073336456ad938f5b7e58a2ad66e4632b0","datavalue":{"value":{"entity-type":"item","numeric-id":5556395,"id":"Q5556395"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887528$37D71AE9-24D1-43F0-AD2A-43EA64FC39C7","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":"Q5887528$664E7A5B-99D3-4F65-A81F-E8A33047DAED","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":"Q5887528$B5EE5688-44A9-46F8-B1AC-78DC8966B21A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"636ad5764b05f4af86c53cf69119bbb490e0e290","datavalue":{"value":{"entity-type":"item","numeric-id":5583835,"id":"Q5583835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5887528$DCBDE757-1C23-49CC-96B5-C00A6AB57335","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5eaf110a3d577177674e173b537294ca23c20c58","datavalue":{"value":"10.1007/BFB0040269","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5887528$428AD9DE-11ED-408E-99FE-A15595165193","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bce586cc7f691a30ec1aad8229a6a3d5c6c2dae9","datavalue":{"value":{"entity-type":"item","numeric-id":1825630,"id":"Q1825630"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a3eb80fff70f2b84da4787942204fd4179216c8f","datavalue":{"value":{"amount":"+0.8300914168357849","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":"Q5887528$07947D7B-1CCB-4D2F-B1FB-A76AD0C4621D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b9968a81f101b3dda94d0e82c4e51378c913a3db","datavalue":{"value":{"entity-type":"item","numeric-id":3341880,"id":"Q3341880"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"84cdd8b566c6f3c369f48e0be8ea4737c5e38897","datavalue":{"value":{"amount":"+0.7939590811729431","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":"Q5887528$5C692DE3-0D45-4F5D-9304-5ED57E0858AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0c42abca5f1957af99c29414df960c3ba393d8e3","datavalue":{"value":{"entity-type":"item","numeric-id":1071491,"id":"Q1071491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4be2c4dd29be45478ea662be4e181cfd3594bc4a","datavalue":{"value":{"amount":"+0.7915451526641846","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":"Q5887528$CA0544C9-715D-4085-A050-83928C583CCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7d2235f5043c5c02ba72156c260d6b677974f5e4","datavalue":{"value":{"entity-type":"item","numeric-id":3698302,"id":"Q3698302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1ec67a4557907e7416a4ada4167545e1671b8d71","datavalue":{"value":{"amount":"+0.7667489051818848","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":"Q5887528$05EB3B8F-5397-4F2D-BC52-3123AEC0AFB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6fc03231c8b2da69323dec19dd32ea7016e52a15","datavalue":{"value":{"entity-type":"item","numeric-id":3975138,"id":"Q3975138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88ee509de7f9f00bca1f92cd95bfc19c363b61ea","datavalue":{"value":{"amount":"+0.7552392482757568","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":"Q5887528$5636E243-41DE-47DF-8BC2-B87FCCBD0539","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5887528","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5887528"}}}}}