{"entities":{"Q5717445":{"pageid":7746999,"ns":120,"title":"Item:Q5717445","lastrevid":101651531,"modified":"2026-06-06T01:55:57Z","type":"item","id":"Q5717445","labels":{"en":{"language":"en","value":"Mechanizing Mathematical Reasoning"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2244727"}},"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":"Q5717445$9484C3E9-2812-405E-BA2C-FDA8A59546EC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"72fe85e01709f12944d8ecd77a8d9733a0d516d8","datavalue":{"value":{"text":"Mechanizing Mathematical Reasoning","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5717445$C982CD9D-D8B1-4EC4-9115-780BCD4673C4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"aa07b50397967019e666686ed72edead9e39308c","datavalue":{"value":"1098.68696","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717445$2A91CC60-4D8B-4E11-A84F-6D0ABEC5259E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a525f7cd8b191ac2b9090383b0dabde3689f4ff2","datavalue":{"value":{"entity-type":"item","numeric-id":287280,"id":"Q287280"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$2E2053EE-4BB9-43E1-8580-308EC8FF1651","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"63a8ceece294270cdd3e0740817fe33ec4f8e10a","datavalue":{"value":{"entity-type":"item","numeric-id":862391,"id":"Q862391"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$B9F4EB63-965C-43E6-A1FE-300840BCD522","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ae7b209f4f6620b5b1c5d47a6aa15c4f2fbff1de","datavalue":{"value":{"entity-type":"item","numeric-id":862392,"id":"Q862392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$99B6ED30-5CE4-41BF-9D84-13BBAE86F953","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":"Q5717445$DB3649E4-9E04-4E22-AA71-EEFC89AFFB58","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0e93cf8dacd1ede76e69913529f9bf4e8192e151","datavalue":{"value":{"time":"+2006-01-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5717445$C1C692F3-34FD-4B55-A4CF-560062CB401C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717445$5058F557-5228-4597-A696-3B8D0E143D11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"0c6e71133293256880be082f6af9aa793c57d433","datavalue":{"value":"68T30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717445$54DE946E-4286-4212-8FD9-1651A270CF25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a762d1a2468ec8882180d0d1124f12b94f8eb1b0","datavalue":{"value":"68P20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717445$0E831FBE-776A-4B2C-8CA3-6A9B37C2047C","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c36c223eb207d0bc905cc76eaa328ae066b45e81","datavalue":{"value":"2244727","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717445$CB3B265C-D3E8-4EB5-B2F2-006A6B32EA39","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b443b776731e3bc75eb79b752e7ef8c4cee2d97a","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$754E81AD-1126-49D8-BD28-4124A0C67044","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c845b927c7c8299e3e10848fbe9373f51ae3559b","datavalue":{"value":{"entity-type":"item","numeric-id":13461,"id":"Q13461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$D20425D1-DB4F-4C94-9483-C599855A2EB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d3ed9701b24c07e8ddeb19932e1fa77191c06e95","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$5119C746-ED21-417A-A5C4-13C16048C5E8","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":"Q5717445$683B465C-EBE3-4BAF-96FD-CD997840E77B","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":"Q5717445$923277DD-2E94-4877-B00D-CA5F4F65407A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"aa1932f570e73c7f62a4052c44d20ca5fc49605f","datavalue":{"value":{"entity-type":"item","numeric-id":20724,"id":"Q20724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$0656395D-328D-47F3-AD9F-9D55F7EF5AAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d4b47ce3ba240cb2e5f738c61850addd1730efeb","datavalue":{"value":{"entity-type":"item","numeric-id":22255,"id":"Q22255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$1F8817F2-F2EE-4D38-AA9A-6794E0E1D887","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"76802187a7905926b2a38ec174758f899e34b9bc","datavalue":{"value":{"entity-type":"item","numeric-id":22347,"id":"Q22347"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$0BFD7441-F697-47CF-9D88-B45249AB0891","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"f028a8a6db3bc5ae4579b69f24eb8d66b93659f7","datavalue":{"value":{"entity-type":"item","numeric-id":31448,"id":"Q31448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$D0775E4A-36D7-4E26-BD1C-36627B3FFB9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"648f72141e71ba7eece3437af2f76b81124739c8","datavalue":{"value":{"entity-type":"item","numeric-id":33150,"id":"Q33150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$CB2EA79A-82A2-40D9-8DB6-50EE9EEF9950","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"dab39ec190c7fb2818b71468da9efc600915608f","datavalue":{"value":{"entity-type":"item","numeric-id":33151,"id":"Q33151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$81878B83-1E75-487D-AE25-E5DA30BE5C66","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d89eed7087f93c1cdf4120c868b02779d34eaa8b","datavalue":{"value":{"entity-type":"item","numeric-id":13309,"id":"Q13309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$06F54EAA-F9AA-44F9-BFC8-62403BB093A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9c40cf9a35904f638a7cabef2bc178bad46391f7","datavalue":{"value":{"entity-type":"item","numeric-id":13717,"id":"Q13717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$B846F42C-049A-4034-B9A8-9D5109F70FC3","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":"Q5717445$A0E1D8C1-CB38-4267-8F2F-663E326F9146","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":"Q5717445$6C9B263F-09F3-4C44-8C5B-6027E0204D4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c766f98bf98fe7cf06a05963cc75ed84be39ac3","datavalue":{"value":{"entity-type":"item","numeric-id":31394,"id":"Q31394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$D9921EBC-D903-4823-B767-94CE65B3261E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4a761178b05ceb8505a589f51ea41c7640322dd0","datavalue":{"value":{"entity-type":"item","numeric-id":33154,"id":"Q33154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$F262AE5F-6B1C-4C9E-8A48-3C429DD5D72D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a6f02bcb24557f971b385c173492e5163040d683","datavalue":{"value":{"entity-type":"item","numeric-id":33160,"id":"Q33160"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$5ECA4449-BFD5-418C-B5E3-52365650C60F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9352c9e5b9cc7a6f850b959b1d2a4ce245e1fbf9","datavalue":{"value":{"entity-type":"item","numeric-id":33161,"id":"Q33161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$175B869E-D8EB-47A6-AC09-B0EAC0814A46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c6f90a2f4d38316e0bb5a27c4b90cf6cce495aa0","datavalue":{"value":{"entity-type":"item","numeric-id":16295,"id":"Q16295"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717445$4DC21823-E62E-4122-A436-1049156254C8","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":"Q5717445$113D55D1-AA28-477E-9EFF-F033090E16E7","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":"Q5717445$AD15790F-300A-451C-988D-5B1F151DE808","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":"Q5717445$E094AB60-8C02-4531-916D-23112CDDB3CB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"703773b8d2bd6b8fbc89ad622e8566bce28b2e06","datavalue":{"value":"https://doi.org/10.1007/b106663","type":"string"},"datatype":"url"},"type":"statement","id":"Q5717445$8F60F0DD-C4FF-49A5-BAFC-83C374612A01","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"15846dcb4b029236c46835509fa6b1f264866a57","datavalue":{"value":"W2484955858","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717445$0B5DE9A7-5B25-4773-900B-02C7CC8D861A","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"222aa4c71b9d7ceffdd56e5dd6ca1fc858b04bb7","datavalue":{"value":"10.1007/B106663","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717445$4342FB03-1CA0-4423-9747-BC546063BA7C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b168262f9e1b4514313a24dfabf8223d2ad31a3","datavalue":{"value":{"entity-type":"item","numeric-id":556682,"id":"Q556682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5973523c1fcd2c13f4cb7e75523b30baad3622af","datavalue":{"value":{"amount":"+0.7151433229446411","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":"Q5717445$658F17F7-FF3C-4641-8F86-D03FEB921786","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51563debbf33117fd6038171310562485cca5d0c","datavalue":{"value":{"entity-type":"item","numeric-id":2723443,"id":"Q2723443"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"01d972aa2e50afe98b1c475ad12eb0809cb67ed9","datavalue":{"value":{"amount":"+0.7085782885551453","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":"Q5717445$AB096EC1-9448-45F6-A229-6C2A106A82C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"04812e0faa39f2ad2d44990aa281e1a59afe1209","datavalue":{"value":{"entity-type":"item","numeric-id":1353941,"id":"Q1353941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b3a2deb49d6f02e6b2166f801ddf2d286edf627","datavalue":{"value":{"amount":"+0.7036978006362915","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":"Q5717445$5350ABE9-D911-4624-AAF2-AC1876BE2C5C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"361d73910ed31918e003ebc5ef836a04a599699a","datavalue":{"value":{"entity-type":"item","numeric-id":1978469,"id":"Q1978469"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a66ccce5a92caa40817fb9c16dda26d48e5e3383","datavalue":{"value":{"amount":"+0.7020559310913086","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":"Q5717445$71598034-B8E9-48CE-99D0-0FCB46024897","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fae19476a538d18195afae0ca93fef588863cf1e","datavalue":{"value":{"entity-type":"item","numeric-id":4628493,"id":"Q4628493"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"48eb90b26967a3bd207349d9d2fc0480b584cb84","datavalue":{"value":{"amount":"+0.701270580291748","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":"Q5717445$8C924DD0-6030-4F42-9CC1-9D6F1ECA0B6A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Mechanizing Mathematical Reasoning (scientific article; zbMATH DE number 2244727)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Mechanizing_Mathematical_Reasoning_(scientific_article;_zbMATH_DE_number_2244727)"}}}}}