{"entities":{"Q2303595":{"pageid":2314338,"ns":120,"title":"Item:Q2303595","lastrevid":55372783,"modified":"2026-02-17T14:43:36Z","type":"item","id":"Q2303595","labels":{"en":{"language":"en","value":"Bar-Hillel theorem mechanization in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7176931"}},"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":"Q2303595$4125503D-73E6-4912-9A08-C1F6F3C3E5FE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"419b1b2791675a8c4f03be196b41e19327d30be2","datavalue":{"value":{"text":"Bar-Hillel theorem mechanization in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2303595$D1175280-309C-4146-AD47-E83397E753EA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f31e83d7c0e6bdb68aca877c33e185caf9faaf50","datavalue":{"value":"10.1007/978-3-662-59533-6_17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303595$8775259A-71D1-4B31-B79C-0B94AE087147","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ac4d18af3addfb2f0cb6b5a8d357737876e676bb","datavalue":{"value":{"entity-type":"item","numeric-id":2303593,"id":"Q2303593"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303595$65BDBDFC-E9AE-4F2F-A049-8C0F8483AD50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8122b839e84c9b05ee3f611a2e9e15e079eadb3c","datavalue":{"value":{"entity-type":"item","numeric-id":2303594,"id":"Q2303594"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303595$AD57ADF5-AE65-4708-8D9B-DA9EE6BD9F4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cc11f5ce58594feeaf1246d5abc049d97d09e748","datavalue":{"value":{"entity-type":"item","numeric-id":2039299,"id":"Q2039299"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2303595$9F839914-AB42-49CB-A9E3-327EF78FE38A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"28eb8a4277470500766552d0320b8f6735887226","datavalue":{"value":{"time":"+2020-03-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2303595$1C2E53A0-6AAF-4DEA-BE0B-A9F95411644C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303595$D8225A63-A9D2-4F8D-B501-763F04689537","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9632e50dfd324b5cdcefb3a4fb27d3ad6e374703","datavalue":{"value":"7176931","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303595$99DD812E-342D-468F-8121-C798E1370817","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b30b88dd7d8d4d3a542dd1829bf3206a53951e76","datavalue":{"value":"formal languages","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303595$C48CF2A7-CB75-46B8-BE93-C209B87F9196","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303595$B780C430-3D83-443A-ABF9-5F0F5F14325A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"575f84d61c3046b3b70cca9cf4ab9a67592ae27d","datavalue":{"value":"Bar-Hillel theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303595$AAEDF361-AAD5-447B-B342-1ED497356E9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2955d3dde9a15e46dba801e05da2cd70a0c42a19","datavalue":{"value":"closure","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303595$E5EC8D70-D321-4EBB-A087-FBD30985B789","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab57561e8c95fe21680ade7400a07692c4406a75","datavalue":{"value":"intersection","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303595$F1C26C71-5C44-413F-A3A7-2D7A0A7AD061","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3ea9b35a533d874f0a32d77e584c8b61e0e7c2fe","datavalue":{"value":"regular language","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303595$5A636508-46AF-443F-8A3C-DF5E31773889","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d75d448735778f46c4e9667e177539a844422b26","datavalue":{"value":"context-free language","type":"string"},"datatype":"string"},"type":"statement","id":"Q2303595$D0968E3D-8005-4BDE-9BF0-C7226E03EE6D","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":"Q2303595$62DF4468-22CD-4F48-83E5-4DDC9073262B","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":"Q2303595$5E662CD1-5775-44DC-90B0-3EE54EDF6F0D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6e9088e234909e39d20acef234dbf12c2d3d2e96","datavalue":{"value":"https://doi.org/10.1007/978-3-662-59533-6_17","type":"string"},"datatype":"url"},"type":"statement","id":"Q2303595$533540AB-B339-4703-960A-9757943BC8FC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7c47bcf5a400e878201fa4d067043bbab1d88127","datavalue":{"value":"W2952435866","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2303595$84DE929E-6A0E-47C9-9E43-A1F78ECC463B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4b3c4d5ed75c3eac6e204b8dd838123f665867f9","datavalue":{"value":{"entity-type":"item","numeric-id":2333674,"id":"Q2333674"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"13b7d5b802607f7dac752a40925058fed5f62e5c","datavalue":{"value":{"amount":"+0.7809949517250061","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":"Q2303595$DF2B4084-9844-4F51-ACB4-FE14E0B551FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a91af2a4ed092b1374cfa3b06e47833008317d33","datavalue":{"value":{"entity-type":"item","numeric-id":2820703,"id":"Q2820703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e7d33724dfda8e1ed35b3577f1794d2f25b6031f","datavalue":{"value":{"amount":"+0.7655259966850281","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":"Q2303595$9DB587E6-8536-402B-81A0-224A76DDE688","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4115e76d2c8c1db7b9627e76ded168c94e3852cd","datavalue":{"value":{"entity-type":"item","numeric-id":5195278,"id":"Q5195278"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7c8b90d7037537ec58585000544b403f1722572f","datavalue":{"value":{"amount":"+0.7484056949615479","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":"Q2303595$F29BCE6B-D373-4FDF-B805-D12B30B54270","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d5cfc9baf4bf6693de7c50f02a5cc4c4483e419b","datavalue":{"value":{"entity-type":"item","numeric-id":386032,"id":"Q386032"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"79f94981be84989380f291636b4b7221e617aabf","datavalue":{"value":{"amount":"+0.7034903168678284","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":"Q2303595$1B3FE48C-0072-4C5A-97E5-0BA8904652BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b8cce3d082a23af633d39b9d288104134db74a13","datavalue":{"value":{"entity-type":"item","numeric-id":4931595,"id":"Q4931595"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d0f30240fa4093c7d4d2946a023140ac28daa2de","datavalue":{"value":{"amount":"+0.6861805319786072","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":"Q2303595$DC915BB7-A082-40F0-97FA-32B4402D3B07","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2303595","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2303595"}}}}}