Document Open Access Logo

Hammering Mizar by Learning Clause Guidance (Short Paper)

Authors Jan Jakubův, Josef Urban

Thumbnail PDF


  • Filesize: 353 kB
  • 8 pages

Document Identifiers

Author Details

Jan Jakubův
  • Czech Technical University in Prague, Czech Republic
Josef Urban
  • Czech Technical University in Prague, Czech Republic

Cite AsGet BibTex

Jan Jakubův and Josef Urban. Hammering Mizar by Learning Clause Guidance (Short Paper). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 34:1-34:8, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)


We describe a very large improvement of existing hammer-style proof automation over large ITP libraries by combining learning and theorem proving. In particular, we have integrated state-of-the-art machine learners into the E automated theorem prover, and developed methods that allow learning and efficient internal guidance of E over the whole Mizar library. The resulting trained system improves the real-time performance of E on the Mizar library by 70% in a single-strategy setting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Computing methodologies → Theorem proving algorithms
  • Computing methodologies → Machine learning
  • Proof automation
  • ITP hammers
  • Automated theorem proving
  • Machine learning


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail