{"entities":{"Q1722645":{"pageid":1733386,"ns":120,"title":"Item:Q1722645","lastrevid":68903085,"modified":"2026-04-13T03:00:18Z","type":"item","id":"Q1722645","labels":{"en":{"language":"en","value":"From types to sets by local type definition in higher-order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7024458"}},"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":"Q1722645$4DE9E474-9A88-40A8-A394-A21A99E19399","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1941342efebd09f7b579c9d76092055a61a016ef","datavalue":{"value":{"text":"From types to sets by local type definition in higher-order logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1722645$75E2684F-DFF8-47A6-8DB3-99DFA6905E03","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"73b353399636bd25a6dcf06a60e28f66de4c4a78","datavalue":{"value":"1468.68295","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1722645$B2737AB1-3649-496C-87A9-BA964790706D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb18cf0542c9d5785b9c3d13ac135abc8a7efb68","datavalue":{"value":{"entity-type":"item","numeric-id":1687532,"id":"Q1687532"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$401F9FE2-1A0F-4A48-9873-C9CD1A556EC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2ef4ea61388b67726824db4b9b444c6863305920","datavalue":{"value":{"entity-type":"item","numeric-id":817686,"id":"Q817686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$2FD7D24F-CFF6-49B2-8A65-48EBC704D494","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$19DEF0EA-3B11-47F6-9614-D93E95E96B40","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0e07e584aaf32d9a9691066d4a126742d1828198","datavalue":{"value":{"time":"+2019-02-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1722645$E032A013-C415-4FD4-BABA-7857E0D2DCF7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1722645$70CD1117-72F4-486D-9F4F-1DA7E0FF3624","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0224f16d89ad92e2886ee3a8c3376cf23064ca60","datavalue":{"value":"7024458","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1722645$21DAC924-DF94-4FEA-9E1C-CC87E14C9B76","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5343ecd15a8e87cb138c7d9e4c8f0d52a5afdb65","datavalue":{"value":"HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q1722645$58E4C287-F924-4F28-92DC-4A8E0D291657","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q1722645$21D4C670-9252-4B16-898F-12F3BF238D77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bea11f51d52c4b463c5616c2f53f32b10036a0b9","datavalue":{"value":"local typedef","type":"string"},"datatype":"string"},"type":"statement","id":"Q1722645$4959AD6D-9F40-4431-A6AD-A7A075BE85E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9849395d50a5a8f69e8acfb50bf7a9a7aaa85055","datavalue":{"value":"type definition","type":"string"},"datatype":"string"},"type":"statement","id":"Q1722645$ED0BC2F1-7692-4E58-875C-5A4F37B8E23F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"06059c11269d258bbccac60c4e9a619d8f9e5b9a","datavalue":{"value":"relativization","type":"string"},"datatype":"string"},"type":"statement","id":"Q1722645$822EC8A1-162D-4278-B7A8-0B98EAAE4AE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ff33796796e98480bd831c12f8abdaa6ed1568ba","datavalue":{"value":"type classes","type":"string"},"datatype":"string"},"type":"statement","id":"Q1722645$E5A0EDCD-31D2-4A51-9C37-AC231EE97FE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ec44778685040bd9bd5cbc0ffb12f352e97e79b2","datavalue":{"value":"overloading","type":"string"},"datatype":"string"},"type":"statement","id":"Q1722645$8AFD39E7-55BA-4017-9353-08C49D280C97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q1722645$7A044276-207E-44F3-A06A-F3DC31A820AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"52c2513afc8941299b07e63a5555cd1e7cb85f4a","datavalue":{"value":"consistency","type":"string"},"datatype":"string"},"type":"statement","id":"Q1722645$60714C73-6314-4D73-A4DD-A4C3B7553F6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"548d1f07e827d6a0aac33d5f8508c1249beecb5f","datavalue":{"value":"transfer","type":"string"},"datatype":"string"},"type":"statement","id":"Q1722645$58B51535-D653-4B4C-AECA-A539ED68D3F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9cdc2f4292137e17dee1d0c0dcb6e29151d5bb03","datavalue":{"value":"type-based theorems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1722645$17F6E29D-0D40-414B-A644-986E148485B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42ae96a8bf437fbe7bebf327060d3518d5c986c1","datavalue":{"value":"set-based theorems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1722645$1E91C3B8-B1BB-4F2D-A604-BA94976A45AB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$EF9B3956-F5C0-4B45-AE88-8E974FC85E72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$F86CABC8-DD02-472A-8BD2-4140DE314B5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2ad21f150c621099eebc7c2e673cd9cf43b81a4e","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$51A5B1D9-59C4-4D70-819D-B0CECA3C8A24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$33130A39-35B5-4790-89F3-8BD749F3532C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e262f47aa23786f0d5ca3c491b5060c53e80792f","datavalue":{"value":{"entity-type":"item","numeric-id":18274,"id":"Q18274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$1E9073DC-500A-4546-B058-C7FEDE89B007","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$5B2350A4-4936-46ED-81C0-94D01E144683","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$525A6E0F-3581-4696-87F7-D8E0CADB2A81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$B84DA622-578A-4AAB-81F0-DCBA0CDD6CB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ad35e1f036cc1a37637a9bb57b386a55e86e9fd2","datavalue":{"value":{"entity-type":"item","numeric-id":18673,"id":"Q18673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$A27E736C-A03D-4E3E-BDAB-AAABFF60AB94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$2F147E89-9068-4759-BE4E-B6A0A315691A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$71833758-E781-416B-9FF9-96EBB8C45ADB","rank":"normal"},{"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":"Q1722645$5F7B22B9-8DF8-42CE-9975-CCFA4B6DA7A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"468fad61234030d4d4bd64e4991e6e30fb2af1d0","datavalue":{"value":{"entity-type":"item","numeric-id":29451,"id":"Q29451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$99772C39-0026-482D-8D4F-CA6C0636F5C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1f427ab6dbbd025b0c0b66dd047be36c332e9e80","datavalue":{"value":{"entity-type":"item","numeric-id":32822,"id":"Q32822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$DFF96F70-9C36-4734-B61B-8D741A4BE5B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e9fd7dbff509abaee9c64d21afb19f85055bad01","datavalue":{"value":{"entity-type":"item","numeric-id":32823,"id":"Q32823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$8B89A819-BEC9-47E0-A3F4-7D00357E55A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2c491ca24cb85bbd6f9c4698ce87ed511fac835c","datavalue":{"value":{"entity-type":"item","numeric-id":40310,"id":"Q40310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$7A78AE04-BB67-468D-B067-CA3B50678F07","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":"Q1722645$C24FC4B8-181C-4D93-8383-CD27B27C03FB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"29a1141a521dc87704978d9c53dace5c591c25d2","datavalue":{"value":"https://doi.org/10.1007/s10817-018-9464-6","type":"string"},"datatype":"url"},"type":"statement","id":"Q1722645$0067CBBD-93E1-4D39-908B-CAB4C60C1E7D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"bf434b6015a29764a4632aa56c70fa99ae01e062","datavalue":{"value":"W2806477068","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1722645$D2FEB83E-5838-4288-82D1-B0FFA3DEDB99","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a5cab1513e2457c77b799379237c33e5461fd89","datavalue":{"value":{"entity-type":"item","numeric-id":2829259,"id":"Q2829259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$780B9D71-A3EC-481E-A75B-584932B88083","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1903be4a36187a0a0e197e708bc72f62f93b28bd","datavalue":{"value":{"entity-type":"item","numeric-id":3183520,"id":"Q3183520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$3B2E2BB1-9C15-4205-9D1D-E410F98E0BBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$DCF702E1-CE44-42A7-949F-B8AB9B022BB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fbe1455cc5dda38390654a9baeba09eedb655d2e","datavalue":{"value":{"entity-type":"item","numeric-id":5200015,"id":"Q5200015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$38F369A3-7408-4A34-8AEB-B859B2B788C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$24EBBECA-DA48-432C-B64D-0055F5EE0DF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5552c73af9ffa4d08773105bfa675feb6642eb2e","datavalue":{"value":{"entity-type":"item","numeric-id":3453119,"id":"Q3453119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$14364C54-AC40-468D-A8CD-45387FD050DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc149579e2c0f9cf6c6f1a082b600b053a6569c3","datavalue":{"value":{"entity-type":"item","numeric-id":3183533,"id":"Q3183533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$2643D5E6-2D11-465B-A7CB-08B9041273AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af5454750f5d297118e2d43ae886b47301283891","datavalue":{"value":{"entity-type":"item","numeric-id":928666,"id":"Q928666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$B46DC395-FA07-4E8C-8CEA-033122287305","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"863dff1ec39c42296687f1c2c5d2b7c1e2903d5d","datavalue":{"value":{"entity-type":"item","numeric-id":2945627,"id":"Q2945627"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$EAB25BEC-43E8-4A4A-BBD7-B81B0875326C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34dd873a66486e9e38fc156a4b8aa6ba19960bb7","datavalue":{"value":{"entity-type":"item","numeric-id":3088003,"id":"Q3088003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$18252635-3B98-407F-B293-F1429037543B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34776a41f104a7bb21fbef16d60bb8b4116b09d5","datavalue":{"value":{"entity-type":"item","numeric-id":682381,"id":"Q682381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$111EDD36-F973-46C3-96EE-F174CBE9D8BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$CF4C1C9B-53DF-4ED1-A18C-356E33858695","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2622e8892c0aaf09e727281c5cb9109808708d59","datavalue":{"value":{"entity-type":"item","numeric-id":2988665,"id":"Q2988665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$2DA8B233-7193-4C50-9EE5-BDC7EC298B00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14533123e0b9e73c06f9737a070ee002c25f5f1b","datavalue":{"value":{"entity-type":"item","numeric-id":3612442,"id":"Q3612442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$253F2926-207F-43AB-81E7-9B785CB9CBA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67c913a72527b57ea467866b24b8cfd23fe78226","datavalue":{"value":{"entity-type":"item","numeric-id":5747659,"id":"Q5747659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$4126233C-0027-48E5-AE3C-19D1C72AA394","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9d8e0ff8a7d0c4fc199c213531e4694eacc1d9f6","datavalue":{"value":{"entity-type":"item","numeric-id":2938044,"id":"Q2938044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$7702A6C6-9B1B-46A8-A3DD-610A3F856BCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2fa401b3f58fb4c2bc9ea2f71ee0d728db11587","datavalue":{"value":{"entity-type":"item","numeric-id":2986838,"id":"Q2986838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$AAF9998C-8C63-437B-AC5D-4A29CBBEFFE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0ef84619234e2e46e8c4513d6d1ef3cba6f5b65","datavalue":{"value":{"entity-type":"item","numeric-id":1945903,"id":"Q1945903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$58EE13F9-DEFA-442C-AD4C-F9959CA16510","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a5e182d22cd63374751049cb1ad374f0b5175f7","datavalue":{"value":{"entity-type":"item","numeric-id":5477650,"id":"Q5477650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$A40F7744-8225-4360-AE7A-D72CA5DE0931","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4f9b358bef184a43a1b759d46554e4d4bb5b4e0","datavalue":{"value":{"entity-type":"item","numeric-id":1984794,"id":"Q1984794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$1453BB87-6E9F-4FC6-AF57-BE91E94C0B8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4738798d9702e646d9743f53f948745583da971","datavalue":{"value":{"entity-type":"item","numeric-id":2352487,"id":"Q2352487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1722645$C301EF8B-E790-437E-BF40-E65F29A3E3C1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"67ff112ed9f56f772b6f1abe3626f2a86e8ec720","datavalue":{"value":"10.1007/S10817-018-9464-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1722645$B6D9F054-BE46-4FCE-BCAC-57134E874A07","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"57561d8103315a979045f0c2201c893bcb717a32","datavalue":{"value":{"entity-type":"item","numeric-id":2829259,"id":"Q2829259"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f6d2372b891a21f721cf04c78dc61d72cc3191ee","datavalue":{"value":{"amount":"+0.9947508573532104","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":"Q1722645$CB032C28-8EC9-477E-906F-3ABE17623BF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5a89dd6970994c099e3030bbed6db81931530f4a","datavalue":{"value":{"entity-type":"item","numeric-id":5747659,"id":"Q5747659"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"725f836a7e864fdce8591162b4f2195fd95f6258","datavalue":{"value":{"amount":"+0.7338233590126038","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":"Q1722645$A1C61EEC-19D4-445C-A290-48770ACC5033","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f007afffaa9d82c697dfde08e38474d46ab399f3","datavalue":{"value":{"entity-type":"item","numeric-id":1739913,"id":"Q1739913"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d6867baf6c47d218a8f07fd3c4d08a4e389c4010","datavalue":{"value":{"amount":"+0.7324916124343872","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":"Q1722645$F1FA1241-34E0-4BAC-B69E-A39CE61BA035","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"880184504bd47d4aab173f44873bb04dbe6f5cfc","datavalue":{"value":{"entity-type":"item","numeric-id":1309243,"id":"Q1309243"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d59d29b9cfcd5c7584a4a336eefaca791018ad1","datavalue":{"value":{"amount":"+0.731674313545227","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":"Q1722645$9E419860-7539-456A-83B9-46B76F3B3F18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f486f15bb96c9d702825bb4445acddcc63515c3a","datavalue":{"value":{"entity-type":"item","numeric-id":287358,"id":"Q287358"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"27a1d10e7a6a37ca5157f55ddf06d55c19ff09b1","datavalue":{"value":{"amount":"+0.7314767837524414","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":"Q1722645$1A55CBC8-DD9A-4B6D-9E0F-F6CEE9D808A2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"From types to sets by local type definition in higher-order logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/From_types_to_sets_by_local_type_definition_in_higher-order_logic"}}}}}