| ||||
| ||||
![]() Title:The Isabelle ENIGMA Authors:Zarathustra Goertzel, Jan Jakubův, Cezary Kaliszyk, Miroslav Olšák, Jelle Piepenbrock and Josef Urban Conference:ITP 2022 Tags:Automated Theorem Proving, Interactive Theorem Proving, Isabelle Sledgehammer, Machine Learning and Premise Selection Abstract: We significantly improve the performance of the E automated theorem prover on the Isabelle Sledgehammer problems by combining learning and theorem proving in several ways. In particular, we develop targeted versions of the ENIGMA guidance for the typed Isabelle problems, targeted versions of neural premise selection, and targeted strategies for E. The methods are trained in several iterations over hundreds of thousands untyped and typed first-order problems extracted from Isabelle, leading to a large improvement of the automation both in the typed and untyped setting. The Isabelle ENIGMA ![]() The Isabelle ENIGMA | ||||
Copyright © 2002 – 2025 EasyChair |