Monte Carlo Tableau Proof Search

November 18, 2016 · The Ethereal · 🏛 CADE

🔮 THE ETHEREAL: The Ethereal
Pure theory — exists on a plane beyond code

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Michael Färber, Cezary Kaliszyk, Josef Urban arXiv ID 1611.05990 Category cs.LO: Logic in CS Cross-listed cs.AI, cs.LG Citations 15 Venue CADE Last Checked 6 months ago
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.
Community shame:
Not yet rated
📄 View on arXiv 🌐 View on ar5iv 📑 PDF 🎉 Report Code Found
Community Contributions

Found the code? Know the venue? Think something is wrong? Let us know!

📜 Similar Papers

In the same crypt — Logic in CS