Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
From MaRDI portal
Publication:2908509
DOI10.1007/978-3-642-31365-3_30zbMath1358.68259OpenAlexW2097437276MaRDI QIDQ2908509
Daniel Kühlwein, Twan van Laarhoven, Tom Heskes, Josef Urban, Evgeni Tsivtsivadze
Publication date: 5 September 2012
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-31365-3_30
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (12)
MizAR 40 for Mizar 40 ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Hammer for Coq: automation for dependent type theory ⋮ Learning to Parse on Aligned Corpora (Rough Diamond) ⋮ Recycling proof patterns in Coq: case studies ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ The CADE-27 Automated theorem proving System Competition – CASC-27 ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ Machine learning guidance for connection tableaux ⋮ Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving ⋮ ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\) ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Uses Software
This page was built for publication: Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics
