{"entities":{"Q6064277":{"pageid":13198435,"ns":120,"title":"Item:Q6064277","lastrevid":41654505,"modified":"2025-05-06T20:25:27Z","type":"item","id":"Q6064277","labels":{"en":{"language":"en","value":"Program extraction from classical proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7776716"}},"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":"Q6064277$BE8B8619-7F4A-447A-B17E-F5619D7EE96D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a295aec24e46394c86c7cec85381bb928f2b4d40","datavalue":{"value":{"text":"Program extraction from classical proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6064277$67481999-38F7-48EF-ACAB-17FD507F39F1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1f94d0d026b00ff9a32cbf09550f238e85af5a4c","datavalue":{"value":"10.1007/3-540-60178-3_80","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6064277$DB52E131-6D7F-42D8-B0B1-8050A6992403","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":"Q6064277$08D0FDE8-3C07-45BE-AD97-B744AE9D4E56","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":"Q6064277$239042A3-7A3A-40BC-AC5C-5436D4D4E674","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":"Q6064277$ED658A52-5345-47EA-81E8-0BE3BAA55E14","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"066d1477c8c2dc8167e035c2af02788021afe714","datavalue":{"value":{"time":"+2023-12-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6064277$AA9B69D0-0B6F-4829-AA24-F3CF1D1070B7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7a1d4d343889492e30dd853837039fd3cd08322a","datavalue":{"value":"03-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6064277$AE2820DF-E2AE-4CAF-B31A-EF7910DDF2D1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"68adc3c6e99d919a7be30eb2f5012b66bc92a1f3","datavalue":{"value":"7776716","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6064277$1C081DD6-20E9-413E-8363-56CC0441CDC1","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b4d0143549108a9da09a29aebec2ecbb52363908","datavalue":{"value":"derivation term","type":"string"},"datatype":"string"},"type":"statement","id":"Q6064277$654493AD-1FC7-45C0-B444-975DED175B59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a0a59e9d1948bcb3be072d2977517cfc6b207456","datavalue":{"value":"atomic formula","type":"string"},"datatype":"string"},"type":"statement","id":"Q6064277$50BE7A2F-5F85-4700-A940-624BA6F21EFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8d5f0a28de693e8b2b8d3680d78ebfe7bc738773","datavalue":{"value":"predicate symbol","type":"string"},"datatype":"string"},"type":"statement","id":"Q6064277$A60475CD-FDD3-43AA-8B7B-1D1708A498C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b0f753085618d72380bf71914f44fbaf7280fa64","datavalue":{"value":"closed term","type":"string"},"datatype":"string"},"type":"statement","id":"Q6064277$0DBAC29C-4224-4CC8-8953-71E9CD86C322","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fad0553e6f0be36cc67caa50c1ff2d40ad5675ea","datavalue":{"value":"classical proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q6064277$DC3C382E-5191-42B8-9F1C-4DA63ECF6647","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":"Q6064277$52B601AC-A587-4DBA-AFB9-5212B1CACE30","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2aab9a05a67cdce82745e3a6f914aa32ee0b5c78","datavalue":{"value":"https://doi.org/10.1007/3-540-60178-3_80","type":"string"},"datatype":"url"},"type":"statement","id":"Q6064277$6958CE98-EF79-4BB4-8CE3-139AA41D02DF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"612b7afec6ff70822cf383be08dc098f50f23b9a","datavalue":{"value":"W1511668160","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6064277$4B056DB7-3A46-4F5C-B66C-366A4A5B80E8","rank":"normal"}],"P223":[{"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":"Q6064277$34E29A3C-A923-4305-A49E-892ED1BAF3FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"58709679cfff7718457ae5dbfaa34a4e9b17219c","datavalue":{"value":{"entity-type":"item","numeric-id":5812263,"id":"Q5812263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6064277$7E4439D5-FA02-43F6-AECB-04CA1EA34163","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ac3bd59819bab3c20ab46afa2f257091fcd8fbd","datavalue":{"value":{"entity-type":"item","numeric-id":5344164,"id":"Q5344164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6064277$54CEC294-A742-484D-9FF9-5B8A6D0E8590","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":"Q6064277$6DE292DC-EFB8-4F09-9883-79130FE5ABC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ed0853d5d25943754f0b88d3bc5a4e688b584cb","datavalue":{"value":{"entity-type":"item","numeric-id":5734436,"id":"Q5734436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6064277$39AEAA5D-F995-4DF9-AB9A-1003D31E6851","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d2c7bbd8aeb065572be5518f5b89cf1cd49c3a0","datavalue":{"value":{"entity-type":"item","numeric-id":3718711,"id":"Q3718711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6064277$19FF26D1-4AB5-4DB2-BD1E-1F0288A1D8C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67fac3d055d90ee3aafe3674088228fa265868c9","datavalue":{"value":{"entity-type":"item","numeric-id":3138828,"id":"Q3138828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6064277$5685F4E8-E27F-446B-B4DD-0AC8D393343E","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":"Q6064277$4148C047-8221-4ACB-86A4-3153B55B8BAE","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":"Q6064277$00CDB2E0-930D-451F-B15F-9E1D8E5C157E","rank":"normal"}],"P1643":[{"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":"e7456902bfc6ea0c93f130ddbb856c41f8fb8994","datavalue":{"value":{"amount":"+0.9886949","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":"Q6064277$5985E3AD-2141-459F-AF95-F7826034E56D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bd717f4b364c057469372f99f8840236b942a9db","datavalue":{"value":{"entity-type":"item","numeric-id":5957850,"id":"Q5957850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2355043710f8dd15f05fda55c9e61c0c5ef3306a","datavalue":{"value":{"amount":"+0.9764682","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":"Q6064277$798E780F-FD69-4868-A908-184872BF9207","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4b4e9f165d8e7081b314ba650364565840fb38f7","datavalue":{"value":{"entity-type":"item","numeric-id":2876077,"id":"Q2876077"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"77a3b4886d40bb26fba0cf1413ffa89bba21461f","datavalue":{"value":{"amount":"+0.9667361","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":"Q6064277$A67C71AE-7469-489C-80CF-41F1BE84AA77","rank":"normal"},{"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":"2b1a280c157499dbb083fa03deee655fff166bf0","datavalue":{"value":{"amount":"+0.9573351","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":"Q6064277$2220CC72-5862-457B-8473-C22B45529446","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":"f6011dd98c162a400a4cd2185f77a661348cd9f6","datavalue":{"value":{"amount":"+0.95715475","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":"Q6064277$F31B5734-FD3E-46FB-9678-C1E4057ED4CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fac440234bc7126bd1963a74389d5ddb43e6c842","datavalue":{"value":{"entity-type":"item","numeric-id":3608421,"id":"Q3608421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10c7693bdcf3ff7ff07084f86548ae733c7bb3a8","datavalue":{"value":{"amount":"+0.9438892","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":"Q6064277$9D3FECB7-8F20-4A25-990F-75058CB1A71E","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":"ee2f3476737ab26df33b1b67f093a873eb9c4eca","datavalue":{"value":{"amount":"+0.9411589","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":"Q6064277$096AC964-E33A-4313-8ABA-85487CDEB09F","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":"74c71321899f32f57316147f4bd587427a2c0f18","datavalue":{"value":{"amount":"+0.9367628","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":"Q6064277$F8791A32-7660-46DD-8716-5A711BF28A79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b9152ec9adda1d6ca91f0619412e3b33aee49a0e","datavalue":{"value":{"entity-type":"item","numeric-id":3559767,"id":"Q3559767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"114e1220d3542c69302464dd1213b61639b8edd9","datavalue":{"value":{"amount":"+0.9355835","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":"Q6064277$9FC39E84-7C62-424D-8583-09C72C87E5D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"40b681b8f19e2d8c6c9e63744dd97ab3461df7f2","datavalue":{"value":{"entity-type":"item","numeric-id":4764104,"id":"Q4764104"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0d42d249df4beecaa8d388538d954bf7058f3309","datavalue":{"value":{"amount":"+0.9300696","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":"Q6064277$363FFDE9-39EF-442F-B6DE-5ECABDF978BF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6064277","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6064277"}}}}}