The Tactician. A seamless, interactive tactic learner and prover for Coq

DOI10.1007/978-3-030-53518-6_17zbMATH Open1455.68242arXiv2008.00120OpenAlexW3043685015MaRDI QIDQ2219409FDOQ2219409

Authors: Lasse Blaauwbroek, Josef Urban, Herman Geuvers 

Publication date: 20 January 2021

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.

Full work available at URL: https://arxiv.org/abs/2008.00120

Recommendations

• Online machine learning techniques for Coq: a comparison
• TacticToe: learning to reason with HOL4 tactics
• Refactoring proofs with Tactician
• scientific article; zbMATH DE number 1696760
• Mtac: a monad for typed tactic programming in Coq

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited In (11)

• Guiding an automated theorem prover with neural rewriting
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
• Online machine learning techniques for Coq: a comparison
• Refactoring proofs with Tactician
• The role of entropy in guiding a connection prover
• A Coq tactic for equality learning in linear arithmetic
• Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
• Learning Proof Transformations and Its Applications in Interactive Theorem Proving
• CoProver: a recommender system for proof construction
• SEPIA: search for proofs using inferred automata
• TacticToe: learning to reason with HOL4 tactics

Uses Software

• Coq
• Tactician

This page was built for publication: The Tactician. A seamless, interactive tactic learner and prover for Coq

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2219409)