Automated theorem provers: a practical tool for the working mathematician?

DOI10.1007/s10472-011-9248-8zbMath1237.68177OpenAlexW2025572920MaRDI QIDQ657585

Alan Bundy

Publication date: 10 January 2012

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://www.pure.ed.ac.uk/ws/files/416060/Automated_theorem_provers_a_practical_tool_for_the_working_mathematician.pdf

zbMATH Keywords

automated theorem proving

Mathematics Subject Classification ID

Related Items (3)

A fully automatic theorem prover with human-style output ⋮ Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation ⋮ Computer-aided proof of Erdős discrepancy properties

Uses Software

• MAYA
• Isar
• Mizar
• Flyspeck
• kepler98

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Social processes and proofs of theorems and programs
• Every planar map is four colorable. I: Discharging
• Edinburgh LCF. A mechanized logic of computation
• A proof of the Kepler conjecture
• Abstracts of additional presentations made at the Royal Society Discussion Meeting ‘The nature of mathematical proof’
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Mechanizing Mathematical Reasoning
• A note on the Entscheidungsproblem
• On Computable Numbers, with an Application to the Entscheidungsproblem

This page was built for publication: Automated theorem provers: a practical tool for the working mathematician?