Monte Carlo tableau proof search

DOI10.1007/978-3-319-63046-5_34zbMath1494.68286arXiv1611.05990OpenAlexW3103335455WikidataQ108482129 ScholiaQ108482129MaRDI QIDQ2405274

Josef Urban, Cezary Kaliszyk, Michael Färber

Publication date: 22 September 2017

Full work available at URL: https://arxiv.org/abs/1611.05990

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

Vampire with a brain is a good ITP hammer ⋮ \textsf{lazyCoP}: lazy paramodulation meets neurally guided search ⋮ Hammering Mizar by Learning Clause Guidance (Short Paper). ⋮ Machine learning guidance for connection tableaux ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)

Uses Software

• Mizar
• Satallax
• MaLeCoP
• CVC4
• leanCoP
• ileanCoP
• E Theorem Prover
• LeoPARD
• FEMaLeCoP
• nanoCoP

This page was built for publication: Monte Carlo tableau proof search