{"entities":{"Q4647500":{"pageid":6677081,"ns":120,"title":"Item:Q4647500","lastrevid":97924982,"modified":"2026-06-05T15:49:19Z","type":"item","id":"Q4647500","labels":{"en":{"language":"en","value":"Learning domain knowledge to improve theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7001894"}},"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":"Q4647500$82FA97FC-2CE0-4AFB-9889-EF7BFBE387AB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"ada34f0f792e5183c3cf82ebe98fb5ca0de564a2","datavalue":{"value":{"text":"Learning domain knowledge to improve theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647500$36CF9E05-01E2-4D79-A294-906E5F523F81","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c20b1a6ea58d1a15522b78eea45fb484bedd032f","datavalue":{"value":"1412.68217","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647500$39E7C459-4076-42F5-AFE2-C876869946F2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"0254756085a724500b016f700458c7f10b2ece9c","datavalue":{"value":"10.1007/3-540-61511-3_69","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647500$E85823A9-1630-46A8-8F09-D8C97FE0A6E3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d56d5ccd17352375824e5b771556391ff9b2d99c","datavalue":{"value":{"entity-type":"item","numeric-id":1854366,"id":"Q1854366"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647500$DA0C1928-E325-4317-A487-A824A2D3DA75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"41390ccb2889a06af91bd7d467009a1fde2d1850","datavalue":{"value":{"entity-type":"item","numeric-id":862394,"id":"Q862394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647500$09B57D2D-F611-4586-A557-DB4A9450F57D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1c1c5ae1cd90ac8f2e7ae6528ac21a720bbd1fe8","datavalue":{"value":{"entity-type":"item","numeric-id":4647495,"id":"Q4647495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647500$CD5FF5AF-05F8-438A-8839-1A8ED08D5096","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647500$41F9EB9C-410F-4A36-AC2C-47DAD5601F23","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647500$A193E342-AA32-48A0-B060-8789D3908019","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"66c278d699dcccb832c10cd7e1826f2c69d6d8f0","datavalue":{"value":"7001894","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647500$F0AFBE05-C8EE-428A-9F0D-8B7058A319D9","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ecfb6d83a48569689cbe547116ad47417c503610","datavalue":{"value":"learning strategy","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647500$8B299D4E-52CB-4FD7-950E-BBEDC15B20E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"14a0dd3e1b83404196449aa90cc83aae915af1cf","datavalue":{"value":"proof system","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647500$AEFCC2BF-7B09-4CE8-B880-C0EBFB61E6E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2d636dc56d6724ceb60a2cfdc326a204980b039f","datavalue":{"value":"reproductive mode","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647500$2877878F-FC26-4B59-95B3-E3620320F7F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"840232c250b1e1458d71cfdc7fbe467b8d493361","datavalue":{"value":"critical pair","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647500$25B41C2F-82F8-437B-950C-27A5606546B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d838d10ca3a34938b22d8466db1577eef0990384","datavalue":{"value":"learning team","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647500$77458A18-5879-4B6B-89DC-0B1827AB20CB","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3f1ae8e244d27f4e93f1981ec80f87d04dfe89da","datavalue":{"value":{"entity-type":"item","numeric-id":31438,"id":"Q31438"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647500$8AD93E6E-2B2F-43DA-A48A-E44EB37D8076","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":"Q4647500$F1B6A33D-F75C-4DC4-8276-03263AB35D24","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":"Q4647500$059CC64E-FFB2-41A3-BD82-35CF25DB8AAF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"eea75ec7e90f07d72c5505b6bd3fca2d4d19ca7c","datavalue":{"value":"https://doi.org/10.1007/3-540-61511-3_69","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647500$D01DC921-665A-416E-9153-DB1F71DC2E40","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2b5577163047941114104f3c3f10c6cace843322","datavalue":{"value":"W1881432009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647500$B37C4D80-32D9-4662-BF02-959D0CE1705C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b4e3dde57ec92f719c86b2adbfa7880e19c17f","datavalue":{"value":{"entity-type":"item","numeric-id":5055785,"id":"Q5055785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647500$FE4CA91C-5FD3-4A2E-A843-11398143D967","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"59bb3344b4f89870291c44462654819d8a7d7295","datavalue":{"value":{"entity-type":"item","numeric-id":3809306,"id":"Q3809306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647500$076DFB0C-3EF9-4E4C-B1E7-79E482D943BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b11e19574508418c19657a6f1385e1d5821221a3","datavalue":{"value":{"entity-type":"item","numeric-id":4647545,"id":"Q4647545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647500$CF0C04B2-CF9B-47AE-B498-C307CB42F9FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b95a10e194b852a6f6838734d909c8312bfc826f","datavalue":{"value":{"entity-type":"item","numeric-id":3028369,"id":"Q3028369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647500$B42F9A10-5528-4A9C-B024-D254D20AC1CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"599c5dbf52817fbbe5f2f15e33a96dc6ac97514e","datavalue":{"value":{"entity-type":"item","numeric-id":3908463,"id":"Q3908463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647500$ABF5AC35-D35A-46D6-8EC5-6F8969920FF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a1e0b4fc54e8c62a86959e50d4b1b27d9d9a092c","datavalue":{"value":{"entity-type":"item","numeric-id":5581665,"id":"Q5581665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647500$C0F2F6E1-D31C-41E0-8ECC-F9AA49F92365","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07441aec0715add91dbf903fea4c539fe7c16a9c","datavalue":{"value":{"entity-type":"item","numeric-id":5210777,"id":"Q5210777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647500$EB4868A0-37D0-4074-9364-46A42C701CE3","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5dc35801f25d4e873a92e4e6ee27d4249fb83802","datavalue":{"value":{"entity-type":"item","numeric-id":4728284,"id":"Q4728284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3f92c4789d194c9630aa56a8758b134db9fb8c27","datavalue":{"value":{"amount":"+0.9184743","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":"Q4647500$BCF0FF88-D09F-4F8C-9612-4BCB4DE0B84A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3b47d0f068d0e927590f2b56d80859ca587da1d3","datavalue":{"value":{"entity-type":"item","numeric-id":2740950,"id":"Q2740950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6ec85177fd1c4b4561effb38bd484818d0e36bb5","datavalue":{"value":{"amount":"+0.88644207","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":"Q4647500$A73188B8-3F59-4049-BB84-0DC5A7D1E459","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"56a0240dbb35af4bd803f60f4a8d82ce9b39f33b","datavalue":{"value":{"entity-type":"item","numeric-id":2142080,"id":"Q2142080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8f0d1900e9bb7fde7744ecb96552ed689fb0823e","datavalue":{"value":{"amount":"+0.8651241","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":"Q4647500$6FEDE174-6387-490A-880A-EF3C4321A084","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3e6e726c1ccf3d48bbd9191c4571af0a1046a6a6","datavalue":{"value":{"entity-type":"item","numeric-id":485842,"id":"Q485842"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"75ba542cdd49b4e9228759437ecece4b21235c58","datavalue":{"value":{"amount":"+0.8619283","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":"Q4647500$DBF354BC-D2FF-4C57-96F5-8190C6D52E86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"307c527ff9a633ff8423b5ee15fcb4c6f847fcfe","datavalue":{"value":{"entity-type":"item","numeric-id":5717445,"id":"Q5717445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"24e0ae5bd0d9082d1806faf560baf2984b651bbc","datavalue":{"value":{"amount":"+0.8586576","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":"Q4647500$88EDBBD8-A54D-4526-852D-85E7A5337957","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"776e4c784830960f08191feacfb851aa37febae2","datavalue":{"value":{"entity-type":"item","numeric-id":4797437,"id":"Q4797437"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5f771503e44ac24b4b268e27c35ca2bb8e3743bd","datavalue":{"value":{"amount":"+0.85559595","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":"Q4647500$A1DF51D7-16A9-4D06-BEC8-5CABA67A7892","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"733045d4bdb6ac84e39d437da15db86acd1c641d","datavalue":{"value":{"entity-type":"item","numeric-id":6108816,"id":"Q6108816"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"04ca27f2448befb84f9d770ee35c2380f71f0f21","datavalue":{"value":{"amount":"+0.85362226","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":"Q4647500$F4ED61C0-0320-4A22-A445-34B3B7AFD5E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b672819769f56e78f920c18ff9a2be8c99577da","datavalue":{"value":{"entity-type":"item","numeric-id":2751546,"id":"Q2751546"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"84214d655dd38afe21171fab9f5e8ef7ca6b1a8d","datavalue":{"value":{"amount":"+0.8488792","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":"Q4647500$7B046387-AE96-42CD-99FD-DE266460B9AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0ee8b4c79deb3aa57ce2641b4039a91462d9cc63","datavalue":{"value":{"entity-type":"item","numeric-id":4465166,"id":"Q4465166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f8a4f946298d27fc516ba5f4b30a1e2e313d9239","datavalue":{"value":{"amount":"+0.8425404","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":"Q4647500$38DE7F28-40DC-4C29-8DC8-A95A27DC2059","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Learning domain knowledge to improve theorem proving","badges":[]}}}}}