{"entities":{"Q4382485":{"pageid":6412084,"ns":120,"title":"Item:Q4382485","lastrevid":41076301,"modified":"2025-04-18T03:44:23Z","type":"item","id":"Q4382485","labels":{"en":{"language":"en","value":"Proofs of strong normalisation for second order classical natural deduction"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1130665"}},"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":"Q4382485$269B2044-282A-498D-A0A0-347A5C01E428","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f09c771c23ea90aba9b9e543d2f961acf9799c6d","datavalue":{"value":{"text":"Proofs of strong normalisation for second order classical natural deduction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4382485$45938848-1E1F-4D52-AADD-70654C9E093B","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9b369d973991c14c77fa96d5e48cdb620b9af561","datavalue":{"value":"0941.03063","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4382485$7476452D-F9C1-48FF-8989-941026E7A193","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0884b51b48a0f60572c5e188f799946d3f793f6d","datavalue":{"value":"10.2307/2275652","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4382485$73562A5D-3EEC-4B47-AA59-98F8A71D6E9F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9bb422b0a71c7373d6ef3f0283ecc33ac78f3208","datavalue":{"value":{"entity-type":"item","numeric-id":1083859,"id":"Q1083859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4382485$4D399BE7-ABFA-42FD-B0CF-E2B49EBE90A7","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6218d42f0175ef35f91c4900eb5db86484a9463d","datavalue":{"value":{"entity-type":"item","numeric-id":2710590,"id":"Q2710590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4382485$16CF89D1-B929-48DE-B55B-C81CF06FC05A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0a70e1c598c77a2c68107d0b0c1806859c43bcd6","datavalue":{"value":{"time":"+1998-04-29T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4382485$C037E4B0-C707-4B5E-B733-49D2EA884202","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4382485$D52F3060-F14C-48C4-8308-1658923466A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4382485$578320A4-2D7B-4B8C-8776-162CCD78BD8B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2d2f50ce6fae1b5edb75bb465e2e0d23b5bab09c","datavalue":{"value":"1130665","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4382485$E782BCA6-6FFA-4E03-9244-A2EBCC7CF9E7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8d8bb84bd86abec9f57c8cf048201e810211b8ba","datavalue":{"value":"strong normalisation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4382485$ECDD8F68-7949-465E-80FA-C4A4EB09528B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5e2443d46b9781eaf654c2170e9579ddc41424d6","datavalue":{"value":"second-order classical natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q4382485$9E7D581C-B88A-486C-A3FD-EA2CCA96D146","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6d35f71b2feeef33ab46de91b2f82b629e259d0f","datavalue":{"value":"reducibility candidates","type":"string"},"datatype":"string"},"type":"statement","id":"Q4382485$56EA44DA-0663-441E-B8B2-9633A0DB52B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"78b2cd6f429f89630fd41abd7cd3011871aef3d1","datavalue":{"value":"intuitionistic natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q4382485$29A774C2-C48C-4B02-87A3-9A05A0F355C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"772f5faa34caedf2451888fb0d9881373d87f9e5","datavalue":{"value":"Kolmogorov translation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4382485$AFA3ED7A-17D3-40C8-A7B0-6A951B194E24","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":"Q4382485$12B55519-0D11-4E8D-A1DA-A82E858C86A0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"22592b0d25604c7a6c72dcbcdd12cfc07489bc8d","datavalue":{"value":"https://doi.org/10.2307/2275652","type":"string"},"datatype":"url"},"type":"statement","id":"Q4382485$FFB2411B-F828-4815-9775-C8346E6B1482","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"4dc810515b5c59ae9f3d28d259bd6bfd9d0204b7","datavalue":{"value":"W2132936218","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4382485$85630F9E-AD25-473C-8870-4E070BF71EBC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1e84ff42267477e949575e937efae295817dbcbf","datavalue":{"value":{"entity-type":"item","numeric-id":4372906,"id":"Q4372906"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4382485$231EDFDC-0205-46FF-AFEC-721FCD719BAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e27be5516997b567899ad0b0d96cb56d275522c","datavalue":{"value":{"entity-type":"item","numeric-id":1225449,"id":"Q1225449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4382485$93FAC4CA-32F0-4172-8E37-2841D0F63E3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"16de9a4f8e129e311d9ce09ae9e120dd4a226b8b","datavalue":{"value":{"entity-type":"item","numeric-id":3997016,"id":"Q3997016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4382485$352B1C62-5866-4981-A52E-DEDE785D56EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4382485$ABB725A5-4317-4F5D-B5B2-987603451274","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d66518f09c99314187d256b3e54c7fdc6eb07ce","datavalue":{"value":{"entity-type":"item","numeric-id":4006233,"id":"Q4006233"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4382485$20BC2AB6-18D6-4F2A-9AC8-47314276D145","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0004f8fddecc0a33725b971c1c77c93c033b938f","datavalue":{"value":{"entity-type":"item","numeric-id":4692942,"id":"Q4692942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4382485$AB7F79A6-9566-4FF9-B237-6010AB102DF0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53bcfabc22212d3db2a4fa41c3566844e5ecdda6","datavalue":{"value":{"entity-type":"item","numeric-id":3668859,"id":"Q3668859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4382485$07569B7C-756F-4242-8D84-30781F23ABEA","rank":"normal"}],"P1643":[{"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":"601fff0943c9fa388b48713d7eba4208e1075d85","datavalue":{"value":{"amount":"+0.94973296","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":"Q4382485$9E4EA0D7-B8BB-4CBC-A1A1-B9E6E6B6D71C","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":"ada7b010750397f30bef3059d9ef09313b95e969","datavalue":{"value":{"amount":"+0.94369406","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":"Q4382485$BA21FDAF-04B0-4184-B5AA-CB76F7096349","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7ab8f2efce65f1bb0e13fc4caa073a89436edf6c","datavalue":{"value":{"entity-type":"item","numeric-id":1769440,"id":"Q1769440"},"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":"Q4382485$57113E65-67EB-48F0-BB31-96B2E24012BC","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":"17fbf590970f84b731f1cd2c538288ed83bece5b","datavalue":{"value":{"amount":"+0.9285209","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":"Q4382485$F72EAB2D-5730-4CD4-BEB8-B88FBE495E61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fd0408c0d7dfc173c00f52df72da5ff9eeb3b8e2","datavalue":{"value":{"entity-type":"item","numeric-id":3981450,"id":"Q3981450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1f6c84c48b61e41d8672fb1772ff9f2711faeb46","datavalue":{"value":{"amount":"+0.92300546","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":"Q4382485$4E8DE025-B4E7-4711-AFE9-2AFE0A3C838F","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":"4bddc5f7982390d6deb3d1a211166285db16d140","datavalue":{"value":{"amount":"+0.9180703","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":"Q4382485$5076A7C2-5CD2-4BEE-9A5D-57C1ADB8A601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"05d1cb7f50ff15314687d4e9e68913f9827f827e","datavalue":{"value":{"entity-type":"item","numeric-id":2482841,"id":"Q2482841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"43571bf4dff9df2355dcbe223468645e98eccedb","datavalue":{"value":{"amount":"+0.91735125","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":"Q4382485$30E5A8E9-6F44-4957-9EF3-9D021DA78959","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1ad9f76053e2eec268eabfc3f030a1df49e12bb0","datavalue":{"value":{"entity-type":"item","numeric-id":265002,"id":"Q265002"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9601b98cb4e77080e683a467e5d65b088f7354a3","datavalue":{"value":{"amount":"+0.9156736","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":"Q4382485$A56C2D72-C34B-405B-8DA7-64B8A8E3F9CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ac325c0bd52d9b011f3757fae07bfdf508a5a94","datavalue":{"value":{"entity-type":"item","numeric-id":2778822,"id":"Q2778822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"772a152d80b293c9483f56896ee39bd73d7cb74e","datavalue":{"value":{"amount":"+0.9139531","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":"Q4382485$E8ADF8EE-76EC-4EA7-9AC0-E895168DE45F","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":"543b759e34de25fc7b173f5791f5dad479a4f752","datavalue":{"value":{"amount":"+0.9079355","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":"Q4382485$4A393FBC-3C50-4ACA-B708-36C670FC10AD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4382485","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4382485"}}}}}