{"entities":{"Q5428262":{"pageid":7457836,"ns":120,"title":"Item:Q5428262","lastrevid":41878664,"modified":"2025-05-09T08:31:44Z","type":"item","id":"Q5428262","labels":{"en":{"language":"en","value":"Certified Computer Algebra on Top of an Interactive Theorem Prover"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5215402"}},"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":"Q5428262$19A9C716-4265-4426-B3B5-566CFD5CC2E6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7e0e75b5bf6058f9d00da4901adce4873d989fcc","datavalue":{"value":{"text":"Certified Computer Algebra on Top of an Interactive Theorem Prover","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5428262$B1D94F3B-F199-4D48-A3E3-4B8FDCB47E63","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a7bf2e5c6842daffcc6feaf82441173dbe671155","datavalue":{"value":"1202.68382","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428262$AEA1C4F6-C665-47C2-AA2E-48CD7385976D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4890e3b69781f5171c94b258b5a2f06753bb4983","datavalue":{"value":"10.1007/978-3-540-73086-6_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428262$29C03F5D-D8B1-4F51-AFF5-6A1B58D3597A","rank":"normal"}],"P16":[{"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":"Q5428262$F2F966FA-83B3-48DD-B3D1-A3B7B7A51D41","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c24cc198e7b26916e61ffb256f7b2af313e3e7ee","datavalue":{"value":{"entity-type":"item","numeric-id":865657,"id":"Q865657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5428262$2B4C1E2D-6488-4F20-86EC-F5B269E89E3B","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"0fde56500ce7b4c1f33971d2e4b588b592b48421","datavalue":{"value":{"entity-type":"item","numeric-id":5428254,"id":"Q5428254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5428262$F52FE282-0CD1-4198-86DF-25F20244C238","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f07a6e02313146619eb76647232125f099011046","datavalue":{"value":{"time":"+2007-11-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5428262$92A1D070-8E21-4F0C-AE8D-A269D8B80C8C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428262$D9D8C715-868F-43A2-99A2-38E26951A9D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428262$80D08ED9-D28D-48B3-BB33-646FDA8E835D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"13c9edf97977cedf01f3f221693abe6a2f1bb7bd","datavalue":{"value":"5215402","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428262$5371AB15-0FDC-4D0A-81ED-2D940C3E28C0","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"9313847d4265f8968cde9bf06161b8561b0bbabd","datavalue":{"value":"Q108482198","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428262$BC1BE443-E3E1-48A1-ADD0-DE33E4DC17CB","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":"Q5428262$61BB11BE-5381-4191-B901-766323402D66","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":"Q5428262$833B7684-91EF-4726-8AED-0ABDDF8FC676","rank":"normal"},{"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":"Q5428262$E7474ED6-895E-4162-9309-0B56120626D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d89eed7087f93c1cdf4120c868b02779d34eaa8b","datavalue":{"value":{"entity-type":"item","numeric-id":13309,"id":"Q13309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5428262$7A408FCD-5A0B-4B10-A220-31366247CF4A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5428262$22FF1B95-4A7D-431B-8A8F-FA01B6736FB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fed35f2083e1592d074e2b779038b334adec1c0c","datavalue":{"value":{"entity-type":"item","numeric-id":16433,"id":"Q16433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5428262$C9D88BF3-5912-4442-ABF8-2B064DBE4DBE","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":"Q5428262$5ADD6110-0DB4-45DF-9320-848B8F91BBF9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d951f9755d511d807df705d43cac69ff3257bb02","datavalue":{"value":"https://doi.org/10.1007/978-3-540-73086-6_8","type":"string"},"datatype":"url"},"type":"statement","id":"Q5428262$B863AA1B-DCB1-4DE6-A982-0AC4B376CB16","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d029414113e175a0cc56b35704344867a98b84d0","datavalue":{"value":"W1569069553","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5428262$3D265FCA-DF06-461C-B537-8D93959822E5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1fb8201d9b2c9308d37814ab7b71433d20eb0d52","datavalue":{"value":{"entity-type":"item","numeric-id":4499160,"id":"Q4499160"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"581382f6dd4109814ec452fe90bf0e5cdb3eb8d5","datavalue":{"value":{"amount":"+0.90025187","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":"Q5428262$BBCB55A5-E644-4A02-ACC9-A801354D0573","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea349871a95e3aab8afff32d430ce5dac7abae75","datavalue":{"value":{"entity-type":"item","numeric-id":4302792,"id":"Q4302792"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"625ae67542a4e30d0050a55abf115c27839b54a6","datavalue":{"value":{"amount":"+0.8966696","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":"Q5428262$C9834EAE-47C7-4A19-B15C-FF602317CBEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dc08b17a1ddd4ae826edaf57fd3e506f7115e9de","datavalue":{"value":{"entity-type":"item","numeric-id":3002926,"id":"Q3002926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"40aeabf01ccac5ce5772b24b47635300323370e3","datavalue":{"value":{"amount":"+0.89203626","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":"Q5428262$980EE55A-190F-4ADD-BEE0-671FEAC965D4","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":"404c55c56b59385a269b92b6bd7c3b055b8b6c46","datavalue":{"value":{"amount":"+0.89109993","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":"Q5428262$A512B930-19E4-4AA4-A225-418D45C2598F","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":"507506023178b659408c286c27e7a26624bb5624","datavalue":{"value":{"amount":"+0.8886622","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":"Q5428262$2BAB2353-AD71-48D3-BADF-9028671D0967","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":"dcdad1446d4dbfd51307cb6e7f580b75581d8a89","datavalue":{"value":{"amount":"+0.88866204","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":"Q5428262$B8A1C93D-B959-41F1-BE03-321EE9579F0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"89a1ccdd29f698747b6aa96da88440d993be29ab","datavalue":{"value":{"entity-type":"item","numeric-id":1272609,"id":"Q1272609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce34c3383802aefa43e604aeae44893a7f5fb289","datavalue":{"value":{"amount":"+0.88633585","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":"Q5428262$0329FE37-1539-48F8-9D7B-DD3CD355D2C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f578685aa3e5d0210ee8a4b098c1f01d3e10b455","datavalue":{"value":{"entity-type":"item","numeric-id":3831934,"id":"Q3831934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"12d4ef2970fea19d1cbf4ff404fc8b44e40ddc7b","datavalue":{"value":{"amount":"+0.88516676","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":"Q5428262$7963DE72-6ED5-42C0-8705-2A602DA100A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"88964ec0dcca17e8370c66d933dc0b826ae9cc08","datavalue":{"value":{"entity-type":"item","numeric-id":1080247,"id":"Q1080247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"12d4ef2970fea19d1cbf4ff404fc8b44e40ddc7b","datavalue":{"value":{"amount":"+0.88516676","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":"Q5428262$79E0C335-3660-451E-A70B-96E431587208","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8edc1921a70c57523407c530057e7f7de557b3ec","datavalue":{"value":{"entity-type":"item","numeric-id":4900163,"id":"Q4900163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ec9ef59b5dcd19c1679655c866fc259b52c9e127","datavalue":{"value":{"amount":"+0.8776649","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":"Q5428262$94F23199-9ACE-4DE6-9617-39E180D03C4B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5428262","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5428262"}}}}}