{"entities":{"Q1362142":{"pageid":1372881,"ns":120,"title":"Item:Q1362142","lastrevid":67240938,"modified":"2026-04-12T16:18:26Z","type":"item","id":"Q1362142","labels":{"en":{"language":"en","value":"A higher-order unification algorithm for inductive types and dependent types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1042561"}},"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":"Q1362142$40D11D29-5B7D-4ED3-B529-A8C7CFD44B2F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8fa221b6778cb89b0b004f65506b9c2e559aad5e","datavalue":{"value":{"text":"A higher-order unification algorithm for inductive types and dependent types","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1362142$0C1436DB-059C-43AD-ACE3-15C6362A1796","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ff1fb14a039907b9f2b866b7385e45b4374dc5e1","datavalue":{"value":"0878.68069","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1362142$161233E2-6AC3-4B09-982C-58647F4A9923","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f0970e79428eeb552fcc957e9616e7d40ba89741","datavalue":{"value":"10.1007/BF02948973","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1362142$B00ABF1A-E28E-4E19-85BB-92443DA16F5B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8e027238e0b1145d7b7ae6350689c8dc72769ce9","datavalue":{"value":{"entity-type":"item","numeric-id":362269,"id":"Q362269"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362142$3A438EBD-4884-4F8C-9F12-FE9B0F089B98","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4c3c57bd2a24956e0520aebbb172d094d92623f1","datavalue":{"value":{"entity-type":"item","numeric-id":182337,"id":"Q182337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362142$4C1AF0E8-34AE-4F60-9EA6-8D827D9149A3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1742a10e6409607193ef806e8f573a0e208ec887","datavalue":{"value":{"time":"+1997-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":"Q1362142$7F05432B-E329-44B0-A6C6-F73B56C634FC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"1de3565cfd3393000dd87ca545f95ff84d4c1446","datavalue":{"value":"68W10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1362142$2BC5FCBC-0B46-4B3D-9572-CA27EB603DE8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c2c0bc9852b549d77da12637e2003e1911e34699","datavalue":{"value":"1042561","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1362142$9E3734C1-DC77-4776-8253-242ACC6B3A19","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b876698d821b50cd7ba02ddb5424ed80f1905d8","datavalue":{"value":"lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1362142$985B3ABD-4266-4267-85F1-9DD716AC1CAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q1362142$4DB92737-1054-44B4-AAB6-C5C2BE93A373","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"95c030d9a0c4c312aef7a319ac8b5849913b2040","datavalue":{"value":"logical framework","type":"string"},"datatype":"string"},"type":"statement","id":"Q1362142$2F03D29C-B6A7-4C9B-83CC-AC509188C24C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e1202fa4aaeffc809043c1d94983ad89396bca2","datavalue":{"value":"inductive types","type":"string"},"datatype":"string"},"type":"statement","id":"Q1362142$475982FD-AB45-41D5-AE8C-82CF2E669C56","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":"Q1362142$C197A1C4-DFA3-44A2-8CC7-53B3D0135966","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4fecc7ce8fe53bf0ab0f560a96ff760721b70f9b","datavalue":{"value":{"entity-type":"item","numeric-id":1230505,"id":"Q1230505"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362142$E157C378-6643-4EBE-8237-5F7CB3997DE4","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":"Q1362142$B1C19A22-5B4B-492E-9E31-C0244C066609","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18ce06304bf3709cc235c3276b4f500aec1ac468","datavalue":{"value":{"entity-type":"item","numeric-id":1239309,"id":"Q1239309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1362142$DDA2C4AA-D1A0-499C-B838-138139C9FB99","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ec2f0bb38b56f759cbb69a7dc3cbce032e16f8c6","datavalue":{"value":{"entity-type":"item","numeric-id":5055716,"id":"Q5055716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9ea7b63b920bfff2d85f4d2e6e90881e62bc4f0d","datavalue":{"value":{"amount":"+0.8199328184127808","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":"Q1362142$9D7342A8-B334-4B29-A5D6-2850EF74D72C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"387cce94216297b66f69d2aa4feef49d02d8cfd3","datavalue":{"value":{"entity-type":"item","numeric-id":4681362,"id":"Q4681362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dfaf08cc844ea525da21d86ff1151da4883ff60c","datavalue":{"value":{"amount":"+0.7857190370559692","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":"Q1362142$D7CA118C-1D20-4D49-A08A-BD4D4F44C6E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2842a69ce505d76f527982e81a57a0ca07074c7d","datavalue":{"value":{"entity-type":"item","numeric-id":5286030,"id":"Q5286030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"029eafea743f89efe75bd712a964f4c4059ff68a","datavalue":{"value":{"amount":"+0.7736331224441528","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":"Q1362142$EE102818-8B59-4B36-B5DE-2A53FA4C8384","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6fce87e1e4581922017d2f5560c916cadcfe98fc","datavalue":{"value":{"entity-type":"item","numeric-id":5055872,"id":"Q5055872"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"02e0541721cf85f33910448d9a0d7ca9cf9ad705","datavalue":{"value":{"amount":"+0.7630168795585632","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":"Q1362142$FD1CF422-46AA-42B4-A349-94CCAFBCF82B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A higher-order unification algorithm for inductive types and dependent types","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_higher-order_unification_algorithm_for_inductive_types_and_dependent_types"}}}}}