The Tactician. A seamless, interactive tactic learner and prover for Coq
From MaRDI portal
Publication:2219409
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
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
This page was built for publication: The Tactician. A seamless, interactive tactic learner and prover for Coq