Färber, Michael; Kaliszyk, Cezary; Urban, Josef Monte Carlo tableau proof search. (English) Zbl 1494.68286 de Moura, Leonardo (ed.), Automated deduction – CADE 26. 26th international conference on automated deduction, Gothenburg, Sweden, August 6–11, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10395, 563-579 (2017). Summary: 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.For the entire collection see [Zbl 1369.68037]. Cited in 5 Documents MSC: 68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) 68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) Software:Mizar; Satallax; CVC4; ileanCoP; leanCoP; E Theorem Prover; LeoPARD; MaLeCoP; FEMaLeCoP; nanoCoP PDF BibTeX XML Cite \textit{M. Färber} et al., Lect. Notes Comput. Sci. 10395, 563--579 (2017; Zbl 1494.68286) Full Text: DOI arXiv OpenURL