zbMATH — the first resource for mathematics

Monte Carlo tableau proof search. (English) Zbl 06778426
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].

03B35 Mechanization of proofs and logical operations
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI