{"entities":{"Q2879241":{"pageid":2889961,"ns":120,"title":"Item:Q2879241","lastrevid":52085327,"modified":"2026-01-20T22:02:46Z","type":"item","id":"Q2879241","labels":{"en":{"language":"en","value":"Towards a formally verified proof assistant"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6341472"}},"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":"Q2879241$C06979B1-61C4-4071-B4E3-17537DFCE6EB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"aba2ce341e6e4150a16a723295638c54e9ef66e9","datavalue":{"value":{"text":"Towards a Formally Verified Proof Assistant","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2879241$3944CF9C-F100-4163-9683-0724B619F5CA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f68d4979979efe0eeee1c8dd4d89f449dd6b1325","datavalue":{"value":"1416.68146","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879241$B30C4E37-1318-429E-85E5-F81B2A96376E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2347973f9dc33228c70627e736ba519b1c6f43cc","datavalue":{"value":"10.1007/978-3-319-08970-6_3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879241$1D0E1194-0520-4B3E-B186-E003F2076D51","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"32716be673cdc09479b44e6ef5b44e12f30c3c62","datavalue":{"value":{"entity-type":"item","numeric-id":1791137,"id":"Q1791137"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879241$05F2B0A3-9254-472F-85A0-C87FD781789F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"94e04c8c2512ac0b5c5096b1f636df023ddd07c2","datavalue":{"value":{"entity-type":"item","numeric-id":507362,"id":"Q507362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879241$85CEFF32-B6FF-4840-B0AB-AA6F8734D4DE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879241$30DA17C0-2295-4FB2-A4ED-45813B6E9273","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"565bc5987614f46e32dc98add32d630fe2eeb533","datavalue":{"value":{"time":"+2014-09-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2879241$06BEADA5-067B-481B-B14F-341DF32CCC12","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"77a9c87cd8efe0febe8894af8d4d73490cf6c078","datavalue":{"value":"http://pure-oai.bham.ac.uk/ws/files/71147559/Towards_a_Formally_Verified.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2879241$D6E31C78-C6D4-4CEE-AEFB-0FDD8D998C5C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879241$18A368B4-D3B6-434C-B8A5-65C61052C424","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"363342cc0b59d89920bf7399e52b820be14ecd23","datavalue":{"value":"6341472","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879241$CB35EDFB-AF33-42EB-BDA1-A6C365B2A301","rank":"normal"}],"P1463":[{"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":"Q2879241$089A816D-71C7-481B-BAC6-05579436EFAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"533959f24a509b955614f607e46b8aa4cec190ef","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879241$9BDE4752-9A05-4502-866F-F6BBFD4709FB","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":"Q2879241$1A73C544-C949-4B6B-B624-57C19BC2F729","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8fb5f6da2df561a79b128a652d1df41678f66c85","datavalue":{"value":{"entity-type":"item","numeric-id":22838,"id":"Q22838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879241$2F6D1FAD-6C25-4B88-B187-96263215011A","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":"Q2879241$A6753261-EA2C-4E14-9E44-1EE0ADA31937","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":"Q2879241$177E8AA0-AA7A-444C-A791-6856479914F5","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":"Q2879241$6A98547A-ED80-47E6-ACC7-BF0798A57110","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e079f4640d565f0ca1930fd327c2c7e8d634508","datavalue":{"value":{"entity-type":"item","numeric-id":21954,"id":"Q21954"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879241$19440879-D742-4011-BBA7-06A41D0FEB13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"44e192ea0614ca90dcab29c306f09db708056c50","datavalue":{"value":{"entity-type":"item","numeric-id":24736,"id":"Q24736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2879241$C02CC969-301E-4F18-9063-CEF0DAC73BE1","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":"Q2879241$B0CC4CFA-05E5-4E6E-92AE-9AD7639D0833","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"26b9aab45033b91d5af39c43d32e7c27d511bd95","datavalue":{"value":"W2166178233","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2879241$CDB18F23-85C9-4D3B-8CED-6338B7F9AF64","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6069596235a77af4a0ce188dbd6c4aa338ad0602","datavalue":{"value":{"entity-type":"item","numeric-id":3789525,"id":"Q3789525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dffe104369e61916564e04051dd4a597b67ed683","datavalue":{"value":{"amount":"+0.8032581806182861","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":"Q2879241$3F9F9721-71BC-49DA-8B54-F600B8C5E225","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bf56bcd4e828fd2db297a6d86f9a1367a5bac9ed","datavalue":{"value":{"entity-type":"item","numeric-id":5222980,"id":"Q5222980"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b3a42f208a13f253278aa0ab99a93cf4a38f3d98","datavalue":{"value":{"amount":"+0.7745513319969177","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":"Q2879241$7F44CB8F-7F56-4BDC-ACBF-C3347E1DF6DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac9c2eb9482b783c69c8f44330e38517e321c0e7","datavalue":{"value":{"entity-type":"item","numeric-id":4246942,"id":"Q4246942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"055f9a8372cbe486c91469cb17e118766a99c355","datavalue":{"value":{"amount":"+0.7678518295288086","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":"Q2879241$A31209A0-7BFA-4B18-AD4C-710542ED8329","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"71db8748d8931093cb4d67ac8e92c09b21d35995","datavalue":{"value":{"entity-type":"item","numeric-id":5327349,"id":"Q5327349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"53650ea7c1c55f432a689684abec6ebc3e910de7","datavalue":{"value":{"amount":"+0.7654275298118591","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":"Q2879241$8AFB4E28-DB44-4E2E-83A9-1BA20F8B4415","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24cdcf48e2229f3526631ece2a3e1a80cc930fcc","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dbbf464b04213ebd47c8d704144e0c21779aacf9","datavalue":{"value":{"amount":"+0.7608165740966797","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":"Q2879241$B7C3EB71-3EB9-4E43-9703-476AC59C8F2A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2879241","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2879241"}}}}}