{"entities":{"Q1769440":{"pageid":1780182,"ns":120,"title":"Item:Q1769440","lastrevid":43317936,"modified":"2025-07-24T16:23:47Z","type":"item","id":"Q1769440","labels":{"en":{"language":"en","value":"A direct proof of strong normalization for full constructive second-order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2148380"}},"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":"Q1769440$35F5ADE4-558C-4393-BCA9-D763C1515721","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2b2886086162c1ecdbc69d3dd2af941b4cc9da87","datavalue":{"value":{"text":"A direct proof of strong normalization for full constructive second-order logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1769440$576BE9E4-D4C4-4447-BD7E-0A43BCF83732","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"eff853d9518777ae4ff21a54a3c19f5cf5bc2686","datavalue":{"value":"1069.03005","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1769440$3126A36C-380E-4570-80B8-4F73A2827849","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ff92353fb34e95f211754f35aa330860b987a356","datavalue":{"value":{"entity-type":"item","numeric-id":740208,"id":"Q740208"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1769440$78B626AF-12B4-4844-A5C1-543D61A7A1C2","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b69937174cb511278b81023a5b2696450fbeee7f","datavalue":{"value":{"entity-type":"item","numeric-id":171286,"id":"Q171286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1769440$D0E55083-C954-45F1-AC06-92BDEE846122","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"11b4b9e71888c8ae87efc4750955ed379903fb79","datavalue":{"value":{"time":"+2005-03-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1769440$E981C402-939B-43D7-BC16-4BF30A95A844","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1769440$383D5C33-0B5B-47D2-BA19-894D7E570683","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1769440$5E9A4FAA-25F3-4055-8A6C-FC987BD8FECE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1769440$70D01527-18EE-4102-92C6-D8445725E6E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1769440$8F54D63B-C484-4888-968B-A4A988E3A541","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a6d53bd5b3e4863a2c00b8dece043e872c0a65fa","datavalue":{"value":"2148380","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1769440$90998FD7-D73E-4DBE-9FD8-504854214D4C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"36a96860261afab88486624af0939a44f9aa584f","datavalue":{"value":"program extraction","type":"string"},"datatype":"string"},"type":"statement","id":"Q1769440$F2B878A6-26CE-4415-A14A-2058DACB8064","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"feac4878036376652fb2850261e6224d2a3b5ec1","datavalue":{"value":"Curry-Howard terms","type":"string"},"datatype":"string"},"type":"statement","id":"Q1769440$35CB5BD1-4F2D-4D06-8900-A9D78298AC02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5e01102226a676edcf182ed47a9896bd215db761","datavalue":{"value":"second-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1769440$4B6F3AF0-D982-4683-97B9-9DCA10CB71D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e395ae2d636478627cecf428dd6a45aad417915b","datavalue":{"value":"strong normalization theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q1769440$69F71897-7ED7-48A3-87B7-C1024300FA74","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":"Q1769440$7E7F0AD9-3E5D-4ADE-B403-870730418EB4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d97faa2ac5a7df01c3b864c90903470d7e32d38","datavalue":{"value":{"entity-type":"item","numeric-id":4382485,"id":"Q4382485"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d54578ab21c63f53de9943b2404e96e5f2d5ba3c","datavalue":{"value":{"amount":"+0.94168854","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":"Q1769440$437B19EB-E343-40B8-8B49-822EE5C0A85D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"edf288d97bcbfd54f497c29d54c5db6fc93f37b3","datavalue":{"value":{"entity-type":"item","numeric-id":1044837,"id":"Q1044837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e71fe08bd6df80d1499c3023b2725b4e29d8be8f","datavalue":{"value":{"amount":"+0.92746717","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":"Q1769440$20971E65-704A-4690-BAE8-3482D03C44AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2378f33955b6e304d54ef59f2d34fc42eeae13ac","datavalue":{"value":{"entity-type":"item","numeric-id":1407527,"id":"Q1407527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"580016e15100f96deda5adf95aa4277d5f08a06a","datavalue":{"value":{"amount":"+0.9175082","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":"Q1769440$A31F83E3-D2E6-413C-B258-3063D57D36B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"92ff76a30a27650efc005ec47abf96c99638ef80","datavalue":{"value":{"entity-type":"item","numeric-id":4650260,"id":"Q4650260"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53421607ebef6157803539a06556f1183d3e57c8","datavalue":{"value":{"amount":"+0.9149127","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":"Q1769440$BA6169DB-45C2-4F17-8C51-AC09459DF969","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d45c7dff42ba9946e9a8acd3e138332c15ef18e2","datavalue":{"value":{"entity-type":"item","numeric-id":1902976,"id":"Q1902976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bbf8fc80d9740af7fb9c673045b57063fd314d2a","datavalue":{"value":{"amount":"+0.9137335","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":"Q1769440$7907BFD2-608C-49B3-B939-2B3CE4C824C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a6fdcddadbf3da5f3e6fd0b5fb36d0f4b317eb3a","datavalue":{"value":{"entity-type":"item","numeric-id":818927,"id":"Q818927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f368d3d60b29cc1e6989cebfeed494c80fbd8151","datavalue":{"value":{"amount":"+0.9129324","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":"Q1769440$8726AE36-05C4-49FE-86A8-EF2EBB6F870D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce593f3b388a79b0e95969ed8b7309993d112c8b","datavalue":{"value":{"entity-type":"item","numeric-id":1744419,"id":"Q1744419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"413a3c127a6a772783c46d9a179af260673dcb26","datavalue":{"value":{"amount":"+0.9046724","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":"Q1769440$CD4531E3-8F4B-4AA6-B825-FAE36CAAAE68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9c09444982f9bd042910875767a1ad6a22df771f","datavalue":{"value":{"entity-type":"item","numeric-id":5015364,"id":"Q5015364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"917e7885184f33097154d06e73041e23456aafc1","datavalue":{"value":{"amount":"+0.9023856","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":"Q1769440$F47D665F-28DA-4125-9CD8-E21CA05565D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"255b859759d1659035e2d2f270b6418149b8429d","datavalue":{"value":{"entity-type":"item","numeric-id":4525289,"id":"Q4525289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c96353251384ebd4d1682431e96372b42193706b","datavalue":{"value":{"amount":"+0.89944404","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":"Q1769440$C1E84C9B-5BC3-4778-9127-6CD8C3CA94D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a7771c4a890e5b905e0dda0cd76e96413495b68","datavalue":{"value":{"entity-type":"item","numeric-id":4938598,"id":"Q4938598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fa9cfdc3b2e6c7709e7e735764308ce6e9d7cde9","datavalue":{"value":{"amount":"+0.89812374","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":"Q1769440$5BBE84B0-C6B3-42E6-99AF-DF09D3F5979D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1769440","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1769440"}}}}}