{"entities":{"Q3453106":{"pageid":5232506,"ns":120,"title":"Item:Q3453106","lastrevid":57797043,"modified":"2026-04-02T13:59:19Z","type":"item","id":"Q3453106","labels":{"en":{"language":"en","value":"Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6512410"}},"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":"Q3453106$E1F7ACB1-F54B-4244-8F28-B1E05BB3C01E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f2964b6d47724e13714621978b79f816377c28a7","datavalue":{"value":{"text":"Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3453106$3E96A0BF-20EF-4378-9607-334464EB3DFA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3951e04524afc136614ea5ca42f862133ecb856a","datavalue":{"value":"1417.68180","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3453106$FBACE3AD-B7D2-4F62-8D3E-A3493F5AC34F","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"efff92dbae399bae2fd8024c3689cc0ed3249c6c","datavalue":{"value":"10.1007/978-3-319-20615-8_4","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3453106$0E3F9C69-E8FD-40FD-8AFD-40EC9A3BD331","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"019239a5b99c9161ce4389de57414c8f40f605b4","datavalue":{"value":{"entity-type":"item","numeric-id":340573,"id":"Q340573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$8D1D5728-4D13-49B1-8F58-6E9A6E5259AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0ee03ce229dce1ad90ba116368ba88145bf746ab","datavalue":{"value":{"entity-type":"item","numeric-id":340574,"id":"Q340574"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$9382CF90-4068-4E5C-8D76-D28FD0FD182E","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":"Q3453106$371C1BF4-D9D2-43A8-B88C-6F05E9497005","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7bc62645abb22752583f6909ba0e58feb505ce9c","datavalue":{"value":{"time":"+2015-11-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3453106$23298967-35A5-4310-BF6C-B2FCE1D190D8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ca3378a12a5574252dc4299c4318b2d28ee2537c","datavalue":{"value":"https://arxiv.org/abs/1502.08008","type":"string"},"datatype":"url"},"type":"statement","id":"Q3453106$4380E305-02B7-44A6-AC95-71133C616A4D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3453106$3646129E-BBCB-4E1D-919E-804CB5A4A598","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f97694d44af155a68434cb72eabc6a4d5dd5227","datavalue":{"value":"68P10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3453106$86E03D57-B0F6-454C-A334-14EAA4C84AD4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"fa9ea835ec2e3d744b4d800431fdd10e49b0e99a","datavalue":{"value":"6512410","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3453106$D52E7489-8B8A-4274-A175-8EAF90491B79","rank":"normal"}],"P1463":[{"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":"Q3453106$407DB4B6-CDD2-4B64-8606-FC70E7968E5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"184b17ed6ef8f72f90ef44ecb976296d445c28b6","datavalue":{"value":{"entity-type":"item","numeric-id":21947,"id":"Q21947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$99F67A97-5157-4AE9-96FC-1E155798F809","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":"Q3453106$CEED906D-26E7-492F-8B1B-479C6745CC84","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c6a6f5c9fd8a92ceb7d920a82347ea8457f0db0e","datavalue":{"value":"W1537750720","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3453106$9055B1C1-A0F6-4388-9096-ED8CB68BFEF2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$C764531B-1687-4B0A-A223-285D8817BFF9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6d8d3606448939a44632cafc0ff0031984524e16","datavalue":{"value":{"entity-type":"item","numeric-id":899586,"id":"Q899586"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$A2810155-39C0-49C5-A3E5-F9684876D14A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fda024bf3459ed600e76cd7f05ef4d9afb8ddd7a","datavalue":{"value":{"entity-type":"item","numeric-id":5389068,"id":"Q5389068"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$870E3EC8-4C5D-4A13-ADBD-7B2F1362872D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14caf64abec8078238dd92f041d3edf7f96f3183","datavalue":{"value":{"entity-type":"item","numeric-id":2852042,"id":"Q2852042"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$1488CBE4-2E1C-4205-B773-BBE98C31CF0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8cb9f5c8cfef26ace153ce30bfff08150d2fa37e","datavalue":{"value":{"entity-type":"item","numeric-id":2945629,"id":"Q2945629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$85AF4BF6-0125-47A4-B4AA-01BC697623B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a931f2e4cce499cf66640714bdf5952ff1d4cb0f","datavalue":{"value":{"entity-type":"item","numeric-id":5675725,"id":"Q5675725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$71510A84-AB26-40ED-B4F8-3C67FE5BC08F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff81489e80366438468bf6dfe10c7a159bc3ea8c","datavalue":{"value":{"entity-type":"item","numeric-id":4057549,"id":"Q4057549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$1C792AA4-B0D9-4C52-9134-341E955A3C61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"71989260ea67bc4b5ba36054c70da0e87718c8d1","datavalue":{"value":{"entity-type":"item","numeric-id":5200110,"id":"Q5200110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$46981E15-D8EC-4913-84E3-6E6474DCBDF3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"20a8d1807727f460772d228e59e0090da8175877","datavalue":{"value":{"entity-type":"item","numeric-id":3507450,"id":"Q3507450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$93A57223-E7FE-4CAA-A22A-BE851F4452AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a15f025b82e462b08b6da310a0699c520bda9047","datavalue":{"value":{"entity-type":"item","numeric-id":3543662,"id":"Q3543662"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$AF5CF8B5-1565-409F-9041-9849A059BAD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6c9a8987a7d8efa9b320ab9f4c18049ee75db52c","datavalue":{"value":{"entity-type":"item","numeric-id":4457464,"id":"Q4457464"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$FD71361E-8B1A-4298-A900-9F6C4B2425F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad271a0268ee9bc34ec9210988cce3af5092ba2a","datavalue":{"value":{"entity-type":"item","numeric-id":5327348,"id":"Q5327348"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$28123AA2-F5AB-4773-9E4B-A27DDF011EE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c31fddc109e324ad481a8f2cf8ff2e04d0f8b73","datavalue":{"value":{"entity-type":"item","numeric-id":4999428,"id":"Q4999428"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3453106$24D9397E-928B-4527-A617-7FD6B5621DFC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12a132e4daa2e15bd5dc269ad3507f16b279f28c","datavalue":{"value":{"entity-type":"item","numeric-id":1687744,"id":"Q1687744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec1a408935f80c3e22d42da3b655b6d9f60500ee","datavalue":{"value":{"amount":"+0.903803","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":"Q3453106$ACFC94A6-2F32-4B40-959E-882934D833B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ee9691043fc2fa83f9bcad490e83cd2b178847bf","datavalue":{"value":{"entity-type":"item","numeric-id":1987736,"id":"Q1987736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"54cb36c56326a912ca606c8c277194b8c9847c34","datavalue":{"value":{"amount":"+0.8847601","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":"Q3453106$5B86A83B-6CB7-43D4-908A-5E15362E00AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0363c875fa9253bc0d48c471fde653cdd563a3c9","datavalue":{"value":{"entity-type":"item","numeric-id":2945629,"id":"Q2945629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96f31ab7a8033579a48724d2b93644ef9fa9b92a","datavalue":{"value":{"amount":"+0.877537","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":"Q3453106$AAFC6A04-632C-4714-BBB2-04755F9CAB36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"deacb24347a61f6e207c9f566df13e0a7bb853d3","datavalue":{"value":{"entity-type":"item","numeric-id":6157247,"id":"Q6157247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0a9fcb1b679f24550e43585c5aa6bafd3f47635","datavalue":{"value":{"amount":"+0.8762112","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":"Q3453106$DB9DB43E-F8FE-46B3-957D-690FC02D86E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9f183308078f52a9809a1e7cc50dd85d7acf55c9","datavalue":{"value":{"entity-type":"item","numeric-id":6061878,"id":"Q6061878"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"50e846b5f11c79ba279e039779d715e923eacc6e","datavalue":{"value":{"amount":"+0.8752736","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":"Q3453106$5588E6EF-8F6D-46EE-B648-439C1DB82B6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0820b3aae10200574f5f512f87de065d11dcfbe5","datavalue":{"value":{"entity-type":"item","numeric-id":5255097,"id":"Q5255097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"91b3b5a487f06f101ec320479fa3bb5b39e17056","datavalue":{"value":{"amount":"+0.87326723","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":"Q3453106$4397111E-2A3F-4A16-A437-E8D982BC7A3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"af0a3bf9bdd0f7ea5fe705aa2b46eefc4aba3fb6","datavalue":{"value":{"entity-type":"item","numeric-id":3034850,"id":"Q3034850"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7a9c20855b80ebafffa330656b1e90a1d9a658a1","datavalue":{"value":{"amount":"+0.87318337","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":"Q3453106$3DD87D36-ABC8-4170-8F2D-C6BEF7F7B6D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dad45b5df51d864b4fc298533c8c97a833c1629f","datavalue":{"value":{"entity-type":"item","numeric-id":5495829,"id":"Q5495829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6aa3443dfe72281d1f43f500b317f13af62760b6","datavalue":{"value":{"amount":"+0.8719856","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":"Q3453106$52A7EF71-7935-44FC-9E66-3E40BA904AE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5ef6f8cd8718f1d64bdad3d35d2a8750a28f6eb9","datavalue":{"value":{"entity-type":"item","numeric-id":3759967,"id":"Q3759967"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6366113b49f96bb13f297dcd04fd227be344efe7","datavalue":{"value":{"amount":"+0.87064165","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":"Q3453106$4AA4F2D6-29E4-425A-9EF6-03C706F61A20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d205aa890fd4b97bdd81ee6a8ff8d7fef37acca1","datavalue":{"value":{"entity-type":"item","numeric-id":4647531,"id":"Q4647531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2c296fe01c5518f04ec35bf33a432ceb847138ef","datavalue":{"value":{"amount":"+0.8678487","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":"Q3453106$4AFF73A3-25BE-432E-96B8-BC6BC97274B7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3453106","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3453106"}}}}}