{"entities":{"Q2219409":{"pageid":2230152,"ns":120,"title":"Item:Q2219409","lastrevid":57785619,"modified":"2026-04-02T12:50:01Z","type":"item","id":"Q2219409","labels":{"en":{"language":"en","value":"The Tactician. A seamless, interactive tactic learner and prover for Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7298569"}},"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":"Q2219409$F17C5FBD-3B6F-4E04-A360-574EFB8F0B81","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"913efa52d3efff057ed1f9f8b4e8288f0dc8ab41","datavalue":{"value":{"text":"The Tactician. A seamless, interactive tactic learner and prover for Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2219409$AB587FD7-3167-4FA4-B194-5BF6682EA929","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5ada9b2032d12368b95924e840d2f414676a1009","datavalue":{"value":"1455.68242","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219409$5F237B66-A0D8-400F-8179-5983566DEE55","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"6a00f91004fe499b81cbbf5437aff8271c8e6cdb","datavalue":{"value":"10.1007/978-3-030-53518-6_17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219409$86B0EFB2-3C65-47F6-A768-E6A530746E83","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a2a10f8493b6d512bfd4eade8423906525f6e138","datavalue":{"value":{"entity-type":"item","numeric-id":2128795,"id":"Q2128795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219409$AE303E39-B8DC-45ED-8891-5373C21F8A44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc204e2e78d924e815f2b640ec35c8c2356ad41f","datavalue":{"value":{"entity-type":"item","numeric-id":286786,"id":"Q286786"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219409$551BDA4D-3712-4F02-A42F-38643705028E","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":"Q2219409$9E7800E1-1D11-4B91-A42F-CD74DA95D888","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"233394734482eba32ed4ee15da745b1ac2b96149","datavalue":{"value":{"time":"+2021-01-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2219409$B4BA1D36-C430-4E12-A729-806F03EEC270","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"96aaa1fc7a2b716adda6551fbfb7d50fab7b94f2","datavalue":{"value":"https://arxiv.org/abs/2008.00120","type":"string"},"datatype":"url"},"type":"statement","id":"Q2219409$3D23EBD8-4C29-4B43-8929-5D5FE30B7627","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219409$B808BA7D-4AAF-4018-BC58-52D4317C7D15","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"8e6e1c029041244dee5585e56d903bccc4ca8c26","datavalue":{"value":"7298569","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219409$CB536749-6E28-4D48-A94A-27A0BEB2EF25","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":"Q2219409$085B60DB-ADE3-4C95-8DEC-C2B687A10B13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"62ba86aa6537435eabbaebc8bfe3b9fc42cedbd1","datavalue":{"value":{"entity-type":"item","numeric-id":29448,"id":"Q29448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2219409$C0E13A31-F742-4481-A27E-DAD79110ED79","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":"Q2219409$67736709-6227-49F6-8E3F-CECFC3BB5C3C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"b76e7843f4a57a2c1341ab8851f28a071aabd7dc","datavalue":{"value":"W3043685015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2219409$F775FF6A-3B54-4B82-9856-12D8AC8B9AE6","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b482b16f846194e34941107c6f31674d852f3878","datavalue":{"value":{"entity-type":"item","numeric-id":2128797,"id":"Q2128797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"64535ecce6e567e911a673393ae31455a9b38373","datavalue":{"value":{"amount":"+0.7928164005279541","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":"Q2219409$8FBBD770-AF2E-4FA3-9B21-EF312833C7E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80a02b86f5e7c12a000ea62837c3061ae5ebea26","datavalue":{"value":{"entity-type":"item","numeric-id":4645730,"id":"Q4645730"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9986f6d6c06c3c156be9839af0b5e1fa239db34b","datavalue":{"value":{"amount":"+0.787169337272644","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":"Q2219409$BCB386A9-139B-409B-8DB4-F444693F88D9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0c714f87690a89e1a13166cf2d658c3024e8cde0","datavalue":{"value":{"entity-type":"item","numeric-id":4988643,"id":"Q4988643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce9cd212d47030c9b0964f05570172d7d701a6f3","datavalue":{"value":{"amount":"+0.7771928310394287","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":"Q2219409$E69C2FB0-82DD-4CC2-983B-A40B34990B0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ca320f3d91c0d7a8bb4f611412474fdb2e1c5024","datavalue":{"value":{"entity-type":"item","numeric-id":2767010,"id":"Q2767010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c6c989df7b945dd6d947e4b27a18954edac987cf","datavalue":{"value":{"amount":"+0.7604237198829651","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":"Q2219409$36DEB998-BB8E-4537-8F9D-0AC1AF9BE1AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b3e572badf5bee00e7427a40b4cef297ea325698","datavalue":{"value":{"entity-type":"item","numeric-id":5244791,"id":"Q5244791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"34f019a120c5ae4fd75ffea0c9abf2a36ea406f5","datavalue":{"value":{"amount":"+0.7584680914878845","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":"Q2219409$60DF4AC6-1B21-4860-8F58-4EA2E684C19D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2219409","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2219409"}}}}}