Monte carlo tableau proof search

Popis výsledku

—

Jazyk výsledku
angličtina
Název v původním jazyce
Monte carlo tableau proof search
Popis výsledku v původním jazyce
We study Monte Carlo Tree Search to guide proof search in tableau calculi. This includes proposing a number of proof-state evaluation heuristics, some of which are learnt from previous proofs. We present an implementation based on the leanCoP prover. The system is trained and evaluated on a large suite of related problems coming from the Mizar proof assistant, showing that it is capable to find new and different proofs.
Název v anglickém jazyce
Monte carlo tableau proof search
Popis výsledku anglicky
We study Monte Carlo Tree Search to guide proof search in tableau calculi. This includes proposing a number of proof-state evaluation heuristics, some of which are learnt from previous proofs. We present an implementation based on the leanCoP prover. The system is trained and evaluated on a large suite of related problems coming from the Mizar proof assistant, showing that it is capable to find new and different proofs.

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)

Rok uplatnění
2017
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ů

Název statě ve sborníku
CADE 26 - 26th International Conference on Automated Deduction
ISBN
978-3-319-63045-8
ISSN
0302-9743
e-ISSN
—
Počet stran výsledku
17
Strana od-do
563-579
Název nakladatele
Springer
Místo vydání
Basel
Místo konání akce
Gothenburg
Datum konání akce
6. 8. 2017
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—

Druh výsledku

D - Stať ve sborníku

OECD FORD

Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Rok uplatnění

2017