{"entities":{"Q3083675":{"pageid":3094390,"ns":120,"title":"Item:Q3083675","lastrevid":86165726,"modified":"2026-06-03T15:43:53Z","type":"item","id":"Q3083675","labels":{"en":{"language":"en","value":"Program development by proof transformation."}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5869469"}},"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":"Q3083675$DD977FBD-EBFB-4BD0-BE34-639A5F6D14E0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"258e5b3d95fd5256fdf27142f45fea1006a2127a","datavalue":{"value":"1208.68012","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3083675$9A41B085-F524-48A6-80AC-A602F6D20AE5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a593ed7dad5ab1b97a7ca90b4accd58f1a60cb9e","datavalue":{"value":{"entity-type":"item","numeric-id":3083674,"id":"Q3083674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3083675$01575F17-62DC-47DD-9B9B-F9A7423D0733","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"49da2956fa5d0154b9b86484400b6efcafc64754","datavalue":{"value":{"time":"+2011-03-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3083675$AD79AC54-9C9F-418E-89A0-5C5F5E47860D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"bcb65603eb43c2f628d8a4f95e3763aa3a557c32","datavalue":{"value":"http://edoc.ub.uni-muenchen.de/11064/","type":"string"},"datatype":"url"},"type":"statement","id":"Q3083675$B14AAA6E-934A-4076-AC51-B94AB6D6534C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3083675$DF06B8BC-7FBC-4493-8312-315AD20C9C9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3083675$8352634D-7571-4C30-9E7D-9CFE00C5E8D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"625e55f1f2a96178239720bc1bbbe7ad21cf0a75","datavalue":{"value":"05C70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3083675$497CA289-DAAA-4681-B132-B459BEE68A0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c189c45b466f89dd188bd061df8c45f23f05da60","datavalue":{"value":"68Q32","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3083675$FE6DC068-0C14-4DD4-8E8A-FF0AD4D80974","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3083675$95A292A9-6D6F-4B0C-9961-FC2BBE5F11EC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b9cd83cd3e8c2cfcf3ddd895d9bfc31b2bda9e61","datavalue":{"value":"5869469","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3083675$676225C4-04DE-4D51-B32E-3126FE74118B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f34a54b9375c07ff1536abf8dba8e4259c5ed0ee","datavalue":{"value":"program extraction from proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q3083675$30EC5C1D-DE20-493C-84DC-49920B90C828","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc8caceb6e458ae5d7065db61236b098ed63a4b3","datavalue":{"value":"automatic and semi-automatic methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q3083675$BAB4BA64-7489-41BE-9DD4-CF7B3A44F7AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dd6c644762def59464159d6e17ca63b95129ab4a","datavalue":{"value":"extraction of efficient code","type":"string"},"datatype":"string"},"type":"statement","id":"Q3083675$F2F5CE00-B37B-4C26-8197-7D87DD862616","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"dc53d5be0e42bc6520cd105433c85abaabdce1c9","datavalue":{"value":"computational biology","type":"string"},"datatype":"string"},"type":"statement","id":"Q3083675$D43AD6B1-E683-448D-A978-68ACA9D91736","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7e212e013cb3d64e9bf9c43611c8ab8f8b9640db","datavalue":{"value":"manipulation of formal proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q3083675$4FC99F2B-F041-489A-9635-70482E4898F5","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3083675$E21D36B1-7DD9-4025-BCA9-2D0247577DFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3083675$D36C543A-6ADD-4D12-B31B-2C77DDE64A5F","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":"Q3083675$F731176C-B636-4D69-AAAF-16E94EDD1716","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":"Q3083675$E9B29F72-7856-4F31-8780-22B2195B9EED","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"31e06b4fe6c983bb3ab4de626b40fdcb19de88e0","datavalue":{"value":{"entity-type":"item","numeric-id":1823656,"id":"Q1823656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e0ed65d58fbba2e327f84f274bbbf735f335854d","datavalue":{"value":{"amount":"+0.8179262280464172","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":"Q3083675$89E204B2-1A85-4506-A776-059670D15D9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81235c4d3f4c66b6911717e8cbf43cd34a5bdfea","datavalue":{"value":{"entity-type":"item","numeric-id":912594,"id":"Q912594"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c048700b4d6c5612dd62a26577ee39838a935ca0","datavalue":{"value":{"amount":"+0.7967108488082886","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":"Q3083675$DB306A9B-27CF-4695-8FAA-615185DFE213","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6cc18ee63967d27b68bef5b3a1749be5e3c0935e","datavalue":{"value":{"entity-type":"item","numeric-id":4435458,"id":"Q4435458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5d93f7d51464a47c2e8df49243a6fdc83c84714f","datavalue":{"value":{"amount":"+0.7749921083450317","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":"Q3083675$112A1AAD-A966-48B8-A670-C01C9831C6E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6f59cfc1a0633b01260c3c05ad30aa1c6482bd35","datavalue":{"value":{"entity-type":"item","numeric-id":2722042,"id":"Q2722042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0605c0da4f6035afc1c4900b1c74138995bfbe94","datavalue":{"value":{"amount":"+0.7686616778373718","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":"Q3083675$BCC46C4C-1858-45E9-8E72-F44EFB8AD821","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c823eb76233e4855e66828e769991a47beaee71b","datavalue":{"value":{"entity-type":"item","numeric-id":1190474,"id":"Q1190474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d165f473c83b1edf2cf3eee8af4b1f6ed0240192","datavalue":{"value":{"amount":"+0.7677974104881287","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":"Q3083675$CD2CE9DB-A4C7-4B2B-9044-AF4BAB066CA5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Program development by proof transformation.","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Program_development_by_proof_transformation."}}}}}