{"entities":{"Q2843038":{"pageid":2853758,"ns":120,"title":"Item:Q2843038","lastrevid":83849684,"modified":"2026-05-07T12:59:33Z","type":"item","id":"Q2843038","labels":{"en":{"language":"en","value":"ML4PG in computer algebra verification"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6197198"}},"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":"Q2843038$5C64C703-337D-4633-B76F-E3FF7937715F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b468ae7378b11ae07b7a56ceaa4166ecab90a2c9","datavalue":{"value":{"text":"ML4PG in Computer Algebra Verification","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2843038$989FE642-DBAC-42EB-AC6C-E0F6E0BCBCA1","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"688998d38dcf2438b47610e4c4c1a3e61bb33647","datavalue":{"value":"1390.68780","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843038$A61534AD-FC51-4146-95C8-7AAE18B39924","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4d973814518cd568d3a46b7acc03795556f8a640","datavalue":{"value":"10.1007/978-3-642-39320-4_28","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843038$7986DFED-A654-445E-8A8A-5E4A7A1F3EBA","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bc9df023cae9b25ea4b60776547a8efc95e2e421","datavalue":{"value":{"entity-type":"item","numeric-id":280197,"id":"Q280197"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843038$0A4D90FC-EF15-4F0C-A184-82CB2F4BF184","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"170e56a44d87084edf1707672598135a08e36b5f","datavalue":{"value":{"entity-type":"item","numeric-id":280195,"id":"Q280195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843038$6E38D0CA-5218-4FAC-8E13-B54C8470280C","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":"Q2843038$8658FA31-B626-4E8D-BC3D-40C609B40AEB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"381d46b885a4d4a1524f419ca9a0dc18cd8f863b","datavalue":{"value":{"time":"+2013-08-09T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2843038$E8782705-404F-4F28-93EA-A5F63397EB23","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8856aef6e60294a500f4bd46b4408ec8b7c21b1c","datavalue":{"value":"https://arxiv.org/abs/1302.6421","type":"string"},"datatype":"url"},"type":"statement","id":"Q2843038$5445A800-3100-421C-ACEE-BEDC80E26B50","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843038$480235B7-2E80-4561-A17A-602C0A5EAEB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cfe779e91fe9c53ee133568259955801965765ae","datavalue":{"value":"68T05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843038$FFE25972-390C-45D6-8702-E0AC33778178","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843038$E5689BE2-53A0-4211-8BA0-B7630F7EB0D7","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"343dd47ebee0acabe82021991970fec59a1d1443","datavalue":{"value":"6197198","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843038$6D1072FA-CD61-4A35-BBB9-0542ACBBB7B7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b92ee64274ae7e5afeb914225ec3738028529d8a","datavalue":{"value":"ML4PG","type":"string"},"datatype":"string"},"type":"statement","id":"Q2843038$04D8DCA7-4D92-4284-BF74-C42BC1996E24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2843038$5020240A-8BA9-48B1-AC31-E731C8B4A267","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q2843038$A3B1EA4B-8892-424E-8DC1-4B773D3B69CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"bc8ab3d14e29d837605a9096594ed45030120a23","datavalue":{"value":"SSReflect","type":"string"},"datatype":"string"},"type":"statement","id":"Q2843038$F56FB70F-AD6E-4D35-9ABF-6B294D2E73D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e0afe30fcd4cd25e8e8273c02ad48a97b4a0e001","datavalue":{"value":"machine learning","type":"string"},"datatype":"string"},"type":"statement","id":"Q2843038$15B1C8DE-8D29-4335-9672-3A5402196E97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e9c4e650abc856b5f51d0b5123c5930fad01c53f","datavalue":{"value":"clustering","type":"string"},"datatype":"string"},"type":"statement","id":"Q2843038$D5836AE7-62EE-4D5F-B2C2-18D02EBE2EC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"30b267e2fce1c66246262346a7c651625da01b6a","datavalue":{"value":"CoqEAL","type":"string"},"datatype":"string"},"type":"statement","id":"Q2843038$26054D9C-DEFA-4863-8903-E202A9AC6960","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d4725be8fa705861afbab12b59e447099c9ebb4e","datavalue":{"value":{"entity-type":"item","numeric-id":20216,"id":"Q20216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843038$F28953F2-11EB-4C7A-B05F-DFC27C973A07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9337f62f2e2e1a0506e5668f45d3e954d0bc5d5","datavalue":{"value":{"entity-type":"item","numeric-id":16057,"id":"Q16057"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843038$B65D1AF7-8E4B-493C-ADF1-115680A53360","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a94daa7865c51c0d2412cced8422ea9361d06e30","datavalue":{"value":{"entity-type":"item","numeric-id":21343,"id":"Q21343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2843038$64592EB3-E8FC-408E-91C4-D12BD9AC555D","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":"Q2843038$A80A3C0B-27EB-4EE2-8E10-B77AE57805A1","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":"Q2843038$63D3DD08-0415-4237-84DB-CC1274A4A1BC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"58afd212d531e9e87d864e873972664a72249426","datavalue":{"value":"W2133889836","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2843038$25E8BB15-46A5-47DF-9CB9-C574F7430F08","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"14b8b36929715000acf1cd883b9b1d7bc9f1ba30","datavalue":{"value":{"entity-type":"item","numeric-id":475385,"id":"Q475385"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9d0a1c8082c044f71e9255fbeb73ed0897f576f","datavalue":{"value":{"amount":"+0.745149552822113","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":"Q2843038$352FE39E-B88E-4ABF-81F2-C9B20F6826A1","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":"0ac89f7a61543ff8d263f5eee3c2343d0c5b1877","datavalue":{"value":{"amount":"+0.7072002291679382","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":"Q2843038$18FC3C48-D570-4E2B-8733-D5031159F412","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b3be07494f3ef7fb3e317edac85e81ec7cceadab","datavalue":{"value":{"entity-type":"item","numeric-id":2364671,"id":"Q2364671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0962c46538463ea8287031726528f1891b3455b","datavalue":{"value":{"amount":"+0.6972686648368835","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":"Q2843038$F1402C97-2D02-4AEA-8951-628E45806C8F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1f57a9cb0d60ed8e98a34e94255397679e507b2e","datavalue":{"value":{"entity-type":"item","numeric-id":3842177,"id":"Q3842177"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9d8b042332e97b313ed8f55bc976848a050b4628","datavalue":{"value":{"amount":"+0.6811150908470154","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":"Q2843038$E2DC22B4-706C-4474-ACF9-C3B00A07FB64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c6e02866bedcdddc38a6d5d0dc3312cefd57e45a","datavalue":{"value":{"entity-type":"item","numeric-id":2870142,"id":"Q2870142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9d8b042332e97b313ed8f55bc976848a050b4628","datavalue":{"value":{"amount":"+0.6811150908470154","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":"Q2843038$6C97A001-4AE7-47F9-9F74-4D8D1D0BFE77","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"ML4PG in computer algebra verification","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/ML4PG_in_computer_algebra_verification"}}}}}