{"entities":{"Q2914734":{"pageid":2925454,"ns":120,"title":"Item:Q2914734","lastrevid":51558101,"modified":"2026-01-18T18:56:29Z","type":"item","id":"Q2914734","labels":{"en":{"language":"en","value":"A refinement-based approach to computational algebra in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6084483"}},"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":"Q2914734$56178310-91AA-40B0-83BD-65DCDE50213D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6e8c63da9d508ba5f4e6d0b59235b860e389979f","datavalue":{"value":{"text":"A Refinement-Based Approach to Computational Algebra in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2914734$7A312AC2-E462-4EF3-B516-BAF4872DD5A8","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a9d4dc07d45adf059243b96bc24c0df94676db15","datavalue":{"value":"1360.68745","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914734$2080A118-CC1B-4626-88EB-945F56463A6E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"71c65cc0c8fb65d1ee3e00bf0d343ed3f6ed9c1f","datavalue":{"value":"10.1007/978-3-642-32347-8_7","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914734$ADB3A3F1-6BA0-4428-83D5-9BAA7703D226","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"343748d25c380d16ff7d424df96b35bd8fa80111","datavalue":{"value":{"entity-type":"item","numeric-id":2900559,"id":"Q2900559"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2914734$0A22C16B-BED6-4551-BBAC-CF8AE10323DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"37b6655ff0c1854542b6f28c9af39f0877a44635","datavalue":{"value":{"entity-type":"item","numeric-id":2319989,"id":"Q2319989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2914734$50623FA2-171A-4660-83FE-9AE08C33CDEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9837115d701db3c6d1129817eee769862467ad1e","datavalue":{"value":{"entity-type":"item","numeric-id":2844695,"id":"Q2844695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2914734$A293F0A4-2BEE-4E32-8035-77E5162A18DD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2914734$6ACDBF41-8B45-41A3-9754-F28DEE9FDC43","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3e7cab8cb58b1ff0209167a4d2783976232f08c4","datavalue":{"value":{"time":"+2012-09-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2914734$6ED85CF2-12A9-4BD4-9005-241EB609B71D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6d1f6a87e08ff4ab1dae8d116d2d89a645f1e1d8","datavalue":{"value":"https://hal.inria.fr/hal-00734505/file/coqeal.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q2914734$8FBFC289-65FB-4A3D-AD44-9FFC6484B35C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914734$494B6339-9732-4A17-B22E-B26799BF93C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914734$D9851E6F-1073-4D3A-9203-F20AC8ABAABA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"6be78f1bad1f2f19058dbde65eb124c0430a7d27","datavalue":{"value":"68W30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914734$8768AE49-93D0-4031-ADC5-3492C99C055E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ec8d7fcfb410670b177a2f578b05548c71f31a96","datavalue":{"value":"6084483","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914734$F0700CF9-55ED-4AE0-8815-5F68EA39D83C","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":"Q2914734$98B00A8C-E4F2-49B4-BA58-C55FF781669A","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":"Q2914734$5EE2BFD4-A437-488D-A61A-FA7FCB4722AA","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b4a7d6a1b161f317906cd68330dbaf6beee8580e","datavalue":{"value":"W1649228311","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2914734$68F576E5-AC28-4429-B10F-F9CDD6904C2C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1a5b6de0488af39ef3830498792881213aa4e86d","datavalue":{"value":{"entity-type":"item","numeric-id":2938045,"id":"Q2938045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97077a3b570a5ab306ddb3980216020a8325a901","datavalue":{"value":{"amount":"+0.806471586227417","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":"Q2914734$80E24B5C-A71C-42B1-BB0D-BFFFDB51F4AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"56efa1d86bf45c449941928f13899f3d678e5969","datavalue":{"value":{"entity-type":"item","numeric-id":3613426,"id":"Q3613426"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"10c2d051fc9065700896e85213684d5dc8ba94bb","datavalue":{"value":{"amount":"+0.7686991691589355","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":"Q2914734$0AA35E48-E51B-4273-A1AC-79C3E6375D0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3873e81a6aa7d9231efcf123f72306b279203fef","datavalue":{"value":{"entity-type":"item","numeric-id":2303244,"id":"Q2303244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"415f8cea1b6b73f8138f568dbd390513f85599ff","datavalue":{"value":{"amount":"+0.7635431289672852","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":"Q2914734$E5987DE9-E8FF-41F7-A139-D400AC8ED26F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c160088cf25b70d48dfb6c6d0df5e8c0b8a72f7f","datavalue":{"value":{"entity-type":"item","numeric-id":4249903,"id":"Q4249903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d358ce8756b64bf2151ce602580768568d0da2d","datavalue":{"value":{"amount":"+0.7563775181770325","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":"Q2914734$E9C863AC-1A82-47D9-B53C-09426A560237","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8bc953dd1614a07144d617fb2b8a68487cd9ef5d","datavalue":{"value":{"entity-type":"item","numeric-id":5464700,"id":"Q5464700"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"153b139102f3c148cc56c190af4466288ae7677e","datavalue":{"value":{"amount":"+0.7541675567626953","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":"Q2914734$5795109E-03AB-474A-8DCD-056D828253B6","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2914734","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2914734"}}}}}