{"entities":{"Q1945915":{"pageid":1956657,"ns":120,"title":"Item:Q1945915","lastrevid":69831873,"modified":"2026-04-13T10:38:43Z","type":"item","id":"Q1945915","labels":{"en":{"language":"en","value":"A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6154937"}},"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":"Q1945915$AF84AD5F-AECB-45E6-991A-71B095CE6DE0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4d1ee596188357a0ece4beaca62ac2e4a51147f5","datavalue":{"value":{"text":"A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1945915$B2553CA9-8B3E-47C9-95A9-C49721B40B9D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6d3ad6b53f29961aaf2f297ac85eb1129c8999a7","datavalue":{"value":"1260.68366","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945915$97637396-2EFE-446B-92A6-DD3A98A6C66F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"886664d698445e1702c39c62a8e99a722a88bdd6","datavalue":{"value":{"entity-type":"item","numeric-id":817699,"id":"Q817699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$92EA642A-5F78-4D86-9D4A-AD7939C34C7E","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":"Q1945915$00FC8463-7195-4746-BF4D-A44600F688DE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4bad757aec17a8570e2102d57df4c93baefd6019","datavalue":{"value":{"time":"+2013-04-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1945915$AA253532-2270-48B5-94CC-3DEBD3D16E50","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945915$538CD9DC-5917-4586-91AC-F4EA393702BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945915$1C88014B-D7B0-48F0-B9AE-120D0A6E87B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945915$CF1D6C91-5DE1-4DBA-9DD3-1145DCC08CB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945915$E694B663-295C-4D0D-9F11-9D62FB920400","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b1428ed06f993cb08390081917c84ec9e04a05b7","datavalue":{"value":"6154937","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945915$C6F1E092-B61C-4DF8-BACD-5ABB25C0F0FB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b876698d821b50cd7ba02ddb5424ed80f1905d8","datavalue":{"value":"lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945915$EB82DFF4-1990-4F87-9600-6685A7E68AE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"eaba8710741c3625f74acb34aa4edd5eb82e000b","datavalue":{"value":"type systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945915$E328674B-4BCF-41AC-9178-934EBF1DCEE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d61445ba5f93ffb0691f62c0dbe37940867396dd","datavalue":{"value":"formalized metatheory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1945915$79CDB995-41F9-4B66-A168-8ADEDAC4E9D3","rank":"normal"}],"P1463":[{"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":"Q1945915$F53317BD-2635-414C-AF31-5E50DF952DAD","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":"Q1945915$C7DFDDAA-5BB5-4BF0-859C-31FAE2C6B458","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":"Q1945915$4CFB2EA7-4225-4530-805F-1D8D2D6C4CA4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"040fe209bf9959da562393c0e37eb31592733af3","datavalue":{"value":{"entity-type":"item","numeric-id":18957,"id":"Q18957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$3B269029-1494-4709-84E7-CD4DB901E8DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8be5ee5254d2a781e0ec7bc0b35265c3f1813a9a","datavalue":{"value":{"entity-type":"item","numeric-id":22078,"id":"Q22078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$F85B2B2A-C489-44B0-8A56-1636DDDED014","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d40b61763c81cd80c5c82e03c39b2fdb5cbb80a2","datavalue":{"value":{"entity-type":"item","numeric-id":23989,"id":"Q23989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$259FD7A3-811A-4263-B5BF-DB17ED52EE1F","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":"Q1945915$FE5E9FB6-3139-44B5-8CE6-A1A269FE8189","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"41e93278edeee75df5495af1aa80ae47679202e4","datavalue":{"value":"https://doi.org/10.1007/s10817-011-9231-4","type":"string"},"datatype":"url"},"type":"statement","id":"Q1945915$B24E6A31-9599-4F0D-B5FE-1E9A52DCCF5C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"ebf0e3a3438c74d37ee7033d02ee1fd2e73fb142","datavalue":{"value":"W2077540255","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945915$13EBBFE8-21BF-401F-92F8-F35988D63EDC","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"79ce8544fc5a0489695eae9a558cb4d34b573281","datavalue":{"value":{"entity-type":"item","numeric-id":5477646,"id":"Q5477646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$DB8CB67D-9286-47DA-A204-04A10EF09BE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"739330a58a3c3aae77075c5fb847ca13d50160d0","datavalue":{"value":{"entity-type":"item","numeric-id":3075242,"id":"Q3075242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$0C66B005-58FD-40FB-B77F-5814E54C9131","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eeddfec2d6761bcca5b706cfa4f21836083ab429","datavalue":{"value":{"entity-type":"item","numeric-id":5712322,"id":"Q5712322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$69B8CE82-20B3-40FD-8DB0-8591643424EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c857aaf69cf79c87b310efd65fcb1c3f1d2baf0f","datavalue":{"value":{"entity-type":"item","numeric-id":3183524,"id":"Q3183524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$98EAD128-865F-42E3-96CE-C2B86B71CC68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c60f93a1843fcd9c0656971efa4327b435decb9","datavalue":{"value":{"entity-type":"item","numeric-id":4736387,"id":"Q4736387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$9F38EA0B-B6A2-4AE8-92CD-99ABC9B92DDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a550204b4fc9eb077df82e95f8c42f6d0c6fa7c3","datavalue":{"value":{"entity-type":"item","numeric-id":4764621,"id":"Q4764621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$699428E2-9EC9-4437-937F-E15FF537AE98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ab11f968a1fe231094f125d88568cff5c0be92de","datavalue":{"value":{"entity-type":"item","numeric-id":1595924,"id":"Q1595924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$A96B5EEA-B26A-489E-A1BE-07EFF4D1E873","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":"Q1945915$8CC838CD-4B9E-4405-99F2-5781D087ABEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"085f2f402bb0aaa918a693e06aa64da16c2193f2","datavalue":{"value":{"entity-type":"item","numeric-id":5687569,"id":"Q5687569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$E9BD4682-3885-4DA8-9041-BA445CD49C92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e32e6c895a421389f04c5499d388fc13d53e99f","datavalue":{"value":{"entity-type":"item","numeric-id":2778806,"id":"Q2778806"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$09FEF145-9F90-41B6-8D7C-94735AA768F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4f8f6dff394ac274489a2a8165abb84f760b4be","datavalue":{"value":{"entity-type":"item","numeric-id":5394605,"id":"Q5394605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1945915$5F165BA2-3E0E-440C-99C5-6AE6A1F96EA0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"bd05063913726e17d93047e2c6f7455d3dce6efe","datavalue":{"value":"10.1007/S10817-011-9231-4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1945915$68DFBF6F-F334-43D5-BFAC-CBE1AE25F724","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"57bffbd39784e4f9e8d33d904a9020c22324e6e2","datavalue":{"value":{"entity-type":"item","numeric-id":1945917,"id":"Q1945917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0c171b0d379152230f9f8907afe54713ebd27f7e","datavalue":{"value":{"amount":"+0.8972798585891724","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":"Q1945915$DEE040C2-11CB-499E-AE4C-5C47C26996E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c485adaf5c9d59dfd696e67e8bfc3675d896cd0a","datavalue":{"value":{"entity-type":"item","numeric-id":4992397,"id":"Q4992397"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"080db74fdaa13292b20b27d53ad8e89515bc89c4","datavalue":{"value":{"amount":"+0.7956709265708923","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":"Q1945915$EF19A593-94E6-4608-98B7-2BF73139A26E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2830883c821c59e8ea357fc4abf509bdbccc9c9e","datavalue":{"value":{"entity-type":"item","numeric-id":1945919,"id":"Q1945919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0c504094e380c390729e88a689685b1a93e7993","datavalue":{"value":{"amount":"+0.7848074436187744","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":"Q1945915$73BDE6AB-B178-4AAC-AE95-42B2D74AB95E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51b15cbe5ea309bdc48ff40b9c5acde598f0666f","datavalue":{"value":{"entity-type":"item","numeric-id":5477646,"id":"Q5477646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d7b85c37b8f4eaf1249ea3a410077c98118a35d2","datavalue":{"value":{"amount":"+0.7635305523872375","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":"Q1945915$78737D5D-3AF9-492C-9605-FF2E4B2B12BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e71f7a6493a8dbc04e7dbf14f2f531038e9beeb7","datavalue":{"value":{"entity-type":"item","numeric-id":5111317,"id":"Q5111317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6fca8705c0c8d38c1a7419def6db9fc29e39fa39","datavalue":{"value":{"amount":"+0.7468231916427612","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":"Q1945915$8103648C-5674-484E-BFDF-54D5ACB6EFA7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_solution_to_the_PoplMark_challenge_using_de_Bruijn_indices_in_Isabelle/HOL"}}}}}