2020/07/31 by Lasse Blaauwbroek, Josef Urban, Herman Geuvers · 1 citation
Computer Science · #cs.AI #cs.LO #msc:68T27 #acm:68T27
paper · pdf · doi:10.1007/978-3-030-53518-6_17
published as In CICM. volume 12236 of Lecture Notes in Computer Science, pages 271-277. Springer, 2020 · 19 pages, 2 figures. This is an extended version of a paper published in CICM-2020. For the project website, see https://coq-tactician.github.io
arxiv created 2020/07/31 · arxiv updated 2020/08/04
We present Tactician, a tactic learner and prover for the Coq Proof Assistant. Tactician helps users make tactical proof decisions while they retain control over the general proof strategy. To this end, Tactician learns from previously written tactic scripts and gives users either suggestions about the next tactic to be executed or altogether takes over the burden of proof synthesis. Tactician's goal is to provide users with a seamless, interactive, and intuitive experience together with robust and adaptive proof automation. In this paper, we give an overview of Tactician from the user's point of view, regarding both day-to-day usage and issues of package dependency management while learning in the large. Finally, we give a peek into Tactician's implementation as a Coq plugin and machine learning platform.