{"entities":{"Q858911":{"pageid":860759,"ns":120,"title":"Item:Q858911","lastrevid":64878759,"modified":"2026-04-11T22:50:17Z","type":"item","id":"Q858911","labels":{"en":{"language":"en","value":"Formal proof of a program: find"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5115481"}},"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":"Q858911$E45A774A-D960-419F-AC48-796BA1222B61","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1375263f3432d10df09f1ae013144b4f9ca84da4","datavalue":{"value":{"text":"Formal proof of a program: find","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q858911$3C0AA985-C6DE-4E46-BEBD-81B15D57570F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"726a1315275dec45c64bdd85cf7c4900d45a75d4","datavalue":{"value":"1178.68353","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q858911$E0DED54D-9771-4242-8E93-5BA9171677B4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e5151e47b3481ef47c9a033843060abd7b1dc0f3","datavalue":{"value":{"entity-type":"item","numeric-id":352949,"id":"Q352949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q858911$125CA73E-1CA1-483E-81B1-E4D2BE876590","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4082512e7d3530b9726df691c7c28e9fec542a8c","datavalue":{"value":{"entity-type":"item","numeric-id":169675,"id":"Q169675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q858911$CDBA40D1-A27C-4DB2-B2ED-B76E4696CB27","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8e2bf25ad524fc43d672bc2587bd535911f4f3f0","datavalue":{"value":{"time":"+2007-01-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q858911$1C5500B1-427A-4EE8-BE10-4E499F692ACA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q858911$1471BD10-D2B9-4591-BC4E-6CAC51A5FEB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"517ace4a4f9c45a5475b4a8927a567447dbdb293","datavalue":{"value":"68N99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q858911$CAE5A0C7-C6FD-4B45-8999-1355358B5339","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6e91b0ca9fcef5aa1453ad12f28239217737d7f1","datavalue":{"value":"5115481","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q858911$D74F7B63-D088-46B7-A9FB-1B8CEC9CC9EC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f02f4db7bd17ba3fbae1be6bcee13dc9e5aa86bc","datavalue":{"value":"formal methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q858911$7B75D8E4-27B7-41D7-AB83-53C2589850E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8469432c7e2e4cd59d964f83e69cb11b07596610","datavalue":{"value":"imperative programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q858911$21CC63D2-F548-4F4C-B88A-F6884D945B24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q858911$5CE40759-9120-4AA5-B3AD-E804A3D0512F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"98456cd4cdf0db037b678749018452921ff9260b","datavalue":{"value":"Coq proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q858911$C908A227-445E-4BB6-918D-C8270828F7CA","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9aadc3562b5d3cd99740f94e9d46e7f210998eaf","datavalue":{"value":{"entity-type":"item","numeric-id":33419,"id":"Q33419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q858911$4E554D59-0E07-40A4-89E2-BBC6997EC8A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q858911$A22C6CB1-57F1-4004-AD4B-EA8CB92F7A8D","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":"Q858911$68108D2A-ABEB-4F74-B432-1F51AA91FC44","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4901ca39b8939ffaa1917e6818ff7a860a86aeb3","datavalue":{"value":"https://doi.org/10.1016/j.scico.2006.10.002","type":"string"},"datatype":"url"},"type":"statement","id":"Q858911$DE973E94-6021-4843-BD1B-AED2C63431DF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b802c2df42948c9252d46c2107083f95ab792ce9","datavalue":{"value":"W1971879297","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q858911$7E737F0C-6593-4677-A2AC-0B4C5626BC2B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"07274cb2ee65951954b1c6c13d39809c74f4d835","datavalue":{"value":"10.1016/J.SCICO.2006.10.002","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q858911$C9526438-17FE-4AF5-B4AC-E0653AE7EEE5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"40c8376339754f033a3a0b6702dec6f82357ed1f","datavalue":{"value":{"entity-type":"item","numeric-id":2764255,"id":"Q2764255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"816c94b88a445b43fa44a844cd8ae02da7380400","datavalue":{"value":{"amount":"+0.880666","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q858911$898C7942-CC53-487A-B49B-D2406EB5990E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c9ddfdd0c0639e442b2aadc92973a7dfa0dd16ad","datavalue":{"value":{"entity-type":"item","numeric-id":4733861,"id":"Q4733861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f690fda065f3408dcdcbe33f3bba9626fb8ab45","datavalue":{"value":{"amount":"+0.8738365","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q858911$02489563-F224-4E20-906B-295D770C2C6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"787bce44c26bfa68c4bdd6a337d32f1925d9a163","datavalue":{"value":{"entity-type":"item","numeric-id":3757915,"id":"Q3757915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2aa4d9fff6cef4e12750d42cb70226cc8d058c92","datavalue":{"value":{"amount":"+0.8738364","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q858911$5E3863DC-AC99-4F91-A2A9-0C34F36FF755","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d8068e23ea20162c700746f9d165209e24f53b1","datavalue":{"value":{"entity-type":"item","numeric-id":3219093,"id":"Q3219093"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d4b4b1aa70294460e35b72e96eba2c89291df639","datavalue":{"value":{"amount":"+0.86606145","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q858911$EB0AC339-3A97-4A70-9079-966358D8C8BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a89dc3f8b9c614d3c47ec807c896f5b07eb80c1","datavalue":{"value":{"entity-type":"item","numeric-id":3138828,"id":"Q3138828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d4b4b1aa70294460e35b72e96eba2c89291df639","datavalue":{"value":{"amount":"+0.86606145","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q858911$CD9E18D1-8606-449E-8C41-4E0FE50EB256","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ba5287e0aa1e87217bd42cd2d66e24afc654f209","datavalue":{"value":{"entity-type":"item","numeric-id":1820596,"id":"Q1820596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"158ef11cee620aba2c4b76c87d76fa472633548f","datavalue":{"value":{"amount":"+0.8465599","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q858911$7290AB5D-5CD1-4C51-AFF4-CE5705045E6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"59f8ddf71b2d5cd28cd251b780e95170840ac8ba","datavalue":{"value":{"entity-type":"item","numeric-id":1408657,"id":"Q1408657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"82a17fa3f27dc7027715df5577d5cfb790167250","datavalue":{"value":{"amount":"+0.8461487","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q858911$300550C5-043F-4AE5-9A71-CED6B057B7F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a397b65e7ad8983ba86aefde317b4b5f5c6ffde1","datavalue":{"value":{"entity-type":"item","numeric-id":3654818,"id":"Q3654818"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9231505168a26a085eb3aced88c529d8424c7ff1","datavalue":{"value":{"amount":"+0.84566593","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q858911$166F17E3-E1D6-4DF1-89EE-FC50C8385BCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a660e4dceed4f556c6af12fe4bc3a62ec1c67ef","datavalue":{"value":{"entity-type":"item","numeric-id":3525156,"id":"Q3525156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dfac0c7724a11e069dbbfa51265131260e573ebc","datavalue":{"value":{"amount":"+0.8451325","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q858911$E3DC9047-231C-42A5-8D1E-898F1B9383E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92c8794b5870b1144c6b99b340ca9276a2b2d395","datavalue":{"value":{"entity-type":"item","numeric-id":5690664,"id":"Q5690664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"60cb43d5f13b468e64037219b782274464edbfca","datavalue":{"value":{"amount":"+0.84496415","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q858911$11CAA07E-60D9-4C67-9A20-46694A994268","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formal proof of a program: find","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formal_proof_of_a_program:_find"}}}}}