{"entities":{"Q5747731":{"pageid":7777282,"ns":120,"title":"Item:Q5747731","lastrevid":51080345,"modified":"2026-01-16T13:40:57Z","type":"item","id":"Q5747731","labels":{"en":{"language":"en","value":"A case-study in algebraic manipulation using mechanized reasoning tools"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5785417"}},"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":"Q5747731$18B8E5A4-7D2D-4CCF-A8D6-2CF7E9541735","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"740deeb03bafc14d44b8234f888d4b3f9336c20d","datavalue":{"value":{"text":"A case-study in algebraic manipulation using mechanized reasoning tools","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5747731$D0174F92-BE02-4774-A924-CA0D770A070C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"889655d9509feb0b9d931ab4c19d8a48ab30ecee","datavalue":{"value":"1205.68358","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747731$B8AC9AEE-49A0-467E-AFDB-EAA194ECF907","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"d050f789ce4df95a226a861658e98fac2833d278","datavalue":{"value":"10.1080/00207160802676604","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747731$F03BE12B-DCB7-426C-A8BA-17B260F64760","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"1f8a1cf422dc8a39955e3a7180ef4ce8229538d6","datavalue":{"value":{"entity-type":"item","numeric-id":2710741,"id":"Q2710741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$4EA4148D-FEBC-44AA-9CE1-C4A76262958B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5f7d3744053f89b932df935693d4d726597e5f91","datavalue":{"value":{"time":"+2010-09-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5747731$D19C1D00-C34C-45F1-95DB-67D96F2132F6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747731$97090875-BAFD-43ED-B126-28BDA1B5F44D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747731$C075117E-DFD5-47F1-BCA4-2B7782DF5E4A","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"393a1294413c28f52d7e73b6ad2ef7595f13d60d","datavalue":{"value":"5785417","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747731$141EB882-D405-4392-A2E2-515931130F16","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a1565a842bed93d364bdf283eb7a1a945ea89013","datavalue":{"value":"mechanized reasoning tools","type":"string"},"datatype":"string"},"type":"statement","id":"Q5747731$490A4E90-C544-40AD-96A1-C03F3A69FACD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e36fd2915ee69146bd208b73e1714d6ba9054ec","datavalue":{"value":"symbolic computation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5747731$F45C399B-CCCD-464B-8787-B6AC598A5289","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"759a0214df8d3bfba2a5ae91a42bacd1cb2a9051","datavalue":{"value":"algebraic manipulation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5747731$95F22381-4664-4527-960B-DF865F32714B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q5747731$91ECB285-D8BC-4EBB-99FC-25907DBE09D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q5747731$27866141-A860-4911-B971-048A00CDCC02","rank":"normal"}],"P1463":[{"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":"Q5747731$3ECF0EC7-AEA3-48F4-AC45-A4B54BA208CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d9db21642bb525242f0a9c25c65251a61579aa2e","datavalue":{"value":{"entity-type":"item","numeric-id":21159,"id":"Q21159"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$BBEE8C33-48C5-40B9-9359-FD04E047B9C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"efacd6a40fcceaf80f5658fa8699430affa80235","datavalue":{"value":{"entity-type":"item","numeric-id":17016,"id":"Q17016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$7C995B7D-BC50-4BE3-867F-EE4A67C85A39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$07283C7A-529A-463E-904C-C4A238CB9B80","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":"Q5747731$D116A256-1B2C-4AE7-A59B-7720FFFBD998","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"c4293b48d13cade075a0396d1811f2f3abf815fb","datavalue":{"value":"Q57721919","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747731$21637D88-653F-4933-BDE1-8CD73B66B9C7","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0f9ac9a2ea702d0975f300327bbbef1296ea36e4","datavalue":{"value":"https://doi.org/10.1080/00207160802676604","type":"string"},"datatype":"url"},"type":"statement","id":"Q5747731$A867E1CC-4C5C-4392-8D85-E77973CF43B5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"24d4f38b335abceb5b5f8464d1692b03dda7521e","datavalue":{"value":"W2051578513","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747731$C8D9770E-C162-4BFA-8EE6-3386039EA081","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc11a2379fcf282936837f86ebebfde76a6c82da","datavalue":{"value":{"entity-type":"item","numeric-id":5428255,"id":"Q5428255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$AF70C7E5-9465-40A0-9424-914A1AB7F187","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d879609d8f15fdc4213fe440341358cf0400f2a0","datavalue":{"value":{"entity-type":"item","numeric-id":5464704,"id":"Q5464704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$6CA477B8-9893-4E5B-8D35-F83BEC8B4077","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"af5454750f5d297118e2d43ae886b47301283891","datavalue":{"value":{"entity-type":"item","numeric-id":928666,"id":"Q928666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$1E66002F-DFE7-4643-B41B-F328CA252C23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$6BFA5D2A-C6EA-4C79-A4C2-A4660BBE38E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"54eee2313932f532ca016c516cb047dfc95351e0","datavalue":{"value":{"entity-type":"item","numeric-id":5428257,"id":"Q5428257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$6A612882-9886-4578-9E8C-AE6A6F806286","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$9703C3FD-1AE5-4559-BD0C-9C7FBFFEC28B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$91CC4F92-99E7-4DED-A29C-07A387D8F365","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2d300252a7f5ef02e60bd45537fcdd52068f537","datavalue":{"value":{"entity-type":"item","numeric-id":5505507,"id":"Q5505507"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$D531F0DE-6A87-4858-8F5D-9826F0128030","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"75f2c295c4449018ea4283ff294ef038c1799aae","datavalue":{"value":{"entity-type":"item","numeric-id":5441547,"id":"Q5441547"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$17166ADE-B15A-4A1E-A475-39F38117D996","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6a4fcdc0c0c73019909bb765662c69f2c1d7cae","datavalue":{"value":{"entity-type":"item","numeric-id":5817990,"id":"Q5817990"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$66F39909-F36A-4CA9-90DC-C3FCA3374868","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8a11b587785b43a7aba09896edc5ae68fbca055","datavalue":{"value":{"entity-type":"item","numeric-id":1413645,"id":"Q1413645"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$31E45E34-3A9A-40B9-B2E3-BC6B53D1FDB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9ae8c375c89f07df66a9b775a5c280d396c123b","datavalue":{"value":{"entity-type":"item","numeric-id":3613426,"id":"Q3613426"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$C0F47DEC-8111-4EF9-A5B5-D8978E543CA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50a8569e46b6ebf9bdf790ad48b6a4dab614e1a9","datavalue":{"value":{"entity-type":"item","numeric-id":5550390,"id":"Q5550390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$43795DF3-83B5-4F37-873A-31ED1A391C4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bdf829a201d0ee7f3788d86a2543089dc5b60dc","datavalue":{"value":{"entity-type":"item","numeric-id":3849246,"id":"Q3849246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$40FBD79A-E281-47A3-AC27-2BCF36216FB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$CC6F5EF6-F094-4833-A4A8-6626DE10A7D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9579a4ebc8fc362938d3ee4c1626b4dbb8862f2","datavalue":{"value":{"entity-type":"item","numeric-id":4281483,"id":"Q4281483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$779F6749-3A8F-47BA-9543-956B5D18AA28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9a357a3b561ccdc8d7429c7e14c4c790e76d26e0","datavalue":{"value":{"entity-type":"item","numeric-id":1612751,"id":"Q1612751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$97FD24BA-FFC0-4933-BE3C-4B684A580ACE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aa501f8d67d6302c19c53708c34f273d7a39ff38","datavalue":{"value":{"entity-type":"item","numeric-id":819987,"id":"Q819987"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5747731$DAA9A89B-E0B8-4800-BCC8-0BA8711641A4","rank":"normal"}],"P1635":[{"mainsnak":{"snaktype":"value","property":"P1635","hash":"ae15b4a8dcfe36792dd1877cd42b514641786ce2","datavalue":{"value":"journals/ijcm/AransayD10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5747731$69B550D0-529E-48C0-926C-3D8879EF7E29","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"70f35fc4a81f7271313465fb2bf057f212dc1b5f","datavalue":{"value":{"entity-type":"item","numeric-id":5464704,"id":"Q5464704"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"794dab7784633c01cd8437208ab89b9ebc808b15","datavalue":{"value":{"amount":"+0.7236728072166443","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":"Q5747731$C6662AE8-6C33-44AB-BF34-2D6C5B1B470B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7b68bd28f30ece9166a53b1d139e82f9d7c12d14","datavalue":{"value":{"entity-type":"item","numeric-id":928666,"id":"Q928666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f4aee07fd3dd6c46b0fc1bf22b22460ec38b600c","datavalue":{"value":{"amount":"+0.7156602144241333","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":"Q5747731$2CE7176F-F1FC-48D2-A55F-87B35283FB4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"913f5efd90d90f85d5491384cc864170d414521d","datavalue":{"value":{"entity-type":"item","numeric-id":5200131,"id":"Q5200131"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f47e1acc80e56f19df059b7fa6c1b9819a08ace1","datavalue":{"value":{"amount":"+0.6942824125289917","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":"Q5747731$DBB1C5C0-3F32-47CA-B8F7-6A2BEC2D1060","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d1260c05795c932f06071a586df7e7e9a7ce59cc","datavalue":{"value":{"entity-type":"item","numeric-id":2349534,"id":"Q2349534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eb5b57d17c79c8f2367b91b75b915e2e35136abc","datavalue":{"value":{"amount":"+0.6941736936569214","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":"Q5747731$A6BBF50B-83BA-4DD9-84B5-7A436A502845","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"16e53fc84cf0ec03f82070b7955189ac6aeb9559","datavalue":{"value":{"entity-type":"item","numeric-id":4217948,"id":"Q4217948"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4954d0d93eea29a096a924510b0ee79b10eefeb8","datavalue":{"value":{"amount":"+0.6898862719535828","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":"Q5747731$EA0A81FE-C15C-42F1-A86F-74494F578C99","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5747731","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5747731"}}}}}