{"entities":{"Q5387904":{"pageid":7417478,"ns":120,"title":"Item:Q5387904","lastrevid":50366510,"modified":"2026-01-13T21:58:36Z","type":"item","id":"Q5387904","labels":{"en":{"language":"en","value":"Verification Condition Generation Via Theorem Proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5279586"}},"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":"Q5387904$2A00E5D5-8F7A-4AF9-BC8A-A0E295FEA81A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"98b6a06eb9662b14392f3f6b39a865c8e059e6fb","datavalue":{"value":{"text":"Verification Condition Generation Via Theorem Proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5387904$B5C9A0A1-D998-42FF-A241-0D88BAE24891","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7f8eb85457c8ad79bab718e58fe26952a2f3fab3","datavalue":{"value":"1165.68410","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387904$3AE61E21-B542-432C-9CC1-EA7074B1EF84","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5443b57ee860ccad5cd9d02b8075076a8992a71c","datavalue":{"value":"10.1007/11916277_25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387904$73F93DA5-8214-4796-9954-930E4D701172","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"23864e2be568bb8a6a4b0526f5a5216348320070","datavalue":{"value":{"entity-type":"item","numeric-id":2870110,"id":"Q2870110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5387904$D4A15708-7B4E-4CAA-9DDB-1DFB22E73EA9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6183386ae8366a240584c653ce5ca2494433aedb","datavalue":{"value":{"time":"+2008-05-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5387904$DE78F601-FE57-4BDC-B4CF-D069BF61575A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387904$676D5C26-66DB-4F2F-BDE1-55B5E75110FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387904$26EFECA9-66A6-4311-8709-1B115722FFDC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"24b182ed03fd99285c9b6126ebaff4fa0fa11b9b","datavalue":{"value":"5279586","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387904$BC2FD04D-D758-492C-893F-04382B2DD851","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"692549050d1bcf7f893cd2ef126329e66dbd37cf","datavalue":{"value":{"entity-type":"item","numeric-id":16529,"id":"Q16529"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5387904$10935042-A029-4A59-9316-9C78A9E58918","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5387904$985BEF4F-C2CC-463F-836F-D7CE11AC9C9E","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":"Q5387904$BF65B00E-EA89-4280-9ACF-DDA0736F9572","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"936692b93197a40b9024c8f64ff658675aea81b2","datavalue":{"value":"https://doi.org/10.1007/11916277_25","type":"string"},"datatype":"url"},"type":"statement","id":"Q5387904$C65AEF11-015F-46FE-AA75-FAE2C5B66642","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4f144237c7a0e4bc89a3c646e5e0acb0e2c7ae8f","datavalue":{"value":"W1484808823","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5387904$31C50482-D888-4C63-AC28-1903A2328976","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1991339c595d4dc97bb89adbbc394122047a0c35","datavalue":{"value":{"entity-type":"item","numeric-id":2864396,"id":"Q2864396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eb3153296c3f4e02014b4c165ed23b957655373a","datavalue":{"value":{"amount":"+0.770535409450531","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":"Q5387904$85521B56-B589-43D8-8B2F-A89C72CFE89E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2969032012922ddb21c6cdf39ed8ed34db5a8b98","datavalue":{"value":{"entity-type":"item","numeric-id":3599104,"id":"Q3599104"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8e9bdf20bd15fcb9a8e45c9b481066e6f04a6330","datavalue":{"value":{"amount":"+0.7657343745231628","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":"Q5387904$7817FA20-97AD-40AF-9F2E-10B34A504077","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"79daacd80091bde89a54cb32e28332e739a62c10","datavalue":{"value":{"entity-type":"item","numeric-id":465685,"id":"Q465685"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"54631d851a9df0dac27537822d782a677941c23e","datavalue":{"value":{"amount":"+0.7600338459014893","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":"Q5387904$3B5C7346-FC75-45B5-A87D-DD7B57265A34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"632ec0df6d73828d5ec403ae3e6c35a83d77a285","datavalue":{"value":{"entity-type":"item","numeric-id":4647514,"id":"Q4647514"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d6d3c9100dd540ebe8872f1f1a2b0070323383f","datavalue":{"value":{"amount":"+0.7517213821411133","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":"Q5387904$01BDE4FF-35B1-4E4F-81EE-DB95341F9661","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"47cb83556b7cef6399b3b254f5ad5b10124d3050","datavalue":{"value":{"entity-type":"item","numeric-id":1887136,"id":"Q1887136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2283df34e299bcf7ce4a3f3a1a6edb24dfe7d5d4","datavalue":{"value":{"amount":"+0.7337052822113037","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":"Q5387904$BE440497-22B9-44F0-B2D8-E2D53B315A2F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5387904","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5387904"}}}}}