We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:


Current browse context:


Change to browse by:

References & Citations

DBLP - CS Bibliography


(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Artificial Intelligence

Title: The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq

Abstract: 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.
Comments: 19 pages, 2 figures. This is an extended version of a paper published in CICM-2020. For the project website, see this https URL
Subjects: Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO)
MSC classes: 68T27
ACM classes: F.4.1
Journal reference: In CICM. volume 12236 of Lecture Notes in Computer Science, pages 271-277. Springer, 2020
DOI: 10.1007/978-3-030-53518-6_17
Cite as: arXiv:2008.00120 [cs.AI]
  (or arXiv:2008.00120v1 [cs.AI] for this version)

Submission history

From: Lasse Blaauwbroek [view email]
[v1] Fri, 31 Jul 2020 23:47:29 GMT (35kb,D)

Link back to: arXiv, form interface, contact.