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

DOI10.1007/978-3-030-53518-6_17zbMath1455.68242arXiv2008.00120OpenAlexW3043685015MaRDI QIDQ2219409

Josef Urban, Herman Geuvers, Lasse Blaauwbroek

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)

Related Items (4)

Online machine learning techniques for Coq: a comparison ⋮ Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ The role of entropy in guiding a connection prover ⋮ Guiding an automated theorem prover with neural rewriting

Uses Software

• Coq
• Tactician

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