{"entities":{"Q865656":{"pageid":867504,"ns":120,"title":"Item:Q865656","lastrevid":65005917,"modified":"2026-04-11T23:41:08Z","type":"item","id":"Q865656","labels":{"en":{"language":"en","value":"Supporting the formal verification of mathematical texts"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5128352"}},"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":"Q865656$DFDDF356-7880-4773-BCC6-47BB66EA948E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f5111ec6aeeeb1920abc13e4d500ee6e8a3ace3f","datavalue":{"value":{"text":"Supporting the formal verification of mathematical texts","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q865656$4AE4C0DC-DF46-4FED-BD47-BED5D9D7D060","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ecf76b5ba8403fb924d5a5e9c318765ac07b6234","datavalue":{"value":"1107.68104","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q865656$6F73A933-0E98-46A3-8C9D-1A57D4D9A683","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1b99b045c7913575d08cdf22253e4eeb45cfbfdf","datavalue":{"value":{"entity-type":"item","numeric-id":865655,"id":"Q865655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$DA389F75-BD9B-414E-9FA8-003FF0726823","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"fd9c858b64e538228c66f00c768fd1506ee71010","datavalue":{"value":{"entity-type":"item","numeric-id":124852,"id":"Q124852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$886000CC-BAD9-4258-9B36-7B9BBC32F0D4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b6a3b01ed43848088ad19bc3cf2f29651a0e98f7","datavalue":{"value":{"time":"+2007-02-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":"Q865656$974923E6-0F09-4BDC-9E21-FAA1A336C031","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q865656$A7DDEE04-931C-413F-BC33-728AAB8BACE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q865656$4492A481-D475-4FEF-BD35-4F96404DF223","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"aa8c728541be1682c9533f1b93f4690b8b38bbc1","datavalue":{"value":"5128352","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q865656$CFB455D2-35A1-4114-9343-6B9648559047","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"81576cbb4d1cb8d53ace8c08ef94120219f7cdb2","datavalue":{"value":"modelling mathematical language and reasoning","type":"string"},"datatype":"string"},"type":"statement","id":"Q865656$4C9F876F-1DA5-41F9-A543-74A8C25C81FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9a4151719b9c35c5f4b68922237e211e496a98fe","datavalue":{"value":"discourse processing","type":"string"},"datatype":"string"},"type":"statement","id":"Q865656$BC8BF86C-EB82-45C6-8B1F-652AD9002DE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2e925d21691ae524cbfb2c7846fe00986c22417c","datavalue":{"value":"proof planning","type":"string"},"datatype":"string"},"type":"statement","id":"Q865656$1E68EEC5-1CC8-460F-85CA-D931AE98E495","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":"Q865656$685D7346-6777-4960-875A-78DBDA3139B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab1ccc8faeab7e6c417af9846c477f0e521ebe1b","datavalue":{"value":{"entity-type":"item","numeric-id":14592,"id":"Q14592"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$F6CF5374-9F70-401D-B754-88027EDB912E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9aeef25d5839625565921d83cf1c652bf6f2fbf6","datavalue":{"value":{"entity-type":"item","numeric-id":17052,"id":"Q17052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$135073D3-83D2-4DF8-8390-68AA4103DBB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$28F30E40-5DCD-41A7-8122-DE2D73AE496C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f10e7acb77aa2a053602f0044c4781346f0cbb55","datavalue":{"value":{"entity-type":"item","numeric-id":31444,"id":"Q31444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$4B6651C3-D75E-4F4D-A701-3693C044524F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b222922e2b373ab7fb2b7a049f9de07c755ee255","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$CD24A961-ED62-41C8-9FD6-C7A43F9B7DB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ec97af8dbde1b3f52d57c157b7fa0c737d48882a","datavalue":{"value":{"entity-type":"item","numeric-id":31439,"id":"Q31439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$C9D39CC5-8008-403E-B864-2D18FEE6C7A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1e7b4d238eeafa5b21b1ef85a0d6b8900bfdc422","datavalue":{"value":{"entity-type":"item","numeric-id":15442,"id":"Q15442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$A18AD1B2-9D5F-475C-9EE9-E9994FBDA797","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":"Q865656$DBD22AF4-5512-4635-87D4-F22C403D5493","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bcaf3b20cd7fd897f2f47a708bad9d4f554cb6fa","datavalue":{"value":{"entity-type":"item","numeric-id":14553,"id":"Q14553"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$1ABCF5A7-37D0-483C-AE18-B958ACBF6ED7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$38338463-D9A8-45B4-99F9-5E68F6720887","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a49c6eab3f20625da110b159712fcc58d765d3c6","datavalue":{"value":{"entity-type":"item","numeric-id":31454,"id":"Q31454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$C1AB2004-19BF-49E9-A50D-BDA4E303DD88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"594dfaf0018a3856fda12bed34127aa02bdbfc31","datavalue":{"value":{"entity-type":"item","numeric-id":31447,"id":"Q31447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$6743FA44-B0DD-4E6A-9191-4BB2F1EFA828","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19c3232540dc15c9350e8393498317de25361cb2","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$FC5544B7-EF09-4A13-8DEA-8D75E84E2E44","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":"Q865656$F1084B60-411B-4092-A4A5-7C195A413405","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"22de60673fd152a0d60db99ef07edb90d7f76e3f","datavalue":{"value":"https://doi.org/10.1016/j.jal.2005.10.010","type":"string"},"datatype":"url"},"type":"statement","id":"Q865656$D0CE39CF-6767-405D-98C6-F911626EBC51","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9e881729fc4c11c998bea540fd43bf67a0ce435c","datavalue":{"value":"W2086329789","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q865656$D88B693E-D757-4802-BA52-66B6087AE632","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"1196f5e17dff99bc1a9d16ec3c58ef966832597d","datavalue":{"value":{"entity-type":"item","numeric-id":2729065,"id":"Q2729065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$25523AF9-67AE-429E-BF93-87C8D95E96D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0fec4ebbd0f7e0440d7bf45181d3d2e0b25e7779","datavalue":{"value":{"entity-type":"item","numeric-id":2847390,"id":"Q2847390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$2835B8FD-5AEA-409C-8230-867880D06939","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"87c7d01517d5946f7b490e527f2cfb73be29e8c1","datavalue":{"value":{"entity-type":"item","numeric-id":4664918,"id":"Q4664918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$E702DDBC-880B-481E-9009-3D63056EEF34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a8e3517581f053bd397311cfe8d27c9b34620e8a","datavalue":{"value":{"entity-type":"item","numeric-id":5234706,"id":"Q5234706"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$8D362D24-E07E-471A-89A2-9360476E991A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22a238ed6c54d87ec163b1a7cb181d6ef07206ba","datavalue":{"value":{"entity-type":"item","numeric-id":3804239,"id":"Q3804239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$B3E06696-2158-4FDC-9E86-64C9F8F1CBAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c91a62fc73d328b39f05fc8fae0c1a2a5426db9a","datavalue":{"value":{"entity-type":"item","numeric-id":685548,"id":"Q685548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$09E4111D-6B62-4778-9F58-05E67BF76264","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"366ee1071310872ce51f69ac724d1b1cff46fae5","datavalue":{"value":{"entity-type":"item","numeric-id":5610115,"id":"Q5610115"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$D5C00180-AB65-49FB-9C64-D7B1CB35ED92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"01588d6f9f501ed9209e9cb37c2d5d53381cd6aa","datavalue":{"value":{"entity-type":"item","numeric-id":3478365,"id":"Q3478365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$21BD8267-581F-4708-A4F2-944FBCD2FE63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae4a7fa8abdfcc0e9370ee91a7f38c7187429c7f","datavalue":{"value":{"entity-type":"item","numeric-id":2767009,"id":"Q2767009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$05F965F9-4290-4BB2-A36A-BCE8759FC1E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7db98659fd0d8d989353341e0c12c4246dfe6ee1","datavalue":{"value":{"entity-type":"item","numeric-id":1915134,"id":"Q1915134"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$3D2DC60E-F5D2-484E-8636-C60F03371FDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d1efaf3011598847d3954f457cae839aa26e35d","datavalue":{"value":{"entity-type":"item","numeric-id":1876109,"id":"Q1876109"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$4C74D5BD-9107-4E8A-A890-341BA4AF0168","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c234e4870a3d583d166b6a38151685a4aab4d5c3","datavalue":{"value":{"entity-type":"item","numeric-id":5519616,"id":"Q5519616"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$AC990FEB-0BF1-4D6B-934E-41E5D234F41B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03cbc69cab2b7d5069acc953a5626227ed8c07a0","datavalue":{"value":{"entity-type":"item","numeric-id":1340050,"id":"Q1340050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$DD6D6006-EF40-4EC1-AFE2-E99D81D254A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$81E91E60-B09D-4817-A64D-7E5FD6FD091E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"700e138d664cdf333d4a787c78bb81a437bf8792","datavalue":{"value":{"entity-type":"item","numeric-id":3805957,"id":"Q3805957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$CD083E17-5634-4121-9297-D7709636B6D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5a5928533f1a1251f0d11dc18c7b4ce473f48af9","datavalue":{"value":{"entity-type":"item","numeric-id":4187337,"id":"Q4187337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$7D65D315-B389-4435-AFDD-2523BF21FB02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"daa75d76e1cdc609f7ac46974607202a4c628e1e","datavalue":{"value":{"entity-type":"item","numeric-id":3275832,"id":"Q3275832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$FC25D2B2-706B-4157-BAC3-A2E07A9105D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6533c55d263ccad36a67078c52f1b9a5e6edc403","datavalue":{"value":{"entity-type":"item","numeric-id":3225403,"id":"Q3225403"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$FE793AC0-A3F2-46C8-B995-BD86F4AAB426","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81507f430d90ccca44c5914f167260e0646ee88a","datavalue":{"value":{"entity-type":"item","numeric-id":2751379,"id":"Q2751379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$F7D14E66-EE3B-4779-95B9-8120396399F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d9bcd33943731bfa2ecd0fbea7c90d9866badb75","datavalue":{"value":{"entity-type":"item","numeric-id":1819255,"id":"Q1819255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$7349D349-7A87-4D04-A09B-AB73DE7FF16E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c0f03bf183c7a653e5e84320e58ed58d37b137b2","datavalue":{"value":{"entity-type":"item","numeric-id":1868515,"id":"Q1868515"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$FF00A3CA-F145-4A4B-936C-38512A61317A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78b4d4d0b5630ebb8638d125cfce3aede70a13d7","datavalue":{"value":{"entity-type":"item","numeric-id":5462451,"id":"Q5462451"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$9B924525-B9B0-4DB6-9641-22E8DC0DA991","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb40eaffa350ac2f00c7522e92d2e0a632635b28","datavalue":{"value":{"entity-type":"item","numeric-id":6488570,"id":"Q6488570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q865656$8D8F489D-8D6E-4067-A1EB-35DB8AF826F3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fa6e1584ddd25035cd17bf6777a0ae74b6c441e0","datavalue":{"value":"10.1016/J.JAL.2005.10.010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q865656$570595A0-8254-493B-8A5C-4BF9AAE1B8BE","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cc3a41b77047459a9d4e4943d28167843b41d129","datavalue":{"value":{"entity-type":"item","numeric-id":5505538,"id":"Q5505538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e298a7f4ee4dce0cadf546c0f1d4770647a42a15","datavalue":{"value":{"amount":"+0.7683252096176147","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":"Q865656$FF6E5F9F-015B-47E4-AA4A-DFB76F4B4B99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5caf9de33d1799cb19ca4a87514a35fe4bcf1918","datavalue":{"value":{"entity-type":"item","numeric-id":704001,"id":"Q704001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3236b834facd6a98718e53fb46b23ec76552c8a2","datavalue":{"value":{"amount":"+0.76394122838974","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":"Q865656$764C5D83-85E7-4AAE-861D-8AF7E99A86D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c60e6dd472b339361946582e6d0c3ea63cce798d","datavalue":{"value":{"entity-type":"item","numeric-id":5898514,"id":"Q5898514"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"59b2ef3b3a21b63a50dd5894ff60508ec46910ab","datavalue":{"value":{"amount":"+0.7607335448265076","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":"Q865656$0F3A4391-39DC-4290-B061-F9786FE68A87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bc268baf51e6f99f0ec7fc0e4bd70830f2cc4651","datavalue":{"value":{"entity-type":"item","numeric-id":5302560,"id":"Q5302560"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"22023d86d50324744b63f16a473b99c04a5d580b","datavalue":{"value":{"amount":"+0.7596448063850403","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":"Q865656$AD6A31C7-D4D6-4451-933A-07AA26E78648","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"19203accc4a7a22b6e0e7ded8f7f4df3e916088d","datavalue":{"value":{"entity-type":"item","numeric-id":5898512,"id":"Q5898512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d1bc72dec120453bb4e65b49a0e433ad5bd4727e","datavalue":{"value":{"amount":"+0.7527742981910706","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":"Q865656$0B3222C7-64C6-4AD3-9530-78947513461C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Supporting the formal verification of mathematical texts","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Supporting_the_formal_verification_of_mathematical_texts"}}}}}