{"entities":{"Q5717440":{"pageid":7746994,"ns":120,"title":"Item:Q5717440","lastrevid":48625117,"modified":"2026-01-05T10:32:59Z","type":"item","id":"Q5717440","labels":{"en":{"language":"en","value":"Mechanizing Mathematical Reasoning"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 2244722"}},"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":"Q5717440$0D0C5EC7-E2E8-4341-87EF-369952C45BBC","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":"Q5717440$67EA196D-A5C3-4CEC-BC71-8086620BBBC5","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"54cae8c32bfa509764d48388b42e958a63491c9b","datavalue":{"value":"1098.68699","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717440$09C8E848-9FB8-4357-AE39-565C91A4E3E6","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"6a9059fbad1dac267c8b3db87819e98298f3d65f","datavalue":{"value":{"entity-type":"item","numeric-id":429595,"id":"Q429595"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5717440$DC7C55F2-A096-40CD-8307-20F815B6AC8A","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":"Q5717440$49714303-9D93-4790-8D11-C6127ADF5A17","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":"Q5717440$45E182D8-745E-47A9-B2F8-195760F99E08","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717440$D8038564-105D-42D3-BFC5-D37BA8277D4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717440$186CE7F6-6AAF-40F7-9627-F270E9B42B6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24aafcf24a21bd70cd3b62d3f5f72a6d0d82d816","datavalue":{"value":"68-02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717440$5D22A274-15CE-4FA8-AA67-3EC3405E4EAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"540259e42205310d3310d3dad9dbe9ae50303b84","datavalue":{"value":"68-03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717440$F28A5910-0F07-4B54-83ED-D39E73614831","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8fac778e97ae6432b3528aab99d155b26775440","datavalue":{"value":"01A65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717440$250BFDAF-F26B-4823-BE8C-D8134B87F532","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7e3623752238dd38b6b48185d2cfacb9cb264bad","datavalue":{"value":"01A67","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717440$723E12B4-1286-478C-843E-0F0F422D8ACD","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b2d60c70103151c5517ce8c7111e964de3db8d65","datavalue":{"value":"2244722","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717440$93F96BE4-3D51-4A4E-8B3A-3EA8512889ED","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c02ada00d51bfaa9acd79c1bb4a3514b800c1912","datavalue":{"value":"survey on implicit induction","type":"string"},"datatype":"string"},"type":"statement","id":"Q5717440$2052C66E-7771-426D-BCB1-62D9B62B0B19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ae7cb5a98402b25b0ad53a130c630bf464f5b7a6","datavalue":{"value":"computer-assisted theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5717440$4CF940C8-411D-4C42-8819-AD95EC42FB9A","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":"Q5717440$9C452540-3900-42D2-A041-5BC18F57DC70","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":"Q5717440$14D3B543-066C-4699-8EB3-BB0333317112","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"15846dcb4b029236c46835509fa6b1f264866a57","datavalue":{"value":"W2484955858","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717440$24C1FC32-6E8F-4C66-B160-838896F15EF4","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"222aa4c71b9d7ceffdd56e5dd6ca1fc858b04bb7","datavalue":{"value":"10.1007/B106663","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5717440$712CFA26-2A1E-442A-A8F3-6683A86C0B6D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e78411fb6358c197a545473f7bd40e42ae7a70e0","datavalue":{"value":{"entity-type":"item","numeric-id":1915132,"id":"Q1915132"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"38b0f0bd69ca1149c2a59ee06efefabd102df0c6","datavalue":{"value":{"amount":"+0.7504429817199707","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":"Q5717440$6306CF19-CFB4-49A5-970A-45C86BF1D681","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ae6a11fe9c7925bce8eaf884ea4961802e808d16","datavalue":{"value":{"entity-type":"item","numeric-id":2751366,"id":"Q2751366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"49f09f49b2fe9c2108b12d844f6389586437880c","datavalue":{"value":{"amount":"+0.7419172525405884","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":"Q5717440$07C61E75-B653-49B9-B17A-EBBEAD4FBA31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a33b033c6f23d4730fd2828d4a0b0fd41ff09f32","datavalue":{"value":{"entity-type":"item","numeric-id":4886736,"id":"Q4886736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"49f09f49b2fe9c2108b12d844f6389586437880c","datavalue":{"value":{"amount":"+0.7419172525405884","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":"Q5717440$D93C9417-AFD9-4ED0-8D36-54525E0E62A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51852894019aff4da996e23e31ecb38fe929c33b","datavalue":{"value":{"entity-type":"item","numeric-id":2751365,"id":"Q2751365"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"864093cc090b4929901cf4c99efc4ece457ad658","datavalue":{"value":{"amount":"+0.7319893836975098","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":"Q5717440$C9AA8E0B-41EE-400D-96E3-C4D562E008D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"99e8c2304de6d0f793edbe43b05f387f747a189e","datavalue":{"value":{"entity-type":"item","numeric-id":4913999,"id":"Q4913999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"864093cc090b4929901cf4c99efc4ece457ad658","datavalue":{"value":{"amount":"+0.7319893836975098","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":"Q5717440$E845807B-D190-429C-AA67-5843BA863C61","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5717440","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5717440"}}}}}