{"entities":{"Q6166143":{"pageid":13301025,"ns":120,"title":"Item:Q6166143","lastrevid":47883607,"modified":"2026-01-02T23:40:46Z","type":"item","id":"Q6166143","labels":{"en":{"language":"en","value":"Traf: a graphical proof tree viewer cooperating with Coq through Proof General"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7721431"}},"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":"Q6166143$F0F0B5D2-EDDB-42D4-8C95-26DDD7840454","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6e7d70bf7b4f326a67ecc298e100d7e833c45079","datavalue":{"value":{"text":"Traf: a graphical proof tree viewer cooperating with Coq through Proof General","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6166143$2023C79F-A90C-4134-9393-562F4C73B078","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ae2f6f111643f888e650bb5a1e0dd3ead3689347","datavalue":{"value":"1519.68313","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6166143$912C5B9A-71C9-418A-B358-0511E0E6DB36","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6a572efc522f7bf98d02cf7e8884f13929e642d0","datavalue":{"value":"10.1007/978-3-030-02768-1_9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6166143$82903D35-A2CC-4A5D-A0FC-24E5BFA30240","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c181c9d684a9fb9f9c6da60c764894b939811fa2","datavalue":{"value":{"entity-type":"item","numeric-id":2802490,"id":"Q2802490"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6166143$D4BCB35A-9263-4BC6-B761-0FC62EA8CABA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"9c19dd4d3e8899a403fa0414e68a99d14abfb24c","datavalue":{"value":{"entity-type":"item","numeric-id":5126864,"id":"Q5126864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6166143$69F50A12-5AB2-43B7-A70D-CFA953934BC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"787ffb0c02ec91676cc213b14098056d75874040","datavalue":{"value":{"entity-type":"item","numeric-id":6166142,"id":"Q6166142"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6166143$9F6171E9-E816-4A8B-9E2D-FB9F3944BBC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"565b8ea7186b617940e6131661ec8e05b7d56bff","datavalue":{"value":{"entity-type":"item","numeric-id":4408124,"id":"Q4408124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6166143$D6E95B02-276D-43F0-9AC7-EC9D24360165","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7efb66db9d8cc237b51d0f645d1a54c929d4c460","datavalue":{"value":{"entity-type":"item","numeric-id":2789030,"id":"Q2789030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6166143$C265F9F2-6F92-49F7-8269-1D0EBB0BB238","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c377ab7875b781eda1304e6f4ef79ea097f76f82","datavalue":{"value":{"time":"+2023-08-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6166143$FE0748AA-CDA4-4F70-BC34-48F8D994594D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6166143$62C17C39-76A1-4E9F-9BDE-42AC2CA0D7AF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9c482802f243548233aca362a6c53a086ccbfa18","datavalue":{"value":"7721431","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6166143$B03423E4-A80A-4DD5-90DB-0E2231B56BA8","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d675d4e88ad271e4af8b7876355ea09d0d128e02","datavalue":{"value":"proof tree viewer","type":"string"},"datatype":"string"},"type":"statement","id":"Q6166143$D811E29B-82D9-4CE3-B226-D36A9F54BCB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"73f877e2f1bc95df5bf8181b9880837b7bf0c2ee","datavalue":{"value":"interactive theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q6166143$3DE6F93E-81AF-4B01-BA84-9C2E38EC4994","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q6166143$8DA631D5-90AF-475C-87EE-349D90C145FA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1a16c8a41f16d5dc2d1d5604b56fd02fca958a9f","datavalue":{"value":"proof general","type":"string"},"datatype":"string"},"type":"statement","id":"Q6166143$6BCA7096-1DE6-4650-8C6F-B44468FF61A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9a7e8c577cabe6c92463745843eed5caf8b82260","datavalue":{"value":"readability of proof scripts","type":"string"},"datatype":"string"},"type":"statement","id":"Q6166143$94D5B67F-3D49-4F11-ABF2-E1D8742BEB1A","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":"Q6166143$B5AE11CF-26EA-4A52-BCD3-7ECBFA9EB7F5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a64c828b6f05b327ad7be56f3fde812b698631dc","datavalue":{"value":"https://doi.org/10.1007/978-3-030-02768-1_9","type":"string"},"datatype":"url"},"type":"statement","id":"Q6166143$134A62B6-D9D0-4AFC-B246-B9B543B580A9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"682b9ba4b3b0993d6680b46b12666eeecbbaae9e","datavalue":{"value":"W2896474834","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6166143$234343E3-7FC4-47A7-AA1F-19777382D425","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"757e822784b4bdc641199b06bea0bf174e7498e6","datavalue":{"value":{"entity-type":"item","numeric-id":832103,"id":"Q832103"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f932065022d8fcd1e601b2e47b94a281945096a","datavalue":{"value":{"amount":"+0.7332786917686462","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":"Q6166143$FF2CB29E-4F30-4B69-9FC8-E3E6B0FDCB6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36843b484ec32d33e3910f12af650c4645363dc1","datavalue":{"value":{"entity-type":"item","numeric-id":4647518,"id":"Q4647518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"62dd330e73d1648f8f6fa7f1a679d0e452271bdb","datavalue":{"value":{"amount":"+0.718878448009491","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":"Q6166143$ED647D2F-659D-4869-8D06-654A2C270265","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d66339c795d505f780406e18e20e0f95f8bd017d","datavalue":{"value":{"entity-type":"item","numeric-id":2729065,"id":"Q2729065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2658fa21c501eb8df05c7f1eec59a33018bffa00","datavalue":{"value":{"amount":"+0.7158554196357727","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":"Q6166143$9B8CAE3B-DC9A-40D0-BDFC-5325B26D0696","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9374931cf68530b34205f633bba9ad4c29b915d8","datavalue":{"value":{"entity-type":"item","numeric-id":2870138,"id":"Q2870138"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2988cd208fb01a4664772398d00384dc757a4732","datavalue":{"value":{"amount":"+0.7091035842895508","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":"Q6166143$25CD7E8C-5F00-4E0A-ABED-F63A8EC04259","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea3f33b6db43d9dd3c4f184c10e76950834e5175","datavalue":{"value":{"entity-type":"item","numeric-id":2829283,"id":"Q2829283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b04b8ecdd19b94d9abcd829f06fdca808a00273a","datavalue":{"value":{"amount":"+0.6823101043701172","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":"Q6166143$30AE2F82-7CDC-4560-99B3-27807C5226F1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6166143","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6166143"}}}}}