Theorem Proving Task
(Redirected from theorem proving task)
Jump to navigation
Jump to search
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
”
- "Provide a mathematical proof for mathematical theorem
- Counter-Example(s):
- 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.