Monte Carlo Tableau Proof Search
Michael Färber, Cezary Kaliszyk, Josef Urban
26th International Conference on Automated Deduction, LNCS 10395, pp. 563-579, 2017.
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.
PDF | doi:10.1007/978-3-319-63046-5_34
@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},
}