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.
This work was supported by the European Regional Development Fund under the project AI&Reasoning (reg. no. CZ.02.1.01/0.0/0.0/15_003/0000466) and by the AI4REASON ERC Consolidator grant nr. 649043.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Blaauwbroek, L., Urban, J., Geuvers, H.: Tactic learning and proving for the Coq proof assistant. In: LPAR23. EPiC Series in Computing, vol. 73, pp. 138–150. EasyChair (2020)
Coq Development Team: Coq package index. https://coq.inria.fr/opam/www
Coq Development Team: The Coq proof assistant, version 8.11.0, October 2019
Czajka, L., Kaliszyk, C.: Hammer for Coq: automation for dependent type theory. J. Aut. Reasoning 61(1–4), 423–453 (2018)
Gauthier, T., Kaliszyk, C., Urban, J.: TacticToe: Learning to reason with HOL4 tactics. In: LPAR. EPiC Series in Computing, vol. 46, pp. 125–143. EasyChair (2017)
Gransden, T., Walkinshaw, N., Raman, R.: SEPIA: search for proofs using inferred automata. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 246–255. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21401-6_16
Huang, D., Dhariwal, P., Song, D., Sutskever, I.: Gamepad: a learning environment for theorem proving. In: ICLR (Poster). OpenReview.net (2019)
Komendantskaya, E., Heras, J., Grov, G.: Machine learning in proof general: interfacing interfaces. UITP. EPTCS 118, 15–41 (2012)
Paulin-Mohring, C.: Inductive definitions in the system Coq rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 328–345. Springer, Heidelberg (1993). https://doi.org/10.1007/BFb0037116
Sanchez-Stern, A., Alhessi, Y., Saul, L.K., Lerner, S.: Generating correctness proofs with neural networks. In: arXiv/CoRR. abs/1907.07794 (2019)
Yang, K., Deng, J.: Learning to prove theorems via interacting with proof assistants. In: ICML, Proceedings of Machine Learning Research, vol. 97, pp. 6984–6994 (2019)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Blaauwbroek, L., Urban, J., Geuvers, H. (2020). The Tactician. In: Benzmüller, C., Miller, B. (eds) Intelligent Computer Mathematics. CICM 2020. Lecture Notes in Computer Science(), vol 12236. Springer, Cham. https://doi.org/10.1007/978-3-030-53518-6_17
Download citation
DOI: https://doi.org/10.1007/978-3-030-53518-6_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-53517-9
Online ISBN: 978-3-030-53518-6
eBook Packages: Computer ScienceComputer Science (R0)