论文标题
战术家（扩展版）：COQ的无缝，互动战术学习者和供奉献者
The Tactician (extended version): A Seamless, Interactive Tactic Learner and Prover for Coq
论文作者
论文摘要
我们为COQ证明助手的战术学习者和奉献者介绍了战术师。战术家帮助用户在保留对一般证明策略的控制权的同时做出战术证明决策。为此，战术家从以前书面的战术脚本中学习，并为用户提供有关要执行的下一个战术的建议，或者完全承担了证明综合的负担。战术家的目标是为用户提供无缝，互动和直观的体验，以及强大和适应性的证明自动化。在本文中，我们从用户的角度概述了战术家，关于日常用法和包装依赖管理的问题，同时在整个大型学习时。最后，我们将战术家作为COQ插件和机器学习平台的实现。
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.
