{"entities":{"Q1040776":{"pageid":1042624,"ns":120,"title":"Item:Q1040776","lastrevid":69491613,"modified":"2026-04-13T07:21:38Z","type":"item","id":"Q1040776","labels":{"en":{"language":"en","value":"Data compression for proof replay"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5638511"}},"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":"Q1040776$DF36602E-E5E6-4F77-BCDC-1C7A314ADB50","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f8ed29d35b9f2ca32128182d62571dcd6c44297c","datavalue":{"value":{"text":"Data compression for proof replay","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1040776$82255815-0C52-4469-8967-5B143ED6ADAD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"832d467a417f9e97b59e5374bdf61d424ca39fa8","datavalue":{"value":"1191.68616","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1040776$CFE4A817-0ECA-43D9-A5E9-B7ACE1A0FC25","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"32584f5c482e29078ea6b6dcf1d1dfc11c06bcbd","datavalue":{"value":{"entity-type":"item","numeric-id":469351,"id":"Q469351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$CA7DD7E5-9121-4F19-AF6B-DA02E5044D2E","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$408C92AB-F5CC-4B41-9816-DB713CA89CF0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"74360fd0e383eeb4108c100504aea295aab7ad39","datavalue":{"value":{"time":"+2009-11-25T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1040776$92B6F452-4EDF-48EE-AD67-3A723E583B27","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1040776$0A59F6B0-1F0F-42FA-9DD5-A8B7E5235289","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"4556b22ead8e0c8b2ce72ea01fa74b81e9a181ad","datavalue":{"value":"5638511","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1040776$9E675279-7D34-47A3-A853-723931D6DF64","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bf4383627d45fb5f4ba25831006036a0a071053b","datavalue":{"value":"proof translation","type":"string"},"datatype":"string"},"type":"statement","id":"Q1040776$A9CFA100-26CD-4DEE-82B9-FF8DAB8391F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"543c7d0ffd0c52aa92a423848e3694a5bcbfca1e","datavalue":{"value":"SAT solvers","type":"string"},"datatype":"string"},"type":"statement","id":"Q1040776$78ABA43A-4241-42F5-B193-45B3E24DFB8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q1040776$E1E0AAAD-8CAA-45A9-9F19-D0EA35990D0F","rank":"normal"}],"P1463":[{"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":"Q1040776$3B7F7D73-A1B6-4760-8775-5E1E754F667D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fef5f048f2ff970244195639e7bcf4e64ea5e666","datavalue":{"value":{"entity-type":"item","numeric-id":16795,"id":"Q16795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$89391396-8092-47A1-B371-5C64B2E63D35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fdab07d39556d0075d882dcfd5a58c05fcf1a7e9","datavalue":{"value":{"entity-type":"item","numeric-id":21698,"id":"Q21698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$D535EB96-9F6B-4687-B196-C40FDA0BB0F5","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":"Q1040776$232B4C87-7226-4ED5-963E-BF3F22A9E401","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$7CAA0BC9-D559-4E2C-ABC4-6B97530D00A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8449db7d9aaa28101ba7b0de8e98d9c446365070","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$6807EF12-2E36-4B7D-A5AF-C57E84076000","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$139E59D9-4689-48FA-A628-7ACEF1210089","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$C29FB3F3-4A6E-40E9-AF25-BAB06AE67CEC","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":"Q1040776$93954646-1203-4667-B20E-B0C540976CD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"478f9061f14e098e3fdf3fe3667d3a7084c42e61","datavalue":{"value":{"entity-type":"item","numeric-id":18982,"id":"Q18982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$6D451F07-0013-480F-AF2F-CABFE509F175","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"660ae88d54bdff8273686883f1a29971cae0d7b8","datavalue":{"value":{"entity-type":"item","numeric-id":29185,"id":"Q29185"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$0EEA8218-8626-441E-B30D-05FAEACC51FD","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":"Q1040776$EFB6AEA3-3450-4859-888D-C24A717BDEBB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"09801b5173858500adff6a65c360a9dffc96eb0a","datavalue":{"value":"https://doi.org/10.1007/s10817-008-9109-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q1040776$6506A5D6-3148-403B-ABCA-A5DE5ABB852E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"56a50b146c23a2b577ec4f0403ae68ba5a9a863d","datavalue":{"value":"W1987719146","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1040776$7A84F978-4234-4A46-B18D-1D5ABCD4CA2D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"088d50352df9ad001d77073382165c77d3798fad","datavalue":{"value":{"entity-type":"item","numeric-id":3395034,"id":"Q3395034"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$40AB612F-5E5D-49E7-B3E0-26756D1F20E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0e242557b370e70ca22794bd752775ec0bac8856","datavalue":{"value":{"entity-type":"item","numeric-id":4804887,"id":"Q4804887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$B41F4D92-315C-4088-8BB3-B818E8DDAAE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"60159374e2e3f1fa60e69dc94c949ae9174a77c0","datavalue":{"value":{"entity-type":"item","numeric-id":5308405,"id":"Q5308405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$E1E94B8B-0313-4B24-95E6-0618F27DAB76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bffe48c7c76b90bf68970921698e19786e1600b","datavalue":{"value":{"entity-type":"item","numeric-id":2747613,"id":"Q2747613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$94EB2A12-F0A3-440D-AA99-F156E3B2D8C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62cff4d07ffcb71b5bb9f399ad2347b51931f095","datavalue":{"value":{"entity-type":"item","numeric-id":5621961,"id":"Q5621961"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$FC9164FB-9364-485D-A25A-621C8DDD0B1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a998553d04d92ec750c5db95c511cc38b8ab7659","datavalue":{"value":{"entity-type":"item","numeric-id":5315023,"id":"Q5315023"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$DC60CF70-4A64-493E-9F81-93F7219126D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22485e2e7f5d751287059d6c89f8749b6a408a20","datavalue":{"value":{"entity-type":"item","numeric-id":5325885,"id":"Q5325885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$A473E62E-520A-43D8-BF7A-DDAE85CA0640","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2b783d0052b7f250a9573410e9be2b4624ef11e","datavalue":{"value":{"entity-type":"item","numeric-id":5899057,"id":"Q5899057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$CF451ACE-5949-40F6-81A7-EFD2BAF844D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$89E624CB-2B35-4483-997B-20A3E5DE7249","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"138d808c1a0d7bbfa300ea1020e86219b9fb4bf4","datavalue":{"value":{"entity-type":"item","numeric-id":4229812,"id":"Q4229812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$A85FB59C-56D0-43D5-8289-2ECE503CE7BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05e150681c1d0241ecb463ace4c088cbd7d131cd","datavalue":{"value":{"entity-type":"item","numeric-id":3319776,"id":"Q3319776"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$4DA8A088-68B8-44F6-BFC9-6332C84244C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d935134d0fbfda57f7e887a2b20fddd73460d18e","datavalue":{"value":{"entity-type":"item","numeric-id":1764897,"id":"Q1764897"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$7558AB85-5EEC-4918-A865-9164B672C8A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e0415d643c57f0a367c51d611891732f298610f","datavalue":{"value":{"entity-type":"item","numeric-id":3396552,"id":"Q3396552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$D4CEB318-AA9A-4E96-B45A-09B5C748AFBF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$CAC23BF6-5EE6-4D9C-AD72-32D23D6CDBD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c35f4ebf8ba3be41685e193d999fe177c48a9c0","datavalue":{"value":{"entity-type":"item","numeric-id":4790648,"id":"Q4790648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$3865E91D-591D-4A50-B53D-E778CB1D60F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d13f9f67ee9c12462b09322feae7787641afc07f","datavalue":{"value":{"entity-type":"item","numeric-id":1897476,"id":"Q1897476"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$514F13E5-35C7-489C-909E-BEF36DEDB911","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"271326b3f6ba4699b8b9534f6c64338c8ddd3a50","datavalue":{"value":{"entity-type":"item","numeric-id":1006729,"id":"Q1006729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1040776$9E4E830A-DA39-4A28-9238-3E801DB6AF3E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6587c6f4dc8c04c9937dd704d9d10602a6dbfa58","datavalue":{"value":"10.1007/S10817-008-9109-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1040776$E2B82D3A-CFF8-4D80-BDBA-5AC9BD350B97","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e0f90d678a6e317f374f8cce2229fe81591e5210","datavalue":{"value":{"entity-type":"item","numeric-id":3525003,"id":"Q3525003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4158915c684bef54643f688883269a028d60ffd7","datavalue":{"value":{"amount":"+0.9103927612304688","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":"Q1040776$85D98542-193C-4B5A-A067-F736BBA82DF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c70c7c6cc56bc304adf4c26e41735c161bfeeaf9","datavalue":{"value":{"entity-type":"item","numeric-id":5178991,"id":"Q5178991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9050686e1b30f4273a47375ed9aaeefed9e28deb","datavalue":{"value":{"amount":"+0.8691719770431519","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":"Q1040776$2E306EDB-ABA6-4038-A098-A6492FCEC7F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d688e65c0de1c1e85d877c6b969c1c0ddb056c9","datavalue":{"value":{"entity-type":"item","numeric-id":479815,"id":"Q479815"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3b7cd087e8ab5d0749f2076d78412a0c5f762c2b","datavalue":{"value":{"amount":"+0.8244443535804749","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":"Q1040776$C04DB3D0-8BFF-4931-BBED-469E6A2C6074","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"114f98c35f544187bad11562a615d004d1a3f3c5","datavalue":{"value":{"entity-type":"item","numeric-id":4930598,"id":"Q4930598"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b33b8814391173c766a18e9b42e8b0f5115a1fca","datavalue":{"value":{"amount":"+0.7807439565658569","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":"Q1040776$325752ED-84CD-4860-8D4C-A5B6BC83FDEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36b1f31f0bb5689edb3b47bb744c18b5266f7c34","datavalue":{"value":{"entity-type":"item","numeric-id":2851933,"id":"Q2851933"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"969bc13220f8ab0c27e1379ce43c77302eeee4d6","datavalue":{"value":{"amount":"+0.7806189060211182","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":"Q1040776$D4673DD5-13C5-42EE-8812-9CB0D8386EC5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Data compression for proof replay","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Data_compression_for_proof_replay"}}}}}