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

DOI10.1007/S10472-011-9248-8zbMATH Open1237.68177OpenAlexW2025572920MaRDI QIDQ657585FDOQ657585

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

Recommendations

• Computer theorem proving in mathematics
• scientific article; zbMATH DE number 4119665
• Formal proof -- theory and practice
• scientific article; zbMATH DE number 3880145
• Automated theorem proving in mathematics.

zbMATH Keywords

automated theorem proving

Mathematics Subject Classification ID

Cites Work

• Mechanizing Mathematical Reasoning
• Edinburgh LCF. A mechanized logic of computation
• A proof of the Kepler conjecture
• Every planar map is four colorable. I: Discharging
• A note on the Entscheidungsproblem
• On Computable Numbers, with an Application to the Entscheidungsproblem
• Formal proof - the four color theorem
• Title not available (Why is that?)
• Title not available (Why is that?)
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Formal proof
• Title not available (Why is that?)
• Hiproofs: a hierarchical notion of proof tree
• Social processes and proofs of theorems and programs
• Ascertaining mathematical theorems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Abstracts of additional presentations made at the Royal Society Discussion Meeting ‘The nature of mathematical proof’

Cited In (10)

• Title not available (Why is that?)
• Lakatos-style collaborative mathematics through dialectical, structured and abstract argumentation
• A fully automatic theorem prover with human-style output
• Title not available (Why is that?)
• Computer theorem proving in mathematics
• Title not available (Why is that?)
• Title not available (Why is that?)
• Automated deduction in equational logic and cubic curves
• Computer-aided proof of Erdős discrepancy properties
• Title not available (Why is that?)

Uses Software

• MAYA
• Isar
• Mizar
• Flyspeck
• kepler98

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)