{"entities":{"Q5255085":{"pageid":7284653,"ns":120,"title":"Item:Q5255085","lastrevid":41582942,"modified":"2025-05-06T02:29:58Z","type":"item","id":"Q5255085","labels":{"en":{"language":"en","value":"From program verification to program synthesis"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6445105"}},"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":"Q5255085$2F0FEC8F-101A-46F1-B7EE-7667A9A9D5BC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0e9c614a7574c4a7b34e2cf3c7ecd61b7064cbfc","datavalue":{"value":{"text":"From program verification to program synthesis","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5255085$CE200EA4-78A7-495E-BD05-302AAFF11CA3","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"29643c1132520dc15668a610b7f2688a0daee9cd","datavalue":{"value":"1312.68068","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5255085$807DF89D-5193-4B0E-A942-A2C3C7B7B45A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fd015dfffad784ae43e5424648e92328a11c8e87","datavalue":{"value":"10.1145/1706299.1706337","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5255085$810C58D6-F94B-4F34-BF74-DBD59542DF4A","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"98bc1c13cdde62372439ff6e02951c0fb3c14bd4","datavalue":{"value":{"entity-type":"item","numeric-id":1029010,"id":"Q1029010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5255085$26A455CC-3E2E-476E-BC23-FF4E9207EB14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"00b5dac73a626864066e391d75e33e945e00da80","datavalue":{"value":{"entity-type":"item","numeric-id":859959,"id":"Q859959"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5255085$F6F80AB8-8F65-4C91-9691-D28D62849801","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c998d1694ed82434d9591da5a17b5156805699c1","datavalue":{"value":{"entity-type":"item","numeric-id":2482437,"id":"Q2482437"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5255085$25ABE539-C806-4CC4-BCA1-0FAE05DC3E26","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0a5bbee3666eee3a652778234a38c4005afc7cb6","datavalue":{"value":{"entity-type":"item","numeric-id":5255055,"id":"Q5255055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5255085$2B8F338D-072C-4928-8273-32F2B0D1FE4B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"00c841ea08739fa38b76821129fbbdb6fe48b753","datavalue":{"value":{"time":"+2015-06-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":"Q5255085$E1E8F512-8350-4E35-BECC-12E2325E05F7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5255085$4E3A654F-1CEE-4761-BD37-D2648281AC14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5255085$545C67A4-88E6-4E6A-AA9E-425DB1AE59EE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"571c849755c709554655edb804555827a54a1d8e","datavalue":{"value":"6445105","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5255085$1256D6CA-AB97-4493-AEB5-C268BF5F7A7E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bb9ff00fd7fcaa42a90c7e1abdbfd95c6a8dc2f0","datavalue":{"value":"proof-theoretic program synthesis","type":"string"},"datatype":"string"},"type":"statement","id":"Q5255085$822EA836-8D45-49A0-B807-2141916FB2AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5255085$C5EFE76F-8263-45AA-83E4-EDD6319CB543","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":"Q5255085$5D37D447-B061-4A95-B3AD-C5A8529CA3E1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c31d4d92a5f9d868f3d654e5535d65e868db8dee","datavalue":{"value":"https://doi.org/10.1145/1706299.1706337","type":"string"},"datatype":"url"},"type":"statement","id":"Q5255085$BAF8C037-8290-4013-908A-9AFA24C2A5EC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0cf0bf0be320501feebb2c2263f17a237e4402c8","datavalue":{"value":"W2101432564","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5255085$821A7FF2-39D9-4C81-9B49-B9F29084E71B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2e1d31a1939b7e893a04b16b337fd391a8c5a3ef","datavalue":{"value":{"entity-type":"item","numeric-id":4335371,"id":"Q4335371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d129e05427387580f201269091404adb14be6677","datavalue":{"value":{"amount":"+0.9333246","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":"Q5255085$F3336E65-B412-45FA-88AC-66969D83758C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"150ec41cca31534b83a2031a23ff46f22a466d9e","datavalue":{"value":{"entity-type":"item","numeric-id":2945730,"id":"Q2945730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31d68e68de82ed97fbfebc329b70520dd3bb2a48","datavalue":{"value":{"amount":"+0.9215891","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":"Q5255085$5F15EBC5-EBBD-45B6-B958-4393B1B9F04D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b43363705e05d7362b8437881e77668b78ec908b","datavalue":{"value":{"entity-type":"item","numeric-id":5020648,"id":"Q5020648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"41f4893e27268ef15501eff59d76ccd4871ef7cd","datavalue":{"value":{"amount":"+0.90852666","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":"Q5255085$2EE2D04E-F29D-4A6C-B60C-3EC5B6098A05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"65783770f753a60e730e2f256403c2da900bb4d3","datavalue":{"value":{"entity-type":"item","numeric-id":3766816,"id":"Q3766816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f1db69ea0985881360140d84daa626c6cfaf8d41","datavalue":{"value":{"amount":"+0.9073829","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":"Q5255085$046A7794-008A-404D-886A-2CFBAEB37990","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"773a4408e9fab65ed6222ddff422c8d46a376e3f","datavalue":{"value":{"entity-type":"item","numeric-id":3691667,"id":"Q3691667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a6b1b3e44ee24b002062a55a46fea63fcadc5c9a","datavalue":{"value":{"amount":"+0.90350324","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":"Q5255085$B19C6DFD-57E5-4CC8-8F1C-5EFC5A2DEE86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ab116f62a0b733ec0afd5e508aec01a388df675d","datavalue":{"value":{"entity-type":"item","numeric-id":3685173,"id":"Q3685173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9d37fa54189045967f026b4629d7cb8cc1ea428e","datavalue":{"value":{"amount":"+0.9019101","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":"Q5255085$F3B56372-EBBF-4A81-B81D-F3D5D8E49F32","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe575bdeebfc69be36c9ab5b79768e2cdcba9f44","datavalue":{"value":{"entity-type":"item","numeric-id":2013885,"id":"Q2013885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a371f6ff8ee66bbe0bfb0190ac2f2ad21a113e6","datavalue":{"value":{"amount":"+0.8965382","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":"Q5255085$FB9232D2-B88B-4105-827D-FABFB6B70824","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ff7d60a6ce8052bfa56fde89469334cce4c5fa7c","datavalue":{"value":{"entity-type":"item","numeric-id":5447371,"id":"Q5447371"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f38eaf61ede938dc89b2ddd09cb5d61065cd027","datavalue":{"value":{"amount":"+0.89582926","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":"Q5255085$59FF78E5-2CA1-4178-ABF4-BEB3BF038F69","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5255085","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5255085"}}}}}