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)

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

Describes a project that uses

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)