Automated theorem provers: a practical tool for the working mathematician?
From MaRDI portal
The author lists some reasons which in his opinion form obstacles for using automated theorem provers by mathematicians and speculates on potential applications of the related work of his group.
Recommendations
Cites work
- A note on the Entscheidungsproblem
- A proof of the Kepler conjecture
- Abstracts of additional presentations made at the Royal Society Discussion Meeting ‘The nature of mathematical proof’
- Ascertaining mathematical theorems
- Edinburgh LCF. A mechanized logic of computation
- Every planar map is four colorable. I: Discharging
- Formal proof
- Formal proof - the four color theorem
- Hiproofs: a hierarchical notion of proof tree
- scientific article; zbMATH DE number 1645815 (Why is no real title available?)
- scientific article; zbMATH DE number 2127501 (Why is no real title available?)
- scientific article; zbMATH DE number 3758571 (Why is no real title available?)
- scientific article; zbMATH DE number 1342253 (Why is no real title available?)
- scientific article; zbMATH DE number 1421054 (Why is no real title available?)
- Mechanizing Mathematical Reasoning
- On Computable Numbers, with an Application to the Entscheidungsproblem
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- Social processes and proofs of theorems and programs
Cited in
(19)- Automated theorem proving in mathematics.
- Automated deduction in equational logic and cubic curves
- A fully automatic theorem prover with human-style output
- Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation
- Ascertaining mathematical theorems
- Challenging theorem provers with Mathematical Olympiad problems in solid geometry
- scientific article; zbMATH DE number 3881901 (Why is no real title available?)
- Some considerations on the usability of interactive provers
- scientific article; zbMATH DE number 3938594 (Why is no real title available?)
- scientific article; zbMATH DE number 1100750 (Why is no real title available?)
- scientific article; zbMATH DE number 1951639 (Why is no real title available?)
- scientific article; zbMATH DE number 4119665 (Why is no real title available?)
- scientific article; zbMATH DE number 2090294 (Why is no real title available?)
- Foreword to: Special issue on interactive theorem provers
- Machine-assisted proofs
- Building a library of mechanized mathematical proofs: Why do it? And what is it like to do?
- Finding mathematical proofs using computers
- Computer theorem proving in mathematics
- Computer-aided proof of Erdős discrepancy properties
This page was built for publication: Automated theorem provers: a practical tool for the working mathematician?
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q657585)
