Monte Carlo Tableau Proof Search
Logic in Computer Science
2019-06-18 v2 Artificial Intelligence
Machine Learning
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
@article{arxiv.1611.05990,
title = {Monte Carlo Tableau Proof Search},
author = {Michael Färber and Cezary Kaliszyk and Josef Urban},
journal= {arXiv preprint arXiv:1611.05990},
year = {2019}
}