Monte Carlo Tableau Proof Search

By Michael Färber, Cezary Kaliszyk, Josef Urban. 2016

15 citations recorded by the source corpus.

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.

Subfields: Automated Theorem Proving & Formal Methods

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

1. Cezary Kaliszyk
2. Henryk Michalewski
3. Josef Urban
4. M. Olsák
5. Kaiyu Yang
6. Jia Deng
7. Mingzhe Wang
8. Kshitij Bansal

Citations in the corpus

• Reinforcement Learning of Theorem Proving (2018, methodology): “This has been done in the connection tableau setting [48, 20, 10], saturation style setting [16, 30], and also as direct automation inside interactive theorem provers [12, 14, 49].”