Abstract
ENIGMA is an efficient implementation of learning-based guidance for given clause selection in saturation-based automated theorem provers. In this work, we describe several additions to this method. This includes better clause features, adding conjecture features as the proof state characterization, better data pre-processing, and repeated model learning. The enhanced ENIGMA is evaluated on the MPTP2078 dataset, showing significant improvements.
Cite
CITATION STYLE
Jakubův, J., & Urban, J. (2018). Enhancing ENIGMA given clause guidance. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11006 LNAI, pp. 118–124). Springer Verlag. https://doi.org/10.1007/978-3-319-96812-4_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
