{"entities":{"Q5958776":{"pageid":8135578,"ns":120,"title":"Item:Q5958776","lastrevid":97727585,"modified":"2026-06-05T15:18:22Z","type":"item","id":"Q5958776","labels":{"en":{"language":"en","value":"An induction principle for pure type systems"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1715821"}},"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":"Q5958776$BA6311C6-F3DD-4F0C-A85A-5EBE9EF8AB6C","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f121ca27434d95cd906e3dc3f51ac9a001ef1f3b","datavalue":{"value":{"text":"An induction principle for pure type systems","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5958776$D8504025-71ED-459C-81DE-5636134BA995","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f8650c2b77ceb526c453f6ae84f61d9872029be3","datavalue":{"value":"0992.68188","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958776$3EB8D6EB-0C2A-4D67-8315-0A27339BA63F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5610c83a81cb763085a8fd02bad3e738a8372cf5","datavalue":{"value":"10.1016/S0304-3975(00)00373-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958776$B9DCB6D4-0B64-4438-950A-59AA89AD8AB1","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"df85df02f9f01c867f5b97dc99ba15582bedbdd2","datavalue":{"value":{"entity-type":"item","numeric-id":236461,"id":"Q236461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$6FBC0945-2635-4B80-9CAB-D68925248D9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3446e7dbb7240ad90687dceaaac250247886da36","datavalue":{"value":{"entity-type":"item","numeric-id":236462,"id":"Q236462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$7392A05D-4F37-496F-BFF4-B4E8413BE1E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d2875aee90fd87423322d2627d32e4150c27948c","datavalue":{"value":{"entity-type":"item","numeric-id":1125573,"id":"Q1125573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$5E48A55D-E85E-45EA-95DE-F326D5BEE655","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$FCDC1F19-69CF-4082-AB0B-5519C255BB7E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"de0bbc1f0efc0eda52d8a37720ec217ae66c93cd","datavalue":{"value":{"time":"+2002-03-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5958776$F151E79D-D7A7-4554-950A-5922821E30DB","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958776$C62F3674-7CAF-4A8F-9D2E-30E54798C308","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2569b63ac5590803a5739031e69467097f3f7edb","datavalue":{"value":"1715821","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958776$B44DAC4F-0D06-4E78-B2F8-23D44B86727D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bb82a6bb049eca827530aea8e4ff9bb2ba33b1cd","datavalue":{"value":"induction principle","type":"string"},"datatype":"string"},"type":"statement","id":"Q5958776$71451633-F1DB-41DA-A614-D3B88D840D74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"803071656ef49caf5ffffeffb35be0afbcb7ae7c","datavalue":{"value":"pure type systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q5958776$305D0911-E380-45BF-97C5-77C588DE799C","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"55d1796d289926821ff098bc5ea53615142e836d","datavalue":{"value":{"entity-type":"item","numeric-id":21664,"id":"Q21664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$58FE60CB-68A7-4CA4-866B-837E1AC629A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$D0391C05-1DC5-4476-A821-A67CC0B20399","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":"Q5958776$6FBA8738-2BA5-468B-A62F-073B7814C953","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"787e8787fc0800d23d78fddfd9bf35254e758553","datavalue":{"value":{"entity-type":"item","numeric-id":801050,"id":"Q801050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$0A5E1D06-AC14-4B2C-8898-71D771A9E696","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d63e1d2c1097bf56f38b3464089e43c611b33ec4","datavalue":{"value":{"entity-type":"item","numeric-id":4939697,"id":"Q4939697"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$4605E734-73CD-4604-97B1-F6F4077986E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19bc50e2f4d2cceaac2ab96d0b4ab028848b7d4b","datavalue":{"value":{"entity-type":"item","numeric-id":4023900,"id":"Q4023900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$299EDC8C-8193-4D0E-ACA9-5E66806789EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba7ac73b86cab3a9c097ad46c024c2b40f94da13","datavalue":{"value":{"entity-type":"item","numeric-id":4263801,"id":"Q4263801"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$8C9FCD30-C5D2-4559-B0BD-31A235465112","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"182015ccb61e82934df94bd3aaf2171eddd62920","datavalue":{"value":{"entity-type":"item","numeric-id":4948007,"id":"Q4948007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$56FC11C3-6739-47D7-A996-CA09CCFC8E4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cff418d95b7bb6ba972b96c705625126cc05f715","datavalue":{"value":{"entity-type":"item","numeric-id":1125574,"id":"Q1125574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$C898E2C4-BC9E-4260-A445-7973D4A60F2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7bba503ca0b5969142e3056aa23d82e5afa7c0bb","datavalue":{"value":{"entity-type":"item","numeric-id":5958619,"id":"Q5958619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$4EE5473D-10CF-4CA9-AD6D-9D41CE3D918C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cbed5b14a086787bebc35634de251ea7dadb5fb9","datavalue":{"value":{"entity-type":"item","numeric-id":4762953,"id":"Q4762953"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$2601893E-07C3-4C90-B248-77DEA5787822","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22b0a30febc9fafd0aaf6f91ea1821651d55077e","datavalue":{"value":{"entity-type":"item","numeric-id":4764266,"id":"Q4764266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$AE19B131-F262-4B49-950C-A73BC87BAE25","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":"Q5958776$5AE2AE6B-F343-43B9-8362-70EA7363C7F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad80344fc1eac9869a64dbac310f2d1dda233df0","datavalue":{"value":{"entity-type":"item","numeric-id":4939698,"id":"Q4939698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$606D3059-2AEB-4D70-83AB-872D383FBB54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85724e3e2abe5b8664c9700d62e3fe6eb196e39c","datavalue":{"value":{"entity-type":"item","numeric-id":3024906,"id":"Q3024906"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$18ADC07A-552D-41EE-9BD3-FB63D241FDEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$5DDE8598-4F97-4B57-AD46-D202F67BC828","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2eca81f9fdd20e2c49645c4efb07abd9a2d842cc","datavalue":{"value":{"entity-type":"item","numeric-id":1165004,"id":"Q1165004"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$17C4D884-A872-40C3-918D-14D51CF93404","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"37bc8dae1994f1675072ec162c7c6788e05d8d41","datavalue":{"value":{"entity-type":"item","numeric-id":4296744,"id":"Q4296744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$998E8D20-786E-4196-81F9-4A1650D1C5C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50d92dc238774fd1c651af2baa062a030c6eec7a","datavalue":{"value":{"entity-type":"item","numeric-id":3680263,"id":"Q3680263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$3BEEF971-A927-4B86-85BF-8208EB2B7B58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03cbc69cab2b7d5069acc953a5626227ed8c07a0","datavalue":{"value":{"entity-type":"item","numeric-id":1340050,"id":"Q1340050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$07CA6D01-6DB9-4969-8A7D-56EF6A7D232F","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":"Q5958776$504E5F00-859A-4AAA-BE1A-50A95DF110C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f2e9bc1c1ff023291254b138990be434f6b297b","datavalue":{"value":{"entity-type":"item","numeric-id":4236762,"id":"Q4236762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$FFF1D0A3-EFD1-4325-92A2-8E24ECEAA2CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"91a707f7565046237d79754215ce6024facdf2b7","datavalue":{"value":{"entity-type":"item","numeric-id":4068054,"id":"Q4068054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$8A4BB42B-E140-42A1-869B-37EF14CF19B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e195a519ca02237c87426a6e69de956fcb956d38","datavalue":{"value":{"entity-type":"item","numeric-id":1891251,"id":"Q1891251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958776$56BC93C4-40EA-44D9-B2C9-CA59EDE0C7E2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ebaebae0b6bdb49f7f3fecb065781f60b2c143ad","datavalue":{"value":"https://doi.org/10.1016/s0304-3975(00)00373-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q5958776$A8A1A151-F57C-4120-B5AB-33C357FB35F0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"30ef4ce6fd10d188aedb0824935d2bbcc51ecd42","datavalue":{"value":"W1982157045","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958776$548E9528-17C9-4134-8A58-E25121DF6F21","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af0883e379d10d28de7592d639b18e0f3696c856","datavalue":{"value":{"entity-type":"item","numeric-id":4236762,"id":"Q4236762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"66e4d4a192ab826dca8725d3076fdbe90866032c","datavalue":{"value":{"amount":"+0.7714824676513672","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":"Q5958776$FCF5EF67-63C8-4891-9660-3313295A828D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6e9fc4b8d5bbb2ed22afcb9da4a5b0f607645834","datavalue":{"value":{"entity-type":"item","numeric-id":2844696,"id":"Q2844696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c898e097cdebb0da8dd717122d3eb71a52eeda43","datavalue":{"value":{"amount":"+0.7705332040786743","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":"Q5958776$035E2144-C291-46C6-A87A-A2BB8C74EF90","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac7f4474a0f3dbac871198b2b90792a22a031854","datavalue":{"value":{"entity-type":"item","numeric-id":1125574,"id":"Q1125574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97bd21e7e2a6eaf57e141d79dc8550964421eff4","datavalue":{"value":{"amount":"+0.7618679404258728","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":"Q5958776$DB1CB576-E249-4BC0-8420-D045E297E7A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a1f536dd4897b55633cd8707e2d26ca95080188d","datavalue":{"value":{"entity-type":"item","numeric-id":5371956,"id":"Q5371956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97bd21e7e2a6eaf57e141d79dc8550964421eff4","datavalue":{"value":{"amount":"+0.7618679404258728","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":"Q5958776$5605C060-D99C-4A3C-8839-E60206B30922","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9da3f06971b0a5c5e1545510a0e13f468a663910","datavalue":{"value":{"entity-type":"item","numeric-id":4501161,"id":"Q4501161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2bcc54385e8c98894bf548008046d2cb40ca7358","datavalue":{"value":{"amount":"+0.7604966759681702","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":"Q5958776$5E1E8EEC-39EA-4CA2-9254-3666E094FB8D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An induction principle for pure type systems","badges":[]}}}}}