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.
Cite
CITATION STYLE
Blaauwbroek, L., Urban, J., & Geuvers, H. (2020). The tactician: A seamless, interactive tactic learner and prover for coq. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12236 LNAI, pp. 271–277). Springer. https://doi.org/10.1007/978-3-030-53518-6_17
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
