{"entities":{"Q1798946":{"pageid":1809688,"ns":120,"title":"Item:Q1798946","lastrevid":57566859,"modified":"2026-03-31T10:36:40Z","type":"item","id":"Q1798946","labels":{"en":{"language":"en","value":"Concrete semantics with Coq and CoqHammer"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6957957"}},"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":"Q1798946$3798C1FB-E4CA-438A-816B-9358F0931015","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cb0fe348f655eedd2cd91ee044e71f69c645ad2c","datavalue":{"value":{"text":"Concrete semantics with Coq and CoqHammer","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1798946$5D586CC7-73E2-42BD-AD37-119C7EFBA8CF","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"405a8f1ec8c54b9433e3240752a2a616ef305501","datavalue":{"value":"1417.68181","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1798946$42494675-186F-4D49-BDDC-61DEF3216A20","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"673833a7274b9b82c0a357a91c29d43599993e4d","datavalue":{"value":"10.1007/978-3-319-96812-4_5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1798946$A5E682FB-E738-4F43-8737-FA866126B9B5","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f6522355932f1e9a9cd2b2f5c6e08a7adfa3b7ed","datavalue":{"value":{"entity-type":"item","numeric-id":1663239,"id":"Q1663239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1798946$0EFEBBC6-E8EC-4628-B473-46FFCA241EEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"23de4e42d26c5ff113394f059a29a12c73855bdd","datavalue":{"value":{"entity-type":"item","numeric-id":1798945,"id":"Q1798945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1798946$8BC48347-AFEE-4F6E-A435-1F127C68AB99","rank":"normal"},{"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":"Q1798946$2EF8FCD9-3FED-423D-9796-5CE1E09043B2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0172cdede3f306f1b36155a82f67164814fd11e5","datavalue":{"value":{"time":"+2018-10-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1798946$3B2705D5-2D53-45E3-9496-CB39A94F41B3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"94fe435b5cd6c48b4767728117fc020026e08ec8","datavalue":{"value":"https://arxiv.org/abs/1808.06413","type":"string"},"datatype":"url"},"type":"statement","id":"Q1798946$263AD6B0-E901-425C-8621-7B711BBE9DE2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1798946$0866AFE3-5CEF-4490-9C9B-1856A9C31AA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1798946$DC71D608-699F-4FE6-902F-ED022F67D361","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1798946$C17055CE-DC65-46B0-A3D4-CAE639BFFCEF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ae0683a5ad4c65ceeba1f22e5851db4c1b1a62ef","datavalue":{"value":"6957957","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1798946$D0B6420F-7661-4063-88FF-9DACD7C24874","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"faedc0622ee3e3ea3dee75f70d67bbbf05073a54","datavalue":{"value":"Q108482115","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1798946$33480AEA-7797-41FD-A5B3-F17800091995","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":"Q1798946$9ACD0E61-68F8-45A1-A9B7-4821FC7D49BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1798946$5DB33B51-CD3D-4556-A7AC-359A3F736F26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6a54eb5f0bc4bb2434371fed2614d3a40ec43e50","datavalue":{"value":{"entity-type":"item","numeric-id":41110,"id":"Q41110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1798946$6E23DAC7-D870-4738-99BC-6C41895BF7B5","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":"Q1798946$F5C5534C-A974-46A6-8D25-2225FA20C13F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3be7a8b5c8589d8ad8dddebe02be4e2dbe1b3c90","datavalue":{"value":"W3101720310","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1798946$60FC6B6E-98DE-4F61-809F-D0DBC98B4E7A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0758cb2f5792b2024ef075b30c81b3d9098b43b3","datavalue":{"value":{"entity-type":"item","numeric-id":2926333,"id":"Q2926333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b6e742d04a936456c4d6735f770602b43e7aee12","datavalue":{"value":{"amount":"+0.8135568499565125","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":"Q1798946$487599AE-624D-4D05-B938-4900D4C3C76F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d1bf37c15e48fc38e72aa136040f068ea21e0838","datavalue":{"value":{"entity-type":"item","numeric-id":5417200,"id":"Q5417200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f4c4a9b86c2f5e642a7efa94177c223aefa91cc9","datavalue":{"value":{"amount":"+0.7739906311035156","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":"Q1798946$D539EED1-65FC-4FD0-8106-6D18B45B8836","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24cdcf48e2229f3526631ece2a3e1a80cc930fcc","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5cee8ffcea980a2bd410cf8c1e4cdbfb7e03a95d","datavalue":{"value":{"amount":"+0.762656033039093","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":"Q1798946$35B423CC-9323-4EB8-82BA-AA03D06A9E77","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fab6c627236a21dbd8fc724b4508c8696aa53b03","datavalue":{"value":{"entity-type":"item","numeric-id":1663240,"id":"Q1663240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e1519a9fc1305523dbd3a6e7f6330b95c027c824","datavalue":{"value":{"amount":"+0.7467436194419861","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":"Q1798946$C25CA90D-8827-49AE-AE95-37636526FD37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d5d3a9bfaa35aeb9a6c1d64c9f4dc2c86ed3ca4","datavalue":{"value":{"entity-type":"item","numeric-id":4357063,"id":"Q4357063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f940d14c1e7a6fd3434bfbdb0a70f1842feb15d3","datavalue":{"value":{"amount":"+0.7400921583175659","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":"Q1798946$A492A2D0-1B1F-46C1-BD85-5616689580E1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1798946","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1798946"}}}}}