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.
Cite
CITATION STYLE
Färber, M., Kaliszyk, C., & Urban, J. (2017). Monte carlo tableau proof search. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10395 LNAI, pp. 563–579). Springer Verlag. https://doi.org/10.1007/978-3-319-63046-5_34
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
