{"entities":{"Q5957850":{"pageid":8134652,"ns":120,"title":"Item:Q5957850","lastrevid":47759353,"modified":"2026-01-02T15:08:35Z","type":"item","id":"Q5957850","labels":{"en":{"language":"en","value":"Refined program extraction from classical proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1719165"}},"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":"Q5957850$0E413115-2A42-486A-A5CE-4FE8A98B19AA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0641bc0e47bfd118837ba047ff1dfd3bfa7a92c9","datavalue":{"value":{"text":"Refined program extraction from classical proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5957850$F8FC1BBB-9003-48AB-BD47-F37A08CD7DA2","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"87a1578594cb2109bac6a96a3585f61583f9924e","datavalue":{"value":"0992.03070","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957850$2F34E057-8C80-4F0A-8A42-04229F37DD2C","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2f435bcf4721c874a11eadf4c600c3a8b38aa5e6","datavalue":{"value":"10.1016/S0168-0072(01)00073-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957850$2B58585A-A737-4F1C-B7D1-CE2B20F0A6B8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"56802c23e662b5a0028381459762dce10bc420a6","datavalue":{"value":{"entity-type":"item","numeric-id":234584,"id":"Q234584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$1E81A5CF-7871-4424-ADD1-D5F97E0904AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ca3d0fdc4dfe73f15e4cc6198de2fda062014c98","datavalue":{"value":{"entity-type":"item","numeric-id":204229,"id":"Q204229"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$7BD0CE86-C089-472C-BCE7-8C75F7B3F90F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7d89967a655d20159aa875a5d9fe1d91c6683b97","datavalue":{"value":{"entity-type":"item","numeric-id":234585,"id":"Q234585"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$0FF89E2D-6750-4B55-9DDB-76B43E8800C3","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f91a4bcbc93435aed71775d25a4c5cd09e26f12d","datavalue":{"value":{"entity-type":"item","numeric-id":122505,"id":"Q122505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$9F54EA37-9D48-409D-BDA2-DE6D5F39D070","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4f8c686acf111f5870bb8b8a79eaa7f4f60ee12e","datavalue":{"value":{"time":"+2002-09-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5957850$1BA31F9D-3118-4DD9-9EBF-24C84E3E253B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"53a6dd9f6671ef90670f5c57fd3a10f9dadfeea8","datavalue":{"value":"03F10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957850$2494A4CC-7D0B-4508-B79C-8F3C900F8FDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957850$04213B3D-8356-4712-9997-B942FDA98836","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8612eb3fa5372f4e40168b827ed17a01cee8d8f6","datavalue":{"value":"03F50","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957850$5BB0D9FB-93C1-4FED-A9D5-9EC73A0429B8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"76528cb3d8e3e9e7920f307e55e7213e0b56127a","datavalue":{"value":"1719165","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957850$157B0480-FFBE-42BB-A525-7723D8F6B611","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36a96860261afab88486624af0939a44f9aa584f","datavalue":{"value":"program extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957850$BFE488CD-0EA3-4FFA-B29E-FD399604987F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bf6e42c550927d0b6dc1abdbb588fe518df848c7","datavalue":{"value":"\\(A\\)-translation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957850$C26BD9D8-754E-47A7-9FF9-63CDF0FAF62E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eeff098505e14bbf7804f5d4c62d458f4a1d2989","datavalue":{"value":"definite formula","type":"string"},"datatype":"string"},"type":"statement","id":"Q5957850$B15CCC4B-9670-48B6-9EF9-6CA8AA41397D","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":"Q5957850$D988DB28-6B37-4B4D-BD6A-F84D9E54B3EA","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1fdea4f58240b583e8d37e1858a840704f4b8960","datavalue":{"value":{"entity-type":"item","numeric-id":4281464,"id":"Q4281464"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$3106816D-2BAE-4859-8446-FE3B8948BEC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"934b7ab609179fc485a852b1dc9869b7fbb99b6a","datavalue":{"value":{"entity-type":"item","numeric-id":4883280,"id":"Q4883280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$0180617E-5272-4365-8035-FE647D7FE312","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d569ab003e4a3e84d1bb8ff03bcd65c8c355c84","datavalue":{"value":{"entity-type":"item","numeric-id":1595930,"id":"Q1595930"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$B31CFFFC-0A5E-4260-9F01-5F46AE516A6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe7f73b08df7100728ceede07434a97e2ff97fd9","datavalue":{"value":{"entity-type":"item","numeric-id":4012886,"id":"Q4012886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$C4AA1DE7-C849-4CC8-B72A-82B074B843E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61f80c309e64b1cfeded9c015638835fbb819eec","datavalue":{"value":{"entity-type":"item","numeric-id":1101435,"id":"Q1101435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$7D6A08CF-9A11-49E8-BF6A-CA03B7445940","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14199d752f4bebe689aaa85d75a54b5e20dfe3cb","datavalue":{"value":{"entity-type":"item","numeric-id":1199538,"id":"Q1199538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$D0E62332-5387-4DEE-9406-D2C2B291151B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20078d69304e2df97ca3f40332c8d92086a6b541","datavalue":{"value":{"entity-type":"item","numeric-id":4179016,"id":"Q4179016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$3CAE63D8-B953-42A0-B73A-939322DDF16C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9fa6c57aae1d21de49bf812d56ed5b9bb9f3500f","datavalue":{"value":{"entity-type":"item","numeric-id":3837732,"id":"Q3837732"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$06A69F56-5220-43DD-8E43-14D8533FDB1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c1e93b7524b60bb9ab3f8d71fd24ac2451f79309","datavalue":{"value":{"entity-type":"item","numeric-id":1326769,"id":"Q1326769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$E34D7560-2AC3-4950-80D0-FCEA699767DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4622804a4a5864d5bd07b0d1d16a6f64d614c609","datavalue":{"value":{"entity-type":"item","numeric-id":3722497,"id":"Q3722497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$5F88DCDD-A001-4DCC-A997-A2402ECCAE25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"66257d76632b86525de5e8f5c47c6c6cf781ec1c","datavalue":{"value":{"entity-type":"item","numeric-id":4255509,"id":"Q4255509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$B199944A-2B57-44A1-92E3-96EF633F1D4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"384c88ee747368e498e55b1ebc22017816448ffc","datavalue":{"value":{"entity-type":"item","numeric-id":2265415,"id":"Q2265415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$821A68FA-BDA2-4308-A6EF-62E063A0428D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25fc0f83d5ec3109942a6da644b57709f31b1dc6","datavalue":{"value":{"entity-type":"item","numeric-id":1188522,"id":"Q1188522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$B14CA636-7461-4B46-BF64-44E62E3705B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ac1ee249c73c16d45e6922836fb575790a28b14","datavalue":{"value":{"entity-type":"item","numeric-id":3353014,"id":"Q3353014"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5957850$49470972-2DCC-41AF-A274-3CF229328FAC","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"d0f572632b6a9e1670489fa4987b6c32f4defa9e","datavalue":{"value":"Q126421658","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5957850$B3E54A7D-DFA2-4955-AED0-4C610385C615","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8c64f6636386f48a39eb167327ecb52b30231284","datavalue":{"value":{"entity-type":"item","numeric-id":2752052,"id":"Q2752052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"db5c554e5da22df9cac3796fe069007e1550e937","datavalue":{"value":{"amount":"+0.9098197817802428","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":"Q5957850$A05CDB5F-8AFD-49B6-8516-BBF51A2CF881","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5c4de2f674dc67d9ed71923062e0cb417a719c83","datavalue":{"value":{"entity-type":"item","numeric-id":1882897,"id":"Q1882897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70db07731b37c94e58bc71bb506ccaf4507b97e8","datavalue":{"value":{"amount":"+0.8802618384361267","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":"Q5957850$5FC5AECA-36EE-4183-8731-75787C26CA7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2f3729b0e8c4dddb325f1b0df9df0be3d5efa45e","datavalue":{"value":{"entity-type":"item","numeric-id":4883280,"id":"Q4883280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"068119d1a59db5d22e58b1b4e32e87c9310cdefe","datavalue":{"value":{"amount":"+0.8642767071723938","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":"Q5957850$91460DA1-15C0-4DBC-8FF9-8DDFFC9960A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"096d21890c1496138948b96dc35d29ed108a275c","datavalue":{"value":{"entity-type":"item","numeric-id":2852367,"id":"Q2852367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fecbcdcd74b6ce27eb2b596fececc815a93e753c","datavalue":{"value":{"amount":"+0.8341770172119141","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":"Q5957850$5110EFA0-366F-4686-AE03-41594E253A12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b0037b042d10908455dbd830bb139aacf188ace7","datavalue":{"value":{"entity-type":"item","numeric-id":2482844,"id":"Q2482844"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"692dffcebed58964233e3df29be4cc5027439f6d","datavalue":{"value":{"amount":"+0.8337645530700684","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":"Q5957850$0D27ADB9-9703-4718-AED1-4C76630FD02A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5957850","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5957850"}}}}}