Theorem Proving Task

From GM-RKB
Jump to navigation Jump to search

A Theorem Proving Task is a task that requires a formal proof.



References

2017

2016

  • (Alemi et al., 2016) ⇒ Alexander A. Alemi, François Chollet, Geoffrey Irving, Christian Szegedy, and Josef Urban. (2016). “DeepMath-Deep Sequence Models for Premise Selection.” arXiv preprint arXiv:1606.04442
    • ABSTRACT: We study the effectiveness of neural sequence models for premise selection in automated theorem proving, one of the main bottlenecks in the formalization of mathematics. We propose a two stage approach for this task that yields good results for the premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing state-of-the-art models. To our knowledge, this is the first time deep learning has been applied to theorem proving.