The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq
Identifikátory výsledku
Kód výsledku v 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>
Výsledek na webu
<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>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
The Tactician - A Seamless, Interactive Tactic Learner and Prover for Coq
Popis výsledku anglicky
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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Návaznosti výsledku
Projekt
<a href="/cs/project/EF15_003%2F0000466" target="_blank" >EF15_003/0000466: Umělá inteligence a uvažování</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2020
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Lecture Notes in Computer Science
ISBN
978-3-030-53517-9
ISSN
0302-9743
e-ISSN
1611-3349
Počet stran výsledku
7
Strana od-do
271-277
Název nakladatele
Springer
Místo vydání
Cham
Místo konání akce
Bertinoro, Forli
Datum konání akce
26. 7. 2020
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—