{"entities":{"Q3062059":{"pageid":3072775,"ns":120,"title":"Item:Q3062059","lastrevid":51154760,"modified":"2026-01-16T23:26:08Z","type":"item","id":"Q3062059","labels":{"en":{"language":"en","value":"Formalizing simplicial topology in Isabelle/HOL and Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5831403"}},"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":"Q3062059$75A70AF9-E88A-44A4-852E-2A42F8D3C7DB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ec9ea882d4d8423ee853296829a53ff81fc0a3d9","datavalue":{"value":"1209.68502","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3062059$02C524EC-3169-404D-AC8B-488A917D0DD8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d8eb82bb8898c38a2ce640cb1506b4d91fb17bc7","datavalue":{"value":{"entity-type":"item","numeric-id":3062058,"id":"Q3062058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3062059$ED59210A-E204-429E-A043-B4F83853B763","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"4c2f65d791882d0fe991234b07620a5de3e8f853","datavalue":{"value":{"entity-type":"item","numeric-id":631754,"id":"Q631754"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3062059$67CC715E-76C9-4E60-928D-E34B96372D6F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4c2d3c72cfe71d37d0ec412655d40e813991301a","datavalue":{"value":{"time":"+2011-01-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3062059$A894DB09-6DCE-4A44-92C2-F865F72CD63C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3062059$8A215C39-DC8E-423A-A0A1-A7C9A5C267A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1722e8eaf8d0b6e989e3d4620a85df21f8eb2337","datavalue":{"value":"55U10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3062059$AE27F1A0-C2B6-4A0D-87A4-657AB97B473F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ebd2cd049379550c8de89a7f0585fe630abd4b7b","datavalue":{"value":"5831403","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3062059$55271C9C-AEE5-4E36-BA25-8336E1CB3209","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6590184c37d6b984eca99f9b5d9366d6780f743","datavalue":{"value":"theorem prover ACL2","type":"string"},"datatype":"string"},"type":"statement","id":"Q3062059$004B4F05-5B90-408B-8BF8-66A5DEDBD578","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3062059$D4AC4788-C063-49E4-81C1-3BD1D10BDDAD","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":"Q3062059$CA13D374-3800-4038-9922-20DD8267C72F","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":"Q3062059$5108A1B2-04BF-4915-9535-E821C4A4C21B","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":"Q3062059$FE558F6B-01B2-4C1D-9815-C59D6E0F0D58","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":"Q3062059$A75B7164-4B29-41B8-A941-F3D993E3D14E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d1dfd4266e963b75fd65bd359de1b4cbf73c719","datavalue":{"value":{"entity-type":"item","numeric-id":3062057,"id":"Q3062057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c2d6b05b3b095f60397ca47e51da9faf8785850","datavalue":{"value":{"amount":"+0.8530034422874451","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":"Q3062059$417E4C2B-7ABF-431B-91F1-FE8F364858C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8a057d646087c1a86968ef69c61f7db8a49a696f","datavalue":{"value":{"entity-type":"item","numeric-id":3088007,"id":"Q3088007"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cce0903fa64bd23b545e0bfb520185196928dbd0","datavalue":{"value":{"amount":"+0.8006789684295654","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":"Q3062059$7F536704-F127-4FDC-964C-30E928810CBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c8dd60d8ffa429e9574b03af9bed59b69a12dd50","datavalue":{"value":{"entity-type":"item","numeric-id":5200106,"id":"Q5200106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"376438eca31a0d8fdc9c62c366c5556ad3930eff","datavalue":{"value":{"amount":"+0.7945175766944885","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":"Q3062059$6F4439B5-7785-4879-A11E-FC19C6D31192","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"42e85011cc4f8f812313279990efa8b25b1cecf3","datavalue":{"value":{"entity-type":"item","numeric-id":1926582,"id":"Q1926582"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b8b275a490b88d6476474d33832b4c1248b46521","datavalue":{"value":{"amount":"+0.7724840044975281","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":"Q3062059$E762D133-573E-4627-A6BA-F00818B7A06A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a1f3331b51ca53f8eaab24ecae369057c407154","datavalue":{"value":{"entity-type":"item","numeric-id":372699,"id":"Q372699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b49cfd0980416edcccbac6f95cd964bbb25f01e4","datavalue":{"value":{"amount":"+0.7630242109298706","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":"Q3062059$CFD95808-D9EF-41C1-986F-6DBED93E6A11","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3062059","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3062059"}}}}}