{"entities":{"Q5064241":{"pageid":7093817,"ns":120,"title":"Item:Q5064241","lastrevid":100337096,"modified":"2026-06-05T21:53:26Z","type":"item","id":"Q5064241","labels":{"en":{"language":"en","value":"A mechanized proof system of the third generation calculus in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7494929"}},"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":"Q5064241$B0ABB5DA-6E2E-4974-B20E-065D26632679","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0edb52260971df8027152b81bab289cfc5a60494","datavalue":{"value":{"text":"A mechanized proof system of the third generation calculus in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5064241$48B2BA6C-8F0B-499B-8FB3-833837885C2E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"76baa279e89d39bafe3e24909aab77207fffff4e","datavalue":{"value":"10.1360/SSM-2019-0327","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5064241$A8D10D46-4AC1-42D8-9BC4-33F16112BB7E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9150fd7e822de9b5bd6867587e74fac6a01307a5","datavalue":{"value":{"entity-type":"item","numeric-id":2005810,"id":"Q2005810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5064241$9936CA79-89EA-4374-81C4-651A067445BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"91640044ab4f6e0d128352966b648ff9856db7a6","datavalue":{"value":{"entity-type":"item","numeric-id":5041062,"id":"Q5041062"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5064241$704360D7-D642-4FE9-883D-A90C833A9809","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"43a31895517029ad54c69e8d4a7db6cda5630551","datavalue":{"value":{"entity-type":"item","numeric-id":328060,"id":"Q328060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5064241$B2BB246C-F0FE-4EB2-B5B4-558B537F07FF","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b56e80ecf599a7371c14b223e469166f2b1a45dc","datavalue":{"value":{"entity-type":"item","numeric-id":5017549,"id":"Q5017549"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5064241$C86661AE-302A-45DA-8908-FC01B5FCD24B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9d3dbf12e1376632bae2e48d8bc3683002116149","datavalue":{"value":{"time":"+2022-03-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5064241$4CCA65B8-C70C-4E62-9E1C-23B14181A822","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5064241$EF41BEBB-36D5-4326-9FA7-4741133348E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2b303d585fe21f20cd0cb9c8ba90fd986b6486a6","datavalue":{"value":"44A45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5064241$A03EED0C-9E29-4A84-A2FB-5A9D9B72427B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5064241$F9B9DA8F-ACF8-4FDC-8771-D45E97DF2311","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b56dc6b3699dfc9ea2bcc614c3bfc6cfa3734459","datavalue":{"value":"7494929","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5064241$9E6BC643-43A4-45E7-8852-0B9FA0EB4345","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"37d611bfbdf7ac5fdbe5074abdf9cd643165cf47","datavalue":{"value":"proof assistant Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q5064241$57724E68-0004-463A-9022-4EDA24C59537","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ba9377ad63bcfe4528d4ae4ec45d70b7fdbe9ca1","datavalue":{"value":"third-generation calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q5064241$B4440F9D-70F6-4A7E-BC0D-468B46F36B19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d5ef51b89dbf72f7181f6b41896d9233a3e6b1ce","datavalue":{"value":"formalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q5064241$68D8030A-7AE6-470C-AB84-0D4A9520B207","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ed5b36acbbcdd78ff381b3635ec25a20340482b","datavalue":{"value":"mechanized proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q5064241$F0F26827-AA3F-4EF7-BDF1-87A6F26CB48B","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":"Q5064241$0B6EBD2F-B063-497A-BCA7-61C3081887FD","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":"Q5064241$961B0870-E0F7-46ED-9F67-76B93441023D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b500cd390d0d25f5fcc031e986c1f2d17257d34e","datavalue":{"value":"https://doi.org/10.1360/ssm-2019-0327","type":"string"},"datatype":"url"},"type":"statement","id":"Q5064241$DD6FB3EB-44DE-40CD-A58B-036D73F4DD1D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0263b5d309efa84798b1e470937ae83f50737848","datavalue":{"value":"W3119618113","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5064241$5921DD43-CE6E-423B-9031-BD33BFD2F4ED","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1813dee6ade6ce3af2af73d2234b94398df48393","datavalue":{"value":{"entity-type":"item","numeric-id":5958299,"id":"Q5958299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab7cde111ddde45cdf9bfa5a0481c0581941207a","datavalue":{"value":{"amount":"+0.9163793","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":"Q5064241$3765E469-0392-4672-A7A8-44C8A9F72333","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"90bd9f2f511e82abc41ce1f38ff8727559e8b7d0","datavalue":{"value":{"entity-type":"item","numeric-id":1201296,"id":"Q1201296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0d92db2a83affa18befae7adc21e194763eb826c","datavalue":{"value":{"amount":"+0.8912658","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":"Q5064241$54DF051E-3FE7-4B08-8006-C3ABF3D41882","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3f6f497407874e3ab164c554c350f73fc98fdbd0","datavalue":{"value":{"entity-type":"item","numeric-id":4989018,"id":"Q4989018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b2e4e1f16c0c7e923f0cd4955fd22c8d1fc0bd2b","datavalue":{"value":{"amount":"+0.8884","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":"Q5064241$9E322DD6-1C77-401E-BB18-ABC39E4FEE9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f10ab99496cb6262ad3ace56565c78c372e50ef7","datavalue":{"value":{"entity-type":"item","numeric-id":1714805,"id":"Q1714805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e8e791f510a04b84b2064629aaddb59d6b62a929","datavalue":{"value":{"amount":"+0.8824923","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":"Q5064241$D6752B30-2049-406E-8C9B-98814892E951","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"229fa832c9f679ac8d467437b0c437e298bca5df","datavalue":{"value":{"entity-type":"item","numeric-id":5961667,"id":"Q5961667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c6527000328d5ee3278498ca1a302efe6a19797b","datavalue":{"value":{"amount":"+0.8812107","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":"Q5064241$B430E33C-9860-420C-B85C-F3D168A63539","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7d60046bae08126dd93bdd36cf201317f032037f","datavalue":{"value":{"entity-type":"item","numeric-id":1426938,"id":"Q1426938"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3599448ae6012d32419946481785d240a283a559","datavalue":{"value":{"amount":"+0.87887764","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":"Q5064241$8D243EC7-D7C6-441C-9C21-00C4DFB1BA6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"050391e3f27b8bfab5af09f69bc4e968903fe067","datavalue":{"value":{"entity-type":"item","numeric-id":4871733,"id":"Q4871733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9117c1be971fb090abaad3e512dd33870da9c34","datavalue":{"value":{"amount":"+0.8748268","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":"Q5064241$F0BDF8FE-AABB-4111-8DB1-E354C5A5D63D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b112eee35eabfd306112c4a3f285b9abddd0a824","datavalue":{"value":{"entity-type":"item","numeric-id":3086937,"id":"Q3086937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7e03f3b8eaf0b31a7256ef3a2ed7e627ef22bbd2","datavalue":{"value":{"amount":"+0.8697415","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":"Q5064241$78990380-846F-43D1-A74B-7D4BA08989A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ac9c2eb9482b783c69c8f44330e38517e321c0e7","datavalue":{"value":{"entity-type":"item","numeric-id":4246942,"id":"Q4246942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"84475fca71d1424ad6cf963f1d2dea7dcdaa5b0d","datavalue":{"value":{"amount":"+0.8687327","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":"Q5064241$F0F72494-A934-4D7B-BF05-2D85C152E6E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"62ff28979b652e145e4af403c685db82feeaea4d","datavalue":{"value":{"entity-type":"item","numeric-id":2303595,"id":"Q2303595"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fb0c3fd3544c4d06c76068ee11bdc3912567f3e4","datavalue":{"value":{"amount":"+0.86803365","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":"Q5064241$C516CB07-185C-4444-8DC8-3C77D216EAA5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A mechanized proof system of the third generation calculus in Coq","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_mechanized_proof_system_of_the_third_generation_calculus_in_Coq"}}}}}