{"entities":{"Q3637272":{"pageid":5667178,"ns":120,"title":"Item:Q3637272","lastrevid":50705171,"modified":"2026-01-14T21:05:20Z","type":"item","id":"Q3637272","labels":{"en":{"language":"en","value":"ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5576972"}},"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":"Q3637272$7175F37C-03F2-4976-AECC-EC9CA26D9784","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fd4cb2344a8f126bafe921f56b25598c0f5009e8","datavalue":{"value":{"text":"ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3637272$09CE1B12-D7AC-43AD-8B3B-F90978C77CB2","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a49b8dfa158b570f1d801e8fe2d9a682ccf94691","datavalue":{"value":"1247.68325","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3637272$46137A50-0C75-4414-8E30-42F6030F9F86","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9f6d802e1adc6be0379bc0c07871e19575ab2624","datavalue":{"value":"10.1007/978-3-642-02614-0_13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3637272$7B132AF1-CDAA-4C7A-991E-324A535FFFEC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"76b38168777167ff49199bd7f47bfebb8e51e498","datavalue":{"value":{"entity-type":"item","numeric-id":438547,"id":"Q438547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637272$C1FF05CF-48F3-449E-871A-8066CDCBFA22","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3c5989ab1028cea7e9ee7fb42127fc02a808a197","datavalue":{"value":{"entity-type":"item","numeric-id":438548,"id":"Q438548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637272$3243D4EE-CC11-47CA-BBCE-A5FF0962C4F8","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":"Q3637272$1FB6D05B-69AA-4078-83A6-92FEFAD1311D","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":"Q3637272$21BF86EB-0299-48DC-B9C9-3824AE9CDCFD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6e6dc41c09de35f18f848a8f3dd9ef2baecfc096","datavalue":{"value":{"time":"+2009-07-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3637272$68EE157D-505E-410C-A89A-B66950267F5C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3637272$BD6A5E94-C84F-4DCD-8754-2263F8282013","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a2c3a267d39cc0a240359433e7798b450888646","datavalue":{"value":"55-04","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3637272$4267B2E3-7362-48D9-9240-619E71112666","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"aeec0fe5b883ee01d46044fea691f53b23b620e2","datavalue":{"value":"5576972","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3637272$DA6A2A6C-2502-4EA8-A6A5-44EA259F04BE","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":"Q3637272$04F9DBF6-0602-4565-9650-EB87DE59C2DD","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":"Q3637272$BE8E5CD7-5761-4494-AB1C-F533B062D2F0","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":"Q3637272$4A901FEE-BCA3-475D-9C1D-E4733A5C739B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a8f057223c758d6b8295ecbdef4842faac2ccb72","datavalue":{"value":{"entity-type":"item","numeric-id":19253,"id":"Q19253"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637272$6C695D14-A074-4CD9-A30F-5A084713B68C","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":"Q3637272$498A3F86-7A12-4A07-865A-880D82A18426","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7d7af9ee539ad02677011f34e9cd0b4f500429ce","datavalue":{"value":"https://doi.org/10.1007/978-3-642-02614-0_13","type":"string"},"datatype":"url"},"type":"statement","id":"Q3637272$4BB6ECCA-FE13-4A2E-A4DC-16BDB11B9B56","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a4832d900a1e2c61e802cd00e43ed9d17728587b","datavalue":{"value":"W1605757265","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3637272$2759C037-716D-4554-AB26-DA52CA3E5D89","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc11a2379fcf282936837f86ebebfde76a6c82da","datavalue":{"value":{"entity-type":"item","numeric-id":5428255,"id":"Q5428255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637272$295B1274-5E2B-489E-B3C4-5FF9465F0C7F","rank":"normal"},{"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":"Q3637272$98A67BF2-EF27-4630-898C-A2B44E44D4DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9534ea3b2f1d8917f4c6886c66faef8268544b2e","datavalue":{"value":{"entity-type":"item","numeric-id":5394420,"id":"Q5394420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637272$2A8525CF-7E50-4137-A717-87297D5070A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9767b4f993764f1a6ae8e85667cc0e126d88ec7b","datavalue":{"value":{"entity-type":"item","numeric-id":5428258,"id":"Q5428258"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637272$41BD76FC-17CE-4B1F-A940-89033FC2D7FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2d300252a7f5ef02e60bd45537fcdd52068f537","datavalue":{"value":{"entity-type":"item","numeric-id":5505507,"id":"Q5505507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637272$A4019E38-6C4A-443C-93DF-B24A7D405538","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75f2c295c4449018ea4283ff294ef038c1799aae","datavalue":{"value":{"entity-type":"item","numeric-id":5441547,"id":"Q5441547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637272$4B3B9F0E-903F-4260-ABB6-86E3ED811FE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2626254db8aada704f30d688d571249d1e6a9fab","datavalue":{"value":{"entity-type":"item","numeric-id":5505524,"id":"Q5505524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637272$BD980FE6-E891-4B66-B858-959A99E596BF","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":"Q3637272$10514E75-BD45-4788-AF72-CFC7E1EA4CE0","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":"Q3637272$E2CE4387-B1CB-4F82-B49B-A86CDD53C046","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":"Q3637272$EB3983DA-C795-4E4C-B4D6-0B1F76D03527","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b7536e92384e11ec3ce8637ede805331f9e036d8","datavalue":{"value":{"entity-type":"item","numeric-id":3997095,"id":"Q3997095"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3637272$7C3A01CC-CE7A-4387-83AB-69CAAFFEEFE4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2e8c3f2564b881ea1b7e4341684c21fb5e3646fc","datavalue":{"value":{"entity-type":"item","numeric-id":3003483,"id":"Q3003483"},"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":"Q3637272$2CC6B6BD-E8BE-4717-AAEC-30FD90082639","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":"857763f203817af6c8670efbd422896d3bb95f1e","datavalue":{"value":{"amount":"+0.8083839416503906","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":"Q3637272$F488A2CE-8959-489A-B3F5-A44EC25A3EB7","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":"d9847b646c29f606d33042a83817f88ee388cd3d","datavalue":{"value":{"amount":"+0.8065761923789978","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":"Q3637272$B1CFD83F-E023-4772-AB77-538B65424BE3","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":"afaa1febd1f4532ab5d27ef6a1c69c383cf4714b","datavalue":{"value":{"amount":"+0.7803279161453247","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":"Q3637272$33178853-09AB-47D7-A976-BFED38498E8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1af0d66185bd63945888907fa239a13516a8f374","datavalue":{"value":{"entity-type":"item","numeric-id":2430025,"id":"Q2430025"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dd25829f21ada79dfdfb0ba0f380452b0137e68f","datavalue":{"value":{"amount":"+0.7733016610145569","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":"Q3637272$70C5CF32-D8DD-4DAE-8CAD-4A6C2CCC8DCD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3637272","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3637272"}}}}}