Abstract

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.

BibTeX

@inproceedings{mfckju-cade17,
 author    = {Michael F{\"{a}}rber and
              Cezary Kaliszyk and
              Josef Urban},
 title     = {Monte Carlo Tableau Proof Search},
 booktitle = {26th International Conference on Automated Deduction
(CADE 2017)},
 pages     = {563--579},
 year      = {2017},
 url       = {https://doi.org/10.1007/978-3-319-63046-5_34},
 doi       = {10.1007/978-3-319-63046-5_34},
 editor    = {Leonardo de Moura},
 series    = {LNCS},
 volume    = {10395},
 publisher = {Springer},
}