{"entities":{"Q808284":{"pageid":810132,"ns":120,"title":"Item:Q808284","lastrevid":64490853,"modified":"2026-04-11T20:13:48Z","type":"item","id":"Q808284","labels":{"en":{"language":"en","value":"Extraction of redundancy-free programs from constructive natural deduction proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4209628"}},"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":"Q808284$A0BD43FB-142B-489E-BFD1-310D5E28DC13","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"81cda8b619f522dffae21eb7b8957be67ab08a88","datavalue":{"value":{"text":"Extraction of redundancy-free programs from constructive natural deduction proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q808284$B20F5678-1E07-428F-9684-553D09795657","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0d229494c3a5fdc8413ec32ce1790693fbb04d37","datavalue":{"value":"0731.68079","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q808284$781599E4-D405-46D7-A60B-37FB30C1BB99","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"54b9bef84a10af8cf0df6dad904f1275e6d0f8f8","datavalue":{"value":"10.1016/S0747-7171(08)80139-3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q808284$90B7FCE9-F71B-4B4C-8FCC-AA69EBE8109B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b0ac016191ae608530c85a3d4a9c637d05fb94c7","datavalue":{"value":{"entity-type":"item","numeric-id":515712,"id":"Q515712"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q808284$A74D79D6-F693-4BB0-94C9-9A6DF05589CF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"ea72303f92787da89554ee5fa15621068821a762","datavalue":{"value":{"entity-type":"item","numeric-id":99061,"id":"Q99061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q808284$B6C65417-9851-454A-A7DE-DFCEA23A33DF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"391107ffc7a24346d69c573e292e4ff4587e3aaa","datavalue":{"value":{"time":"+1991-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q808284$FA0B84D2-3732-4864-920C-7C83CBA65240","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q808284$12C77731-9407-4594-B4E3-5DE36697387C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b4431676b39ce9114f9445f0ea956b51ba3d495c","datavalue":{"value":"4209628","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q808284$EDDD94EE-260B-4B50-A50F-B4E335930E63","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42b181a2d677c7dcc072d75332ed100453704fc5","datavalue":{"value":"automated programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q808284$52662084-A4BC-4917-90C8-B4B31DF33632","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q808284$15476B49-4426-404E-AE68-44A91F5666B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"06cd28244947e22f9075842138a2db5b118fbe9f","datavalue":{"value":"redundancy-free codes","type":"string"},"datatype":"string"},"type":"statement","id":"Q808284$AA8E3651-896F-4DED-944D-DCE02A62E553","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"595a1e75b49a7c35cfd3caaaff3a4e298be5d31b","datavalue":{"value":"proof trees","type":"string"},"datatype":"string"},"type":"statement","id":"Q808284$482976C1-F156-49EA-84D0-362BB9F6BA37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3102f4c12b5f51fd58e4f3324f426aac8a49e397","datavalue":{"value":"realizability interpretation","type":"string"},"datatype":"string"},"type":"statement","id":"Q808284$1EC523AC-1E19-4B82-9A1A-2F166656CBEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c4a62be59df86ac5656fbe65ad3e6c1589611bfc","datavalue":{"value":"constructive logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q808284$FDE81E5E-B817-4906-9C85-B899A2296C09","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q808284$6D36224B-FE3E-4FDE-B01F-5DFAC02B9A99","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":"Q808284$D144E975-DAE9-42BC-8333-90CBDEDEF867","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1b2e1ab8d6c4a6ea4362f203e5137d4541ef80eb","datavalue":{"value":{"entity-type":"item","numeric-id":3679172,"id":"Q3679172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q808284$8BD47A8F-EB4B-4FE9-9801-F71D6D895707","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q808284$0D94CDA7-5072-41F7-9181-443EA8AF911C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1435f3ecb80e66ef3a6c0e0b3b5e54cc7cafb970","datavalue":{"value":{"entity-type":"item","numeric-id":3880322,"id":"Q3880322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q808284$1D22F536-99D9-4CB7-9C1C-8C97EADD8151","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3ed33d75210f4b470fc995229f8d6e408696f04","datavalue":{"value":{"entity-type":"item","numeric-id":3922646,"id":"Q3922646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q808284$2225E2C1-C877-45AA-8A30-6562FEE9C99E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8d95625ec9e5b7c46cee42d87256157d982706a","datavalue":{"value":{"entity-type":"item","numeric-id":5559220,"id":"Q5559220"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q808284$AB421386-5363-47BA-A78A-6931E13E02A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"160a2374c05e466369d09ccede54688eb30beecb","datavalue":{"value":{"entity-type":"item","numeric-id":5183475,"id":"Q5183475"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q808284$A1E91D01-0337-4293-8FD2-27D8EE10EB72","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":"e473da9e59224ecf3531e13ae2aff5f58ee39c88","datavalue":{"value":{"amount":"+0.8216356635093689","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":"Q808284$B266EB0F-5B02-408E-9C00-7F293FA4BFF0","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":"b189efa82437d01a4d7e9fef76fdc5408d60c4cf","datavalue":{"value":{"amount":"+0.7675149440765381","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":"Q808284$87BA8FA8-3797-4E4D-9FF5-08F11AF3CC84","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe38b243283fc6821c4f28d3effddb01c571fd4b","datavalue":{"value":{"entity-type":"item","numeric-id":3166530,"id":"Q3166530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b8b29ceb219fac5ad113856b1bc16174ff1000ac","datavalue":{"value":{"amount":"+0.7672271132469177","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":"Q808284$E8659E7E-9204-4DE3-86BE-120A0FD1468A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6372b8a24cdca7c3de059415eb18caa3f796d520","datavalue":{"value":{"entity-type":"item","numeric-id":2946659,"id":"Q2946659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7771c864dbe1391147e6e893ad099af78c6153a9","datavalue":{"value":{"amount":"+0.7523461580276489","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":"Q808284$4CACAC2F-591B-46CF-8F13-23EFD2E22607","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"65e3d3670795b31d38c0853f7f79ca71b1eda741","datavalue":{"value":{"entity-type":"item","numeric-id":2703717,"id":"Q2703717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"87b227f569bf7fa66a1ce2e7f4a653defa30045f","datavalue":{"value":{"amount":"+0.7494190335273743","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":"Q808284$60A1D2D3-DD18-434C-944D-0C8992849884","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Extraction of redundancy-free programs from constructive natural deduction proofs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Extraction_of_redundancy-free_programs_from_constructive_natural_deduction_proofs"}}}}}