{"entities":{"Q3386915":{"pageid":3397618,"ns":120,"title":"Item:Q3386915","lastrevid":53899118,"modified":"2026-01-25T21:56:06Z","type":"item","id":"Q3386915","labels":{"en":{"language":"en","value":"Natural deduction and semantic models of justification logic in the proof assistant \\textsc{Coq}"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7291122"}},"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":"Q3386915$0A5BD37A-835A-4F52-9B27-34E4B4DB2D34","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0f4f9f9c7ae37ad388f23ac8088d2c7f73482420","datavalue":{"value":{"text":"Natural deduction and semantic models of justification logic in the proof assistant Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3386915$DA247DC0-BB1F-4A6E-8F09-F74162736C21","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c5aaad65b8ad856410e8b269a319a2ea7ce4183b","datavalue":{"value":"1477.03032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3386915$2F6FE227-D2C7-4A7F-A2CF-127B3A16A717","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7f89853d01fc9a0192ea27c90d2d3a924517a0b2","datavalue":{"value":{"entity-type":"item","numeric-id":3386914,"id":"Q3386914"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3386915$C2DEE743-290B-4F3E-B9F0-C85D1968B43E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"accb1f0221ea6b057b90fd9423bbb12b2a94d5d8","datavalue":{"value":{"entity-type":"item","numeric-id":2011629,"id":"Q2011629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3386915$3F7728F3-9DF8-4351-8DF7-629408482986","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"2322a21df36f02b2b9c16a6174c764d5fc949009","datavalue":{"value":{"entity-type":"item","numeric-id":3061274,"id":"Q3061274"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3386915$41CF48E2-7D84-469E-B8F6-848B81FB4D6F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"20f5a5d62f60415f5fad4a5a75afa6346714a9ea","datavalue":{"value":{"time":"+2021-01-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3386915$4E0A8BC7-9B7F-408D-9154-1F80578DA4B9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3386915$2C742D05-951D-4268-90DF-008FCFED3F1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"19e8b53914fe36a939b2f687be46776db2609217","datavalue":{"value":"03B42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3386915$33A11FC5-2193-4425-999B-C7A4853C8AC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"74a6cec96241e450625296e63e8dd539239d7104","datavalue":{"value":"03B45","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3386915$1A8C463F-1223-441E-A32A-392427A09681","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3386915$962E7667-26FA-4D64-AEDE-668587B5EFDF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"18300a3bc13bf4c9b037b5f57a6c8336b661e7d5","datavalue":{"value":"7291122","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3386915$897CE330-1205-42E4-AD24-DEDB426D7CF7","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"afca37ec283c436ac56ea7dfcea0bd6378181bac","datavalue":{"value":"justification logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q3386915$199F7FBB-216C-40A2-9510-4316A3B0D260","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a7245057d33d9a959e820bafe53b372c083536e6","datavalue":{"value":"natural deduction","type":"string"},"datatype":"string"},"type":"statement","id":"Q3386915$FBDCFEEA-33C9-4D5E-AD08-711970D4E502","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4570cf96dc346c3171ef16b04ffc5ba8285007cd","datavalue":{"value":"\\textsc{Coq}","type":"string"},"datatype":"string"},"type":"statement","id":"Q3386915$B52C9FA3-3C76-4CB5-9585-15DE21100A8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f1dda010537b7b36bd45151721146f720815706e","datavalue":{"value":"modal logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q3386915$3A7782BD-88B0-4348-BF81-CBB4E864E996","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe51228e17b836f3520db7bc0de40e5086eebee3","datavalue":{"value":"soundness","type":"string"},"datatype":"string"},"type":"statement","id":"Q3386915$4BFB193A-D15F-4E1F-BDE4-16E825388D08","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":"Q3386915$61AE0A5B-6437-4A95-8652-115A2E70BB71","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":"Q3386915$B3F2E582-B3DE-4A62-8A59-264E50E94048","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"499fc1fe8feb5f5f713c961c396f67727d807628","datavalue":{"value":"https://doi.org/10.1093/jigpal/jzaa007","type":"string"},"datatype":"url"},"type":"statement","id":"Q3386915$8F09F42A-BCB9-41E6-9CB5-733A8A8FF7D0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e973d8922ffc45cc6cec9ead6a9baf9d34ec02b6","datavalue":{"value":"W3037187760","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3386915$704CBB94-DC88-4A91-8139-5D0452EA4E71","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4a254f2ae6f72c8a81c680239dbcf50fee87442f","datavalue":{"value":"10.1093/JIGPAL/JZAA007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3386915$326F776D-34BC-4B19-ADE8-03D2B9BCF140","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0f1e97173db305564213a200ec48a7aa5ca858bc","datavalue":{"value":{"entity-type":"item","numeric-id":5376691,"id":"Q5376691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a2d8c5b99393e649786a3b80ac74ed43333169db","datavalue":{"value":{"amount":"+0.7891702651977539","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":"Q3386915$F98911C9-27CE-43FE-9ACD-F225F3C8B38C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8d6d293412ec27137e9c499546b1328aad012c7d","datavalue":{"value":{"entity-type":"item","numeric-id":3133155,"id":"Q3133155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"424280bf47b3ddaa8444d66c11e5aea331c95766","datavalue":{"value":{"amount":"+0.7695376873016357","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":"Q3386915$3113EC31-C3D3-4930-B64F-AE596B1D07A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb12b278698d822d19d7761e0d6c2f8b03e37466","datavalue":{"value":{"entity-type":"item","numeric-id":454364,"id":"Q454364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a149924ae669e9a3a06c9509a5be09f6e0f573bf","datavalue":{"value":{"amount":"+0.7676938772201538","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":"Q3386915$65513D63-23CA-4947-B9C8-F707924C45DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1179604e13f068b59eb285e9dea483e3dd0a9e00","datavalue":{"value":{"entity-type":"item","numeric-id":5232011,"id":"Q5232011"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"740d296b5150d0a421486e92cf9c3469ddee5a44","datavalue":{"value":{"amount":"+0.7638079524040222","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":"Q3386915$DF9347E7-328A-4FF0-A262-535326AD09FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7186f0013809c3e4cb025391805c923a1d04187e","datavalue":{"value":{"entity-type":"item","numeric-id":331048,"id":"Q331048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce087b8960f8640430825018d6296a8633debe5c","datavalue":{"value":{"amount":"+0.7631359100341797","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":"Q3386915$8294705A-8263-4C79-80DF-79A21E439C28","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3386915","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3386915"}}}}}