{"entities":{"Q5900714":{"pageid":8007000,"ns":120,"title":"Item:Q5900714","lastrevid":50958536,"modified":"2026-01-15T22:40:44Z","type":"item","id":"Q5900714","labels":{"en":{"language":"en","value":"Proving pointer programs in higher-order logic."}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5695395"}},"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":"Q5900714$79B8BC99-3456-4A54-847A-BF77A5E7FB81","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7e7c3f040a8feb248e6dc29a1def291c92088958","datavalue":{"value":{"text":"Automated Deduction \u2013 CADE-19","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5900714$09AD21EC-DC78-4620-B262-5FA5055F2936","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2a00cad163eef95d0568f43407392e06debd45ef","datavalue":{"value":"1278.68274","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900714$FABD5A05-58AE-46FE-9E76-23E2D2C924EB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"99cc5780872fde33eb92e2707a90697c7b2110cf","datavalue":{"value":{"entity-type":"item","numeric-id":2486584,"id":"Q2486584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900714$CB8FC08E-7BC3-4280-8C1B-56EB5F16D368","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bd39997decddd4925a8ef09cbbffc4f41d2b1f00","datavalue":{"value":{"entity-type":"item","numeric-id":670700,"id":"Q670700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900714$34DA8B28-D202-49D0-8EFC-65DE723E6750","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":"Q5900714$3DE1B608-A4A8-44D0-9AB0-143DC0E3CCE3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2c61bb6d282cc95675f5b726985d020f8b0e6f23","datavalue":{"value":{"time":"+2010-04-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5900714$56191597-A5B6-47C0-83DC-ECA83707F10D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900714$1CD01E18-055A-4B76-B1D6-8FB2B8300820","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900714$7E02A9A0-21E4-4E2F-B9B8-1478C38D2D54","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9288ceebc19683724aa3e97950b0da6b22b910b2","datavalue":{"value":"5695395","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900714$5F93E3A8-F7C2-4A9C-A788-33F0E8CF585C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5900714$1954DD36-8FF6-4A98-8BD2-7895C34FA9A2","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":"Q5900714$171774F3-154A-4E8F-85E4-4946FE0ABC16","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c1c668ddb4fae172b1931ef73496e5bcbc0e7e0c","datavalue":{"value":"https://doi.org/10.1007/b11829","type":"string"},"datatype":"url"},"type":"statement","id":"Q5900714$DB3C1D6F-6C3F-4755-A8EE-1F3E2C7574CB","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5f2de3997ca74820eaa5379240d8d8210d2079dd","datavalue":{"value":"W2483160171","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900714$792069CB-8FFF-460E-B564-7DD40934328D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"77803cf595c8808153636f8e001b2ddb16a0f0ed","datavalue":{"value":"10.1007/B11829","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5900714$C6028754-ABDE-42A9-9596-F7D780C00BE4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"49b75373f9f0445c42710ea3d755e0ae2535555e","datavalue":{"value":{"entity-type":"item","numeric-id":2486585,"id":"Q2486585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56788a68c1c59ee6d0f5ae9157d5436eb881ea25","datavalue":{"value":{"amount":"+0.99312561750412","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":"Q5900714$FD42C99D-A1F0-4A9D-AE81-E5386429E91D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6c0b9c32ef14dffa0a3544b1fd302ae3602cb353","datavalue":{"value":{"entity-type":"item","numeric-id":2721096,"id":"Q2721096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0a06a83d715ea56fe4a152609b65bd059452bb5d","datavalue":{"value":{"amount":"+0.8139293193817139","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":"Q5900714$98DB7007-5171-4F2B-930B-8DE2B6F547E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9568bff96434479bfcf5b344a457cece2ccb41c2","datavalue":{"value":{"entity-type":"item","numeric-id":3071444,"id":"Q3071444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec243a2195c3c3453418ffadf626f565d8d399fe","datavalue":{"value":{"amount":"+0.8123718500137329","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":"Q5900714$16625298-E882-4A51-BE69-9426114568E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"653bb42b19be8ce2e8f831ce06cf512b9e69994f","datavalue":{"value":{"entity-type":"item","numeric-id":5311261,"id":"Q5311261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0a5b333a3454eb7c57b5716f7dc9cfd81842c53","datavalue":{"value":{"amount":"+0.7810260057449341","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":"Q5900714$D8A97D7E-430F-41F9-AD95-47E57E391ABF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ddfe8706eb56f964bdfd12380be6a420c1d49e0","datavalue":{"value":{"entity-type":"item","numeric-id":3543655,"id":"Q3543655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"06ee45e11d6805073407dad79d62628733ca8888","datavalue":{"value":{"amount":"+0.7796199321746826","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":"Q5900714$1952D283-B3CC-4D85-B565-2D0FABF22856","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5900714","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5900714"}}}}}