The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F20%3A00346102" target="_blank" >RIV/68407700:21730/20:00346102 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1007/978-3-030-53518-6_17" target="_blank" >https://doi.org/10.1007/978-3-030-53518-6_17</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-030-53518-6_17" target="_blank" >10.1007/978-3-030-53518-6_17</a>

Result language
angličtina
Original language name
The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq
Original language description
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.
Czech name
—
Czech description
—

Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project
<a href="/en/project/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Artificial Intelligence and Reasoning</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2020
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)