{"entities":{"Q2908568":{"pageid":2919293,"ns":120,"title":"Item:Q2908568","lastrevid":58055319,"modified":"2026-04-03T15:19:36Z","type":"item","id":"Q2908568","labels":{"en":{"language":"en","value":"Dependently Typed Programming Based on Automated Theorem Proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6076973"}},"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":"Q2908568$0C3A627D-C2F3-4188-8E8B-6CDEBAABCEF4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a66de68793bb78e48a270cac074eb1cc94f753ff","datavalue":{"value":{"text":"Dependently Typed Programming Based on Automated Theorem Proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2908568$93907589-1748-40C9-BD8F-44114A754E48","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"36bddf84a5a9cf17b3cb09334de6cd3c8bc58470","datavalue":{"value":"1358.68056","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2908568$9409A6F6-2289-44BA-9EBF-2E8BCAE4C8BA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5026ee307b9e86bdfffc10333651a0021fda6645","datavalue":{"value":"10.1007/978-3-642-31113-0_12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2908568$E1850D2A-A8B3-49BF-B51E-F1FEEF2B969D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"661058c43babba56430a6ee50eb96105dced91de","datavalue":{"value":{"entity-type":"item","numeric-id":406432,"id":"Q406432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908568$91579E92-1848-4CCC-B2DD-6336BBBC41C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6f0d16d56334eda577a220b2d6e48a64c295fa2c","datavalue":{"value":{"entity-type":"item","numeric-id":1617822,"id":"Q1617822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908568$10A10397-FA3A-4BE1-83C3-A4B11008F991","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"eb27aad50a775f188aa99887f496d209cf025869","datavalue":{"value":{"entity-type":"item","numeric-id":299200,"id":"Q299200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908568$C1CE7AC7-08AF-4166-A4CB-6AED34649797","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908568$4C2CA5E3-11E0-4211-92FC-2146BCCE470D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"fd0374f9cee657eee67ac4dd9d79d96d1538c53a","datavalue":{"value":{"time":"+2012-09-05T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2908568$9244492D-5A51-4F8D-8B58-F06CE00B78B5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0b7d8ec9f7e45a9e208387325d502804f7b6aa84","datavalue":{"value":"https://arxiv.org/abs/1112.3833","type":"string"},"datatype":"url"},"type":"statement","id":"Q2908568$07045488-E7F3-4FB6-960A-527D5AD00458","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2908568$95A080A2-BE2E-46FB-B194-F658D0C51E45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2908568$F2B103F0-4983-4896-80C1-05B265925AFF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a5a017e26de13f0e8dca5b360af00674ee0e34ea","datavalue":{"value":"6076973","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2908568$2E17C5C4-6EB5-4C7C-A79E-5BD1F190ADE6","rank":"normal"}],"P1463":[{"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":"Q2908568$1700FC2B-FEDA-483B-94CE-7B7D226CBDB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9aeef25d5839625565921d83cf1c652bf6f2fbf6","datavalue":{"value":{"entity-type":"item","numeric-id":17052,"id":"Q17052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908568$55E533EA-1585-4C3A-88DA-8642FD3D916D","rank":"normal"},{"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":"Q2908568$BCB08636-FF9C-4BC6-8AF8-E46FD62A99FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c766f98bf98fe7cf06a05963cc75ed84be39ac3","datavalue":{"value":{"entity-type":"item","numeric-id":31394,"id":"Q31394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908568$E34A8C7E-08DA-452D-995D-089745472B43","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":"Q2908568$033AFFC4-32C7-400E-8173-02000A75A822","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908568$52B87123-C637-44AD-A201-6FD32D611830","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"067e00213990a6f2431e78667be3f10443c92f4f","datavalue":{"value":{"entity-type":"item","numeric-id":16052,"id":"Q16052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908568$7A9326B9-B676-4D28-BA41-D6964E8F3EB7","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":"Q2908568$2CC4F7C0-D9A2-4EBA-BE9E-B332EAE7ED00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e74e65aea50b572ed5cc320d9d0d7a2d70ec494a","datavalue":{"value":{"entity-type":"item","numeric-id":21666,"id":"Q21666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908568$7ABD41F9-FBC7-4BA8-A711-FBE20CBBEDED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"00a8f0acf50baeb7d842d52472eed7c54b64fe33","datavalue":{"value":{"entity-type":"item","numeric-id":21667,"id":"Q21667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908568$A4664069-1994-472A-960B-007AEB476C27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"43f7c4ee5068daf82f8bffbb0f7510a5f16faf63","datavalue":{"value":{"entity-type":"item","numeric-id":16615,"id":"Q16615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2908568$4578AF01-7282-48C3-A366-7927BE97F187","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":"Q2908568$27477CDC-A485-4A53-9736-6A62FB763FB7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"429c754c938e36a869f878765fefed5b2a1cfc9e","datavalue":{"value":"W1861293286","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2908568$3826210B-292C-4EC0-BD91-1E98971E6C75","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fdc61f049f8d0b30109ea2633d86e084029eda8b","datavalue":{"value":{"entity-type":"item","numeric-id":2751370,"id":"Q2751370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6c6368c5625a77a81aba0308bc603053c2119599","datavalue":{"value":{"amount":"+0.92544734","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":"Q2908568$0C2BD995-1213-4941-9064-5B3980AED0D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2fd0887d9303d6a5b7f60dd0479ea33753b3bb35","datavalue":{"value":{"entity-type":"item","numeric-id":5408400,"id":"Q5408400"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"130752d731ccf1518dbbdda78e9166740e093ffa","datavalue":{"value":{"amount":"+0.9210835","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":"Q2908568$4A512B04-BBE2-4F73-BE46-C51624CD4D7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"83a9a1cb2c762ff8bfb3334266634affdfe71512","datavalue":{"value":{"entity-type":"item","numeric-id":5193019,"id":"Q5193019"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a68df590d8ca2fbd8bf8db1545c600d3e42b240a","datavalue":{"value":{"amount":"+0.9111316","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":"Q2908568$B96174EB-9A2D-43CB-A005-1A10A8311A5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"357860675d9d6383009814e1650bf925597a610f","datavalue":{"value":{"entity-type":"item","numeric-id":4819651,"id":"Q4819651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b51016b0fdaf82884416842d49f36a4677800b9","datavalue":{"value":{"amount":"+0.90104514","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":"Q2908568$C3443F2B-02C5-4E38-B8D0-75641340FF81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"187b62627e66cd358a52ec0d56e639fc73eeacc8","datavalue":{"value":{"entity-type":"item","numeric-id":4025341,"id":"Q4025341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dc05f3fbceeb92bd874f75836df1735bed7818de","datavalue":{"value":{"amount":"+0.8967945","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":"Q2908568$56D44C2E-4E5F-4966-87A5-9C7C3C3421A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"83ead96eb0dad59b33308a29c10c00c5949abf9c","datavalue":{"value":{"entity-type":"item","numeric-id":2723415,"id":"Q2723415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"110c4970545a8693cf8c77ba704c854bd181ba93","datavalue":{"value":{"amount":"+0.88962066","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":"Q2908568$BF06DA1C-33C8-4C92-9A02-3EDA78D7B9E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a08562885acdf630cb480dbe6bb784304badc973","datavalue":{"value":{"entity-type":"item","numeric-id":1868508,"id":"Q1868508"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"110c4970545a8693cf8c77ba704c854bd181ba93","datavalue":{"value":{"amount":"+0.88962066","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":"Q2908568$86215AF6-6B32-434D-B776-F82F3BF440CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"832adab52a6be03c508c7df724145ae73e85a03e","datavalue":{"value":{"entity-type":"item","numeric-id":4524768,"id":"Q4524768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3e21c89e23f2e13dede95a00da32fd2853b9f1cb","datavalue":{"value":{"amount":"+0.88949835","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":"Q2908568$A844B72F-273F-4CBA-9328-2BEB0F40C657","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d3e088cbec1988368e76bc1772341a1c24eb4604","datavalue":{"value":{"entity-type":"item","numeric-id":2753682,"id":"Q2753682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a4e552f8aff0c4eca19713a50a3dfc9b9d3f44b5","datavalue":{"value":{"amount":"+0.8868113","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":"Q2908568$96ECBDBC-1412-40D7-BB2B-22DBE14ADB65","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2908568","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2908568"}}}}}