{"entities":{"Q3559767":{"pageid":5589671,"ns":120,"title":"Item:Q3559767","lastrevid":50976467,"modified":"2026-01-16T01:20:36Z","type":"item","id":"Q3559767","labels":{"en":{"language":"en","value":"Program extraction from large proof developments"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5705580"}},"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":"Q3559767$1031810C-0615-4D22-9E30-977D88E2CF21","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4b748f2f9fd279ca80c0ddd8dee0757648dade72","datavalue":{"value":{"text":"Program Extraction from Large Proof Developments","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3559767$3E0BF38C-CDA7-4E50-8CE2-1750F2327B6C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f306f67b50104b58daefcab694dc09dff1abe96c","datavalue":{"value":"1279.68287","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3559767$B78B1E8C-BB5C-4BC0-BB01-9EDFD2BD0178","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6091b76cd84f0b1016acd69d49b968454ed131f6","datavalue":{"value":"10.1007/10930755_14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3559767$A714CF08-20B0-4C3B-8E28-27058837BEC6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"019239a5b99c9161ce4389de57414c8f40f605b4","datavalue":{"value":{"entity-type":"item","numeric-id":340573,"id":"Q340573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3559767$9388C598-D0F3-404E-A638-EC98DE3B9FBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"603d1427f1b21e289d7f29d1759e5e0b15783239","datavalue":{"value":{"entity-type":"item","numeric-id":185814,"id":"Q185814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3559767$37D26187-5ECB-4002-801D-703047870E47","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":"Q3559767$5467D3E5-CB9D-4FBD-9682-8376B152982F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"17e143d5b33c80948b67548d47c63ee6df7c9f0a","datavalue":{"value":{"time":"+2010-05-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3559767$C70F8B18-0ACB-412A-85FB-8811A4468D2C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3559767$8800549A-8938-4024-8F12-2D104F4220B3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"31bb539f8a2cddda6730879e0dd49ef5f0835c98","datavalue":{"value":"5705580","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3559767$CD172FDD-CEC4-4F9D-A21C-6AA87D553C0A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36a96860261afab88486624af0939a44f9aa584f","datavalue":{"value":"program extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q3559767$718A266D-8D20-4B69-B6F3-F8186283D50D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5830bc9df856ae2559fe681dc92cebe9ada5b3da","datavalue":{"value":"constructive mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q3559767$DE7C7D91-1358-40D9-AEFD-0FB18B6FB14E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3a96a510fd7a7846523150dd8bb125ef8f415fa","datavalue":{"value":"formalized mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q3559767$BC5920B5-1258-41E6-A2C0-4F335EEF2A50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q3559767$3BA74B32-3F6B-4279-A6AF-8F5CB5311B7B","rank":"normal"}],"P1463":[{"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":"Q3559767$0E0DF92A-6E02-4678-AF22-D9F88813D27F","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":"Q3559767$36FBBAE1-3E23-4CFB-BF44-D02180D15653","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4ff6fcdd4a54ffac5d3e15fdcca659959146a9f7","datavalue":{"value":"https://doi.org/10.1007/10930755_14","type":"string"},"datatype":"url"},"type":"statement","id":"Q3559767$1E6593D8-AFC5-4B63-92F9-A7B557BBD371","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"da99c73c81f684edf85ac44a99dac6af80dbab50","datavalue":{"value":"W2096282101","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3559767$A0085962-63B9-449E-A3AD-A23CBFFA4A34","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b914204adbf2ade3bbe867feab1b5e4407feb809","datavalue":{"value":{"entity-type":"item","numeric-id":2852042,"id":"Q2852042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cc56565a7be1114837c411ced999de29e9ffecd7","datavalue":{"value":{"amount":"+0.9020246267318726","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":"Q3559767$C3E1165D-9C40-498B-A73B-23EBBB9CD300","rank":"normal"},{"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":"589b169adc1f0256a52c01cc6750ccd4f9f5d42e","datavalue":{"value":{"amount":"+0.820641815662384","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":"Q3559767$AB953FEC-4137-409C-9D48-9BB6810A2465","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a13c8355df2c2ee6cf641c41615ae6ecc5f0661b","datavalue":{"value":{"entity-type":"item","numeric-id":5394420,"id":"Q5394420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6bc38f4a093d4627874e2c4dda878f015ac5859e","datavalue":{"value":{"amount":"+0.7831862568855286","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":"Q3559767$7267C521-D8EA-4DCC-84CD-BBF1DC803F1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f00b0b942310a027109a9d5f30966bef6363432f","datavalue":{"value":{"entity-type":"item","numeric-id":3613309,"id":"Q3613309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"28ef16fe29177ea1a7fa30a2a387ba007cef44a0","datavalue":{"value":{"amount":"+0.7681785821914673","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":"Q3559767$AA9AED49-D13D-4BAF-8C9E-C67F00127F5C","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":"db4cdfccb355c47c5b840f1fb482818423875774","datavalue":{"value":{"amount":"+0.767642080783844","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":"Q3559767$F7E75265-AF3D-4105-BE83-0A7CAEC256FF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3559767","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3559767"}}}}}