Monte Carlo Tableau Proof Search
This work addresses proof search in automated theorem proving, specifically for tableau calculi, and is incremental as it builds on existing methods like leanCoP with new heuristics.
The paper tackled the problem of guiding proof search in tableau calculi by applying Monte Carlo Tree Search with novel heuristics, including some learned from previous proofs, and demonstrated its capability by finding new and different proofs on a large suite of Mizar problems.
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.