{"entities":{"Q2128797":{"pageid":2139540,"ns":120,"title":"Item:Q2128797","lastrevid":57726669,"modified":"2026-04-01T03:09:13Z","type":"item","id":"Q2128797","labels":{"en":{"language":"en","value":"Online machine learning techniques for Coq: a comparison"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7511926"}},"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":"Q2128797$41ED1B23-713C-4040-AA2D-BB13D4FC4A13","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9734020716cb889437a0ab91789a857844c681df","datavalue":{"value":{"text":"Online machine learning techniques for Coq: a comparison","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2128797$504D4B42-E2B6-4B80-B7BA-B9C54E858973","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"44735a148bbba59d61ee0929d5f904a9431ebca4","datavalue":{"value":"1485.68288","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128797$908C89AA-0E96-4B67-B611-5CE76E925FBF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"68d190c8eecb4e0dc0da13afdbbd0f59cf2db675","datavalue":{"value":"10.1007/978-3-030-81097-9_5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128797$2A1AB3AC-8E7A-427D-9826-185FCD83F1A9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5d60f422ea4078f78ffdc41c4f2ebf2d1fdd669e","datavalue":{"value":{"entity-type":"item","numeric-id":2128794,"id":"Q2128794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$FD77D088-3A26-4D77-9A60-032E4B652E8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a2a10f8493b6d512bfd4eade8423906525f6e138","datavalue":{"value":{"entity-type":"item","numeric-id":2128795,"id":"Q2128795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$E3B0A8AC-F027-4C44-805C-27F7A12EC4F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"95bfee5a3b5a686f6bf8619ba46dc852c102368d","datavalue":{"value":{"entity-type":"item","numeric-id":1799116,"id":"Q1799116"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$39967512-A227-4A93-A104-D096224A4671","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"76183100ad12bd4fa48540b506054eb98c9cbf9a","datavalue":{"value":{"entity-type":"item","numeric-id":2128796,"id":"Q2128796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$28701A80-5E7F-4D9A-90D3-190AF538AA8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"6ad6a046b48bbe4ab777309f1d5c19b5fc7dfbda","datavalue":{"value":{"entity-type":"item","numeric-id":286799,"id":"Q286799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$23A9677F-CAF0-49E3-AA49-4F1A41D67AD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc204e2e78d924e815f2b640ec35c8c2356ad41f","datavalue":{"value":{"entity-type":"item","numeric-id":286786,"id":"Q286786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$07958C0A-B105-43DC-B886-BB4A0C322D56","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6a2d220bbda83e730799716cad61153265e68ffa","datavalue":{"value":{"time":"+2022-04-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2128797$8288E988-FFE0-4C2B-8012-A56193F10147","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8fae2421fe99569bd5b5327fc16ca02fc5687326","datavalue":{"value":"https://arxiv.org/abs/2104.05207","type":"string"},"datatype":"url"},"type":"statement","id":"Q2128797$A84E48C4-6097-4E41-82B2-6914D5CC8557","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128797$C06686D1-4400-49C8-8FF2-C80AA91CB880","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cfe779e91fe9c53ee133568259955801965765ae","datavalue":{"value":"68T05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128797$08D78303-ABDB-4B98-8934-1EA8DBF92CA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2d5a866d412ef8af951814448fda0a03016cd3a5","datavalue":{"value":"68W27","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128797$CA54CE99-2D7A-4E81-8008-9C681C5002C4","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"e133780c55267191f56665e85c3c645195d74621","datavalue":{"value":"7511926","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128797$8331EA29-F914-4C71-95E4-9BBBC54431F5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128797$3EC399EE-9638-4169-AE13-B61C94EFABC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128797$1770B4FD-542A-4A84-BA0E-2AE4F1474515","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e0afe30fcd4cd25e8e8273c02ad48a97b4a0e001","datavalue":{"value":"machine learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128797$BF19E8F0-389E-4AD3-B874-D628325F8984","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ff3a87d2a1ef11672d22dcfbd650d697545a268","datavalue":{"value":"online learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128797$B8FA3902-524F-4CA3-B3C4-97C8E96FFCF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7dbe2a9ceb566acb6fb4d5335d65b6097a2eaa14","datavalue":{"value":"gradient boosted trees","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128797$76571C40-2029-490F-9904-22E0205E2355","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2f44a15a30b8157608a80223cacf62367b27a322","datavalue":{"value":"random forest","type":"string"},"datatype":"string"},"type":"statement","id":"Q2128797$B77D90E4-FADD-432A-ACD1-35C962755F54","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"33061b9a75e57d93e8912d2c2b716b27d6bd52ab","datavalue":{"value":{"entity-type":"item","numeric-id":40369,"id":"Q40369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$81D0A81F-648E-4350-970B-D0BB6176EB42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"742d2cb656243f7db933c39696cbb7d1991ef1dd","datavalue":{"value":{"entity-type":"item","numeric-id":32848,"id":"Q32848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$D6F958A3-0D38-438D-8116-D30DA86CA6D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"efbc9c0ffecce111990689e7c9fa5153da65c282","datavalue":{"value":{"entity-type":"item","numeric-id":5972779,"id":"Q5972779"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$967F1BE0-0345-4AD9-B7A2-10828E684052","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":"Q2128797$355A5D9F-9BD5-47E9-B32E-296445E1499C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"62ba86aa6537435eabbaebc8bfe3b9fc42cedbd1","datavalue":{"value":{"entity-type":"item","numeric-id":29448,"id":"Q29448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$65331300-001C-4357-904D-29BF46563BE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"af7e320eaa043645fcae501eca102305f45924c7","datavalue":{"value":{"entity-type":"item","numeric-id":40341,"id":"Q40341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$CA8C51CF-D527-48C1-AB6F-F0B73A7F0DD6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2eefcd7bdb58c6be6b16e3f48bd88dd62184746c","datavalue":{"value":{"entity-type":"item","numeric-id":40340,"id":"Q40340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$9B4882FE-5558-46A9-A0D7-A11B660ECC28","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":"Q2128797$05E8FA44-BA27-4131-A7E5-AED8E19E061C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0506a8fb0dbcdac73a9ec5e9acd6cb9ac9a15355","datavalue":{"value":"W3186870373","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2128797$4EE3258B-9BF5-4AE4-8359-E3378B14F0E2","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5eb040f4f53698848aa91aa2991b3af0b6cf962f","datavalue":{"value":{"entity-type":"item","numeric-id":4062679,"id":"Q4062679"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$CAFEB3E3-A455-42DB-ABBF-F3E832555CAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3af6b847528569308c270822a9e669d3f5e692fc","datavalue":{"value":{"entity-type":"item","numeric-id":2219409,"id":"Q2219409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$D9916081-85F5-4255-85DC-A52D84FFCF88","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5a73b7e48adb4260cb48d91e95198beb0803e94","datavalue":{"value":{"entity-type":"item","numeric-id":5952197,"id":"Q5952197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$E57B3BD4-F671-4942-948A-1DACFF422551","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"23ae3186b750126567f78f8fbe4fd7d86109b7ac","datavalue":{"value":{"entity-type":"item","numeric-id":2305414,"id":"Q2305414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$8A590524-BA7F-4E1A-9153-AAC162811006","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"579adb7a3f80eb6028df4cf77600de33d9e7a8ef","datavalue":{"value":{"entity-type":"item","numeric-id":1117690,"id":"Q1117690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$F57268CA-30F5-49EA-A266-2E48F62A5173","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05490fe10627fccbccba0d97cead358fcc16c362","datavalue":{"value":{"entity-type":"item","numeric-id":2964471,"id":"Q2964471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$91101198-9A23-41D4-A0BC-A604006E2C7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0df01f1f257aa4e0eda78a40444b30a121e95f5c","datavalue":{"value":{"entity-type":"item","numeric-id":4645730,"id":"Q4645730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$85921B73-CF38-4391-B3CD-6A27FD4D3DB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c577e428611609f51c98d78844448d28a70865f","datavalue":{"value":{"entity-type":"item","numeric-id":2031416,"id":"Q2031416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$40001B4E-2BC4-4FD9-9675-E916867DAFAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2c677e6ce616448e8e47a4ed08a6f7234133be2","datavalue":{"value":{"entity-type":"item","numeric-id":2913814,"id":"Q2913814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$11FF8180-69FF-4E97-BF03-E6519322DC08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"532a62b60e075fff433f243b2f28347c1a6df5f2","datavalue":{"value":{"entity-type":"item","numeric-id":2405272,"id":"Q2405272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$877F28E0-725A-4611-8F39-194908510067","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"41c828c42273fdd92d75a81a8b0926cb29b7e446","datavalue":{"value":{"entity-type":"item","numeric-id":1799117,"id":"Q1799117"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2128797$14F0909F-3589-4C0E-A916-E3D6F8C8CBC6","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"68b122fc17cf6c180e33e2295f43b455fdd3224f","datavalue":{"value":{"entity-type":"item","numeric-id":2219409,"id":"Q2219409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64535ecce6e567e911a673393ae31455a9b38373","datavalue":{"value":{"amount":"+0.7928164005279541","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":"Q2128797$81282856-DD47-47E9-9709-917B35F0F583","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80a02b86f5e7c12a000ea62837c3061ae5ebea26","datavalue":{"value":{"entity-type":"item","numeric-id":4645730,"id":"Q4645730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"29e820308881ab266cda2da10b95cc3c71ceed92","datavalue":{"value":{"amount":"+0.7273422479629517","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":"Q2128797$B59F0898-83E9-4EBD-910D-6F3F46C565DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eb636f355d8796679a448ab2f0465b71bf2a95f4","datavalue":{"value":{"entity-type":"item","numeric-id":3459922,"id":"Q3459922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"403be9716171a3463d3afb46bac4c89cf46bb26b","datavalue":{"value":{"amount":"+0.6894314289093018","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":"Q2128797$6FF973F9-EB7E-4AE7-A1BB-DEA8C22DBED8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d3472b195953f2a339aa5fcdef649bc9eac6cc9","datavalue":{"value":{"entity-type":"item","numeric-id":5327335,"id":"Q5327335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88f8b650c2b24e2514369740dc90a723458c5bdf","datavalue":{"value":{"amount":"+0.6836840510368347","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":"Q2128797$DDB26BBE-0C3F-45A4-B87C-24547C27EDBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eab127e20c4e479e5e30e398294a19c06fe4cca4","datavalue":{"value":{"entity-type":"item","numeric-id":2351414,"id":"Q2351414"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a975f25176ccbfcefe6b5972f4f4cb6146ecc2ec","datavalue":{"value":{"amount":"+0.6826757192611694","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":"Q2128797$B706A7C8-2260-4AC0-BCD6-F09DB0C079D4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2128797","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2128797"}}}}}