{"entities":{"Q3003483":{"pageid":3014207,"ns":120,"title":"Item:Q3003483","lastrevid":51255005,"modified":"2026-01-17T11:36:08Z","type":"item","id":"Q3003483","labels":{"en":{"language":"en","value":"Proving with ACL2 the correctness of simplicial sets in the Kenzo system"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5900384"}},"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":"Q3003483$A4D5ECAD-6ECF-4076-991E-89FF715E3C8E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6b039c9d00d3494b0cd4eabb9fecb5e7175b8332","datavalue":{"value":{"text":"Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3003483$8633AA96-8E44-413A-9E3B-E377D59EB3B4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"f5b0d06b940aa28fcc88aa5caf009fe2881f5a63","datavalue":{"value":"1326.68261","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003483$855FD2AD-6F39-4A8A-8B51-6DC87521D66F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1ddbe8b54fec18c89c0d220641e4fcb17eaf068f","datavalue":{"value":"10.1007/978-3-642-20551-4_3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003483$F975EC70-24A7-49FF-A80F-71AD315BDDBE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bc9df023cae9b25ea4b60776547a8efc95e2e421","datavalue":{"value":{"entity-type":"item","numeric-id":280197,"id":"Q280197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003483$F43A5A42-B068-42F6-8143-711BBC0AFEA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f094f136b80323bed41c924380e7f7932ce72a9b","datavalue":{"value":{"entity-type":"item","numeric-id":1413644,"id":"Q1413644"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003483$27278E9D-113A-49E6-BB3D-418C6C5B1AA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2742bc74281e45d5f573cb9dc1b7a4db7f023f65","datavalue":{"value":{"entity-type":"item","numeric-id":1565829,"id":"Q1565829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003483$79008279-1EC9-441F-96FD-A65B19981124","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"adb24e8791ad8d605f348f62fef07af498b65f70","datavalue":{"value":{"entity-type":"item","numeric-id":2848891,"id":"Q2848891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003483$98DF69F0-B9AF-4743-84BB-D38BC43A98BC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3175b0056ab29270a0640c1aae102bae06142a3a","datavalue":{"value":{"time":"+2011-05-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3003483$64C597F6-2BB4-44B7-BC2C-F10BD0FCD68F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003483$3A7BFE00-60BB-450C-B619-F4639AD5703D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1722e8eaf8d0b6e989e3d4620a85df21f8eb2337","datavalue":{"value":"55U10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003483$E0B793BB-8067-48C9-A97D-543A65B033C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003483$464FC3E0-B745-4A47-BC8F-7533D517DBE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003483$60D097C7-7807-4ABF-8DBA-C754085A5288","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7fff719dbab664d1485d2a02deedea30bf098938","datavalue":{"value":"5900384","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003483$9DC13FBB-F124-4B89-A849-BE1E1EF92C1E","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":"Q3003483$1B4A21D8-4696-4A91-B1AB-77CE91E6EF89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d9db21642bb525242f0a9c25c65251a61579aa2e","datavalue":{"value":{"entity-type":"item","numeric-id":21159,"id":"Q21159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003483$EF319ED6-56E5-4CB3-A88B-EBDEE2812117","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"efacd6a40fcceaf80f5658fa8699430affa80235","datavalue":{"value":{"entity-type":"item","numeric-id":17016,"id":"Q17016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003483$4E9E3DE4-0802-4B19-8AA5-637B677DC942","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":"Q3003483$58DB27B5-A988-440F-A9AA-F2FF0F7AB10A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"3c3bb14e7131e4039ae3e36266126b452ee38021","datavalue":{"value":"https://doi.org/10.1007/978-3-642-20551-4_3","type":"string"},"datatype":"url"},"type":"statement","id":"Q3003483$A7DF9077-5DCA-49D4-99D5-5CF0FD02FADD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"97d6c7200d75d32ee23f20867856091d91a40b9d","datavalue":{"value":"W1847528365","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3003483$8A2C9662-4670-43EF-AE1A-045203717F75","rank":"normal"}],"P223":[{"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":"Q3003483$2D521973-B214-4C66-AE1D-0A2C1EA8102C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"485a5c2d43bcf04725f445cf5f3f084491db724f","datavalue":{"value":{"entity-type":"item","numeric-id":968307,"id":"Q968307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003483$C1728C15-F60D-4D7C-BE62-108E8A85A074","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e55c9a5a5d7a017c2e20d9a304ec72cb817783b0","datavalue":{"value":{"entity-type":"item","numeric-id":3637304,"id":"Q3637304"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003483$856E66F1-A4AE-452C-87CD-CB49A1EDBBCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8a11b587785b43a7aba09896edc5ae68fbca055","datavalue":{"value":{"entity-type":"item","numeric-id":1413645,"id":"Q1413645"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003483$4008C674-45C7-44D3-8C06-2E2A60A5AE4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4a638c1b8d85988bdd45de66bd17f2104917aa1","datavalue":{"value":{"entity-type":"item","numeric-id":3637272,"id":"Q3637272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003483$EFFFA6A4-3589-4F59-B300-BCBAB0CCA2AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50a8569e46b6ebf9bdf790ad48b6a4dab614e1a9","datavalue":{"value":{"entity-type":"item","numeric-id":5550390,"id":"Q5550390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003483$BA71486C-0EBA-46D2-8B5D-FA0C1A46C2ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b00764f2554b817f32c18778472c08f20203f31","datavalue":{"value":{"entity-type":"item","numeric-id":1328492,"id":"Q1328492"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3003483$539DAFBE-EBE4-4E55-8F91-746BB576FB82","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8fc5c52ecc7532ffeb62f04e5cf1ab1b35279224","datavalue":{"value":{"entity-type":"item","numeric-id":3637272,"id":"Q3637272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ad2a45672d412c4ab4ab7151cb44ce409d71204","datavalue":{"value":{"amount":"+0.9155230522155762","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":"Q3003483$D717A4A7-03FD-4D6F-AFAD-60437E1FD038","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":"2a44cab784f7cc4b8e2b21c9a39538c28161e55e","datavalue":{"value":{"amount":"+0.8316904902458191","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":"Q3003483$56161267-55F5-4001-91CF-C7397D3293E8","rank":"normal"},{"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":"9181f5cbb6f0da065906e8cdcfde159138b90a43","datavalue":{"value":{"amount":"+0.7900850176811218","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":"Q3003483$4DA0F1E8-9297-4A3F-B987-4736294BD89F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eb8fdaae5d041429cea115ab94c35deb80e0aa37","datavalue":{"value":{"entity-type":"item","numeric-id":5172125,"id":"Q5172125"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2dd8b4caa48eb5c6fa23cae61350e2c9bfb1e482","datavalue":{"value":{"amount":"+0.7895047068595886","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":"Q3003483$30E7947F-430A-4B35-913B-77A1B3EDBC16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"913f5efd90d90f85d5491384cc864170d414521d","datavalue":{"value":{"entity-type":"item","numeric-id":5200131,"id":"Q5200131"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3c614019ebf57f1f7a86fc9081d5a04b62d4e086","datavalue":{"value":{"amount":"+0.7824039459228516","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":"Q3003483$480575E0-E540-4302-AE23-E9D13DB8D9D4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3003483","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3003483"}}}}}