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

DOI10.1007/978-3-030-53518-6_17MaRDI QIDQ2219409zbMATH OpenOpenAlexFDO

Authors Lasse Blaauwbroek, Josef Urban, Herman Geuvers

Publication date 20 January 2021

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

Mathematics Subject Classification ID

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

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.

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

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
• The role of entropy in guiding a connection prover
• Refactoring proofs with Tactician
• 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
• SEPIA: search for proofs using inferred automata
• CoProver: a recommender system for proof construction
• TacticToe: learning to reason with HOL4 tactics

Describes a project that uses

Uses Software

• Tactician
• Coq

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)