Theorem Proving Task

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

• Context:
  • It can be solved by a Theorem Proving System (that implements a theorem proving algorithm).
• Example(s):
  • "Provide a mathematical proof for mathematical theorem M”
• Counter-Example(s):
  • Software Programming.
• See: Automated Theorem Proving, Inference Task, Automated Reasoning.

---

---

References

2017

• (Wikipedia, 2017) ⇒ https://en.wikipedia.org/wiki/Automated_theorem_proving Retrieved:2017-3-2.
  • Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

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.

---