{"entities":{"Q5170239":{"pageid":7199811,"ns":120,"title":"Item:Q5170239","lastrevid":94402706,"modified":"2026-06-05T06:43:31Z","type":"item","id":"Q5170239","labels":{"en":{"language":"en","value":"Integrating systems around the user: combining Isabelle, Maple, and QEPCAD in the prover's palette"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6319599"}},"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":"Q5170239$BBEF5CE1-29BE-4D8A-9D03-63BB6A30B0FC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a9657bc8556735b7c033c894b9d5de851a6d71a9","datavalue":{"value":{"text":"Integrating Systems around the User: Combining Isabelle, Maple, and QEPCAD in the Prover\u02bcs Palette","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5170239$46E79BE7-5480-43A5-9016-BA2571F062E6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7713341421d91598e941c54167bc36753fde9b5f","datavalue":{"value":"1294.68125","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170239$4509DD3F-7558-4455-9816-B8C213836137","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a20ba0f830157b69065a87d58c4f41556bd7f709","datavalue":{"value":{"entity-type":"item","numeric-id":3559772,"id":"Q3559772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$30E91801-8B0D-4EED-BDFE-8CC8435FD487","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8d78e8b1fd2bada0896418639974db329feb4fe3","datavalue":{"value":{"entity-type":"item","numeric-id":2102945,"id":"Q2102945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$01CE6F2A-6462-40A9-A27C-9936C1236928","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$3AEFBC73-655F-45A3-96BA-B2D44F36805F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ccf050e1c17ecf8d76a38048fff5f6c3dcd9c662","datavalue":{"value":{"time":"+2014-07-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":"Q5170239$B5330BB7-809F-40ED-AADE-784AFB470B5D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170239$6AB7A0EC-5D63-4FA5-A6F1-4629A5D496A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170239$7ECD0A60-7426-4193-8979-0D79EFFB13DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a50ad10d859c37581a66df0bd2c759d3d47ad6a4","datavalue":{"value":"68U35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170239$950179AC-3AB9-4315-AC02-626B640465F5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f439e77810e72c889bcaa2854049baa15aee848e","datavalue":{"value":"6319599","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170239$CBDB7B52-5914-4FAE-B51A-0C00EF719E84","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5170239$1B4E22EC-648C-4BDA-908A-409E7426DDB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"25a0d0a64145a26d41eb5308b1cb512dc20d7b36","datavalue":{"value":"computer algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q5170239$5D9A4D43-A028-4653-AA72-31352B021AE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3dd12981ba79112c8b0b36387f28037a89a463da","datavalue":{"value":"user interface","type":"string"},"datatype":"string"},"type":"statement","id":"Q5170239$E33979BF-4C61-4AA0-B8E8-BD79472D9706","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q5170239$CB21EBE1-72C2-475B-BBBD-E9527641C2F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0b5b609580845c3fde78254e089faf0e4f2c160f","datavalue":{"value":"Eclipse","type":"string"},"datatype":"string"},"type":"statement","id":"Q5170239$ACD45FDD-F773-414D-8773-B08D115E9971","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0086b3055db77debcd4b95500f3fd9ce3afc700b","datavalue":{"value":"QEPCAD","type":"string"},"datatype":"string"},"type":"statement","id":"Q5170239$2C28EA19-C523-4FD0-B195-56791F5BA773","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c69974b8ee44ba9ffc58b48877209f3953502907","datavalue":{"value":"Maple","type":"string"},"datatype":"string"},"type":"statement","id":"Q5170239$722A9EE3-8471-4788-B310-0233CA4CBDC8","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"e10cd4d07ec3897043c72dd605b7ee7599365ed8","datavalue":{"value":"Q113318094","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170239$30FC78BA-119D-4EA1-8C94-6F6DBF9EE72A","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"485f54a0549a89232924cb0abb443c2fad36af9f","datavalue":{"value":{"entity-type":"item","numeric-id":13300,"id":"Q13300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$8689EC5C-4B44-4086-922E-D84708E1AD29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c3aa95a2ec2e1aefe26078e8381cd9d370c279f9","datavalue":{"value":{"entity-type":"item","numeric-id":21663,"id":"Q21663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$A904C513-14C2-48C4-9CE5-F97903C659FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$674B98A8-E6A4-4B63-9950-BBF077AA736D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3c22b4e6c24037f313b1837c22cc6ae0308a77c7","datavalue":{"value":{"entity-type":"item","numeric-id":13503,"id":"Q13503"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$FC5EB80D-8BAF-41D8-ADD1-8ED862964DCB","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":"Q5170239$3A00800C-25D6-4D8F-AB51-03B9F9C42638","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1388bb528910bcb90b4dd9e5ef1eb9301b67baf0","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2012.06.010","type":"string"},"datatype":"url"},"type":"statement","id":"Q5170239$3963651E-0E7F-4B8E-968D-0BA2751F9D11","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"db2f997b7518008377b0cb69d7ab9f871fb4168a","datavalue":{"value":"W1967780008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170239$831B5998-9212-45B6-976F-BF09D0505AF9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8910a816017d823e1c2ea267ab4a7baedcd6f69","datavalue":{"value":{"entity-type":"item","numeric-id":5428268,"id":"Q5428268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$59DCBF5E-208A-4E05-BF88-BEC78DB8D32B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"017dca64578e6979a09aeeb8b382b1388bace1b7","datavalue":{"value":{"entity-type":"item","numeric-id":4810199,"id":"Q4810199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$58CB6BEE-C5ED-46DA-BF5D-C5C1D32EE9EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"08eaa6c03390b94af9efd4280f970d5d0809ce58","datavalue":{"value":{"entity-type":"item","numeric-id":1186711,"id":"Q1186711"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$AF422328-8E3D-4403-B6DD-37B96A9B3A5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a88a3979ab22dde430e91e87c194abc35b0eb626","datavalue":{"value":{"entity-type":"item","numeric-id":5505513,"id":"Q5505513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$A24D2830-AEC6-47E9-99DC-13F5F3D2B729","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c00ecccc176b971f8f655f17f279ab75b6423f0b","datavalue":{"value":{"entity-type":"item","numeric-id":2432769,"id":"Q2432769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$E7641ACC-336D-47C9-A1EC-3C3906C84F0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$4518D8BD-6077-409B-A51F-BCBE62A46ADE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6649652b5923ba2990ca57fd104729b65126b707","datavalue":{"value":{"entity-type":"item","numeric-id":2757856,"id":"Q2757856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5170239$C74C46F5-56F0-4F17-8138-FE8B2BEC5332","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e360320df2e6ba0969a5bba5a98917830ecca52f","datavalue":{"value":"10.1016/J.ENTCS.2012.06.010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5170239$DD5711F7-5E10-4801-A559-EF429452653A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a66722325834f65fa04ece2b13a78e7f4286fc92","datavalue":{"value":{"entity-type":"item","numeric-id":5505513,"id":"Q5505513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"85f0f8ec286962e1e9caa621c39201fa7e230d9a","datavalue":{"value":{"amount":"+0.9032220840454102","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":"Q5170239$C4E485EB-08C5-40BB-9F34-8752A678DC6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"404825eb196e28e9cdb897322b5b207a1e9328bb","datavalue":{"value":{"entity-type":"item","numeric-id":4790649,"id":"Q4790649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0fe707ef44bd4776bf0f712fed36d01c33f463cf","datavalue":{"value":{"amount":"+0.7849527597427368","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":"Q5170239$20C3FAA4-47D1-4D9C-9630-FABD350B6BFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"29cbf49a2d34b109d22fd4aed20f4c51c8b3874d","datavalue":{"value":{"entity-type":"item","numeric-id":4217952,"id":"Q4217952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"24340b3d7e5dcdd1d4fd739d961bf66d816345b9","datavalue":{"value":{"amount":"+0.7593064904212952","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":"Q5170239$65BFB19E-8FE9-43F7-9EF1-17CCAEB1ABCF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"78a99606c904bf3262d15e460058d95f88a306e1","datavalue":{"value":{"entity-type":"item","numeric-id":4934140,"id":"Q4934140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3086c3d0ab6ae241c2cd4fe6dfec4cc3c59aeef2","datavalue":{"value":{"amount":"+0.7530810832977295","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":"Q5170239$B4E0CDFC-6690-4F6A-885E-7E828F1E9B8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d31ac5b611e1dc394bc6dbb9071cf4d1998a3862","datavalue":{"value":{"entity-type":"item","numeric-id":4524769,"id":"Q4524769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"92bb04c74b30ebdd2adf7a991918b58d4421b265","datavalue":{"value":{"amount":"+0.7514771819114685","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":"Q5170239$14EF3387-F5BC-4705-B113-0A7791D9E4BB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Integrating systems around the user: combining Isabelle, Maple, and QEPCAD in the prover's palette","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Integrating_systems_around_the_user:_combining_Isabelle,_Maple,_and_QEPCAD_in_the_prover%27s_palette"}}}}}