{"entities":{"Q5958299":{"pageid":8135101,"ns":120,"title":"Item:Q5958299","lastrevid":40692797,"modified":"2025-04-04T09:24:12Z","type":"item","id":"Q5958299","labels":{"en":{"language":"en","value":"Proof by computation in the Coq system"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1715300"}},"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":"Q5958299$FD6A9FC6-7D3F-40C8-A2F5-F1AE97EFB99B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"42129b6ef318567e3694fed0ed47e6ed589e4025","datavalue":{"value":{"text":"Proof by computation in the Coq system","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5958299$56D9F80A-E51A-4A0F-9072-FD8F87D1555C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5df56915b2abdf0f6afc45d4679ba156d43f1570","datavalue":{"value":"0984.68137","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958299$E964D465-6134-490C-92DB-52C1E1A08B62","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"5f4ca30ee14f292eeb91c68ac5b19804f8b250fe","datavalue":{"value":"10.1016/S0304-3975(00)00354-6","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958299$5E94F377-CDE4-49BD-9047-0FEEA47C5E0F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c183090fe444b6ce6ac310ce96aaf75302471bd8","datavalue":{"value":{"entity-type":"item","numeric-id":235621,"id":"Q235621"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958299$B64DE17D-0D5B-4D61-85C9-435E17A2C7B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"d617c217f8f04ef480d650a973c1ec01fe67123b","datavalue":{"value":{"entity-type":"item","numeric-id":235622,"id":"Q235622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958299$CAF28B63-1AF5-472C-9F3D-A71DEEA199EB","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958299$CE12057A-B8BA-4CFD-9864-B4EA66A3C035","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"de0bbc1f0efc0eda52d8a37720ec217ae66c93cd","datavalue":{"value":{"time":"+2002-03-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5958299$BE97F201-4E94-4D1F-833F-4C55EFAD0A5C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958299$C467EFB5-9EAF-4489-A9B2-D5E94F15F28F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"831e040bb47a4efd27d831b061172aa2b184bd2f","datavalue":{"value":"1715300","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5958299$F307647C-9AF8-45E7-BC07-CFE0C06DDB0A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6a91657b93ea1d0263992f689500fd899d5bf908","datavalue":{"value":"automated proof development system","type":"string"},"datatype":"string"},"type":"statement","id":"Q5958299$7F700BBD-7BD3-4316-9E0C-B7E34330F58A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5958299$F277EFC7-2B2F-495B-9614-3808878B9597","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":"Q5958299$607F4EAA-2C94-47EB-8FEE-9EA29B15D245","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"55d1796d289926821ff098bc5ea53615142e836d","datavalue":{"value":{"entity-type":"item","numeric-id":21664,"id":"Q21664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958299$CDFF5F81-DBB5-416B-ADEC-7B97CA376F3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958299$B795D7D4-9F05-45A3-8A2F-74FA28E90AD8","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":"Q5958299$9A39D799-392D-43B9-960C-AE5578A6C55F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"bb04a3e1f7c2b128c194cbd9b09444095a7d8839","datavalue":{"value":{"entity-type":"item","numeric-id":4023825,"id":"Q4023825"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958299$4F8155D6-36BC-4E1C-916B-62B620C1692C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"09f9dec41c7615ebddca88a5ee0923f61e9449fc","datavalue":{"value":{"entity-type":"item","numeric-id":1610674,"id":"Q1610674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958299$AC5191F5-6A5A-4120-A69C-90B023462794","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f69aa78d91c4421b800f99cb382feb266d80c1d","datavalue":{"value":{"entity-type":"item","numeric-id":4647567,"id":"Q4647567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958299$027E98C6-B028-4034-9D6C-3192794C9A9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6aabaa97feaad45ae0b8bb65c0cb6403d6341e6e","datavalue":{"value":{"entity-type":"item","numeric-id":4393449,"id":"Q4393449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958299$DE1DBF02-1AFA-4385-8AAB-F1DE5CCE1E57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5c0445152e056b327286215039947692dcc08243","datavalue":{"value":{"entity-type":"item","numeric-id":3789525,"id":"Q3789525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958299$D8CAC127-2397-4ECB-B5E8-6279D4201B87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f5971f6f32ccebb0cec2f2ad3abf01be3f8f6ca4","datavalue":{"value":{"entity-type":"item","numeric-id":5958299,"id":"Q5958299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5958299$A0CF7397-2666-4B84-81D8-856821436569","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3dc045fab598bfd3b9a34ed308e2d8c5da3af8bf","datavalue":{"value":{"entity-type":"item","numeric-id":5064241,"id":"Q5064241"},"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":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958299$34C23C12-5C0B-4821-A764-CF14EE2FA4FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e3291d51f91ffa99d748f859f093a3ddfaa21724","datavalue":{"value":{"entity-type":"item","numeric-id":5472879,"id":"Q5472879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a11fccdad6a56f60df212b082cb7eba797fc4cfb","datavalue":{"value":{"amount":"+0.9138029","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958299$A50C3AF6-2654-4057-9EA3-11F7B3700BD6","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":"62128f2d9e5617e3ed5040ea8c28252a8b993f49","datavalue":{"value":{"amount":"+0.9118897","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958299$83E745A2-AD15-4168-90C3-D8122E8CEC51","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":"7c4c7dc51c8ec8d8e1855d278a8365c7c059d47e","datavalue":{"value":{"amount":"+0.90991426","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958299$7FA6A0A3-43E5-4EF9-8D24-26473CABADB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"45259a692f704ff9fa5333f98fe9a1012f3def9b","datavalue":{"value":{"entity-type":"item","numeric-id":2362498,"id":"Q2362498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1c9ebe1ca1aa601d64e284cc5d00bc08af25f4b0","datavalue":{"value":{"amount":"+0.9093776","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958299$4DB5D815-2AB7-43F5-99C4-F4A3A0719414","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f619454ba42d678fe38fa6e07ca2aa149bb91682","datavalue":{"value":{"entity-type":"item","numeric-id":1868509,"id":"Q1868509"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"410da64645666f7a4968a8cb08f8e8d4cb559808","datavalue":{"value":{"amount":"+0.90664005","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958299$080C8E2B-3AD7-4FC7-BD66-33A7C2404A35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"98b8f8d931995eaca57c31014e4409fcbac4255c","datavalue":{"value":{"entity-type":"item","numeric-id":5898820,"id":"Q5898820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1f61810e0c63471899b194792c03e712341b562c","datavalue":{"value":{"amount":"+0.9048687","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958299$80D27694-FF04-4371-8B28-3E1F9C78B7E2","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":"d987e6975b0f1ed538bdeaa5f8e025499e72d5f4","datavalue":{"value":{"amount":"+0.903893","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958299$16736312-1433-4C1A-B1C5-644A582A24D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"eebdd0b218777c7184a5d10cf8ad8d1fba089cb1","datavalue":{"value":{"entity-type":"item","numeric-id":4282573,"id":"Q4282573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5cef5262d3a2bcab298ad87544029a7432369b29","datavalue":{"value":{"amount":"+0.90253055","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958299$B8A9637A-006A-4905-9716-DC32AFC3803D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7f5d84f9f10fe366e1ad2f2e537eef4ae556dc06","datavalue":{"value":{"entity-type":"item","numeric-id":402120,"id":"Q402120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ead3ab904dabe4ff06d3e5b644b30dc14a9dbd1e","datavalue":{"value":{"amount":"+0.90157926","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ba354e87a58191d58d132c60481c945a3234ce85","datavalue":{"value":{"entity-type":"item","numeric-id":6534273,"id":"Q6534273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5958299$A6AF2CD3-E9C0-48E9-8130-82809AB61132","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5958299","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5958299"}}}}}