Checking proofs

DOI10.1007/978-94-007-6534-4_9MaRDI QIDQ2950035zbMATH OpenOpenAlexFDO

Authors Jesse Alama, Reinhard Kahle

Publication date 5 October 2015

Published in The Argument of Mathematics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-94-007-6534-4_9

zbMATH Keywords

proofformalizationhuman checkingobivousness

Mathematics Subject Classification ID

Methodology of mathematics (00A35) History of mathematics in the 20th century (01A60) Philosophy of mathematics (00A30) History of mathematics in the 21st century (01A61) History of mathematical logic and foundations (03-03) Mechanization of proofs and logical operations (03B35)

Recommendations

• Some Historical, Philosophical and Methodological Remarks on Proof in Mathematics
• Types for Proofs and Programs
• Formal Proof: Reconciling Correctness and Understanding
• Formal proof -- theory and practice
• Mathematical concepts in computer proofs

Cites work

• scientific article; zbMATH DE number 5850143 (Why is no real title available?)
• scientific article; zbMATH DE number 2127501 (Why is no real title available?)
• scientific article; zbMATH DE number 3141365 (Why is no real title available?)
• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 3521895 (Why is no real title available?)
• scientific article; zbMATH DE number 1215493 (Why is no real title available?)
• scientific article; zbMATH DE number 481931 (Why is no real title available?)
• scientific article; zbMATH DE number 2115087 (Why is no real title available?)
• scientific article; zbMATH DE number 1426640 (Why is no real title available?)
• scientific article; zbMATH DE number 5486212 (Why is no real title available?)
• A Critique of a Formalist-Mechanist Version of the Justification of Arguments in Mathematicians' Proof Practices
• A proof of the Kepler conjecture
• Every planar map is four colorable. II: Reducibility
• Formal proof
• Formal proof - the four color theorem
• Formal proof -- theory and practice
• Intentional gaps in mathematical proofs
• Mathematical method and proof
• Obvious inferences
• Proofs verifying programs and programs producing proofs: a conceptual analysis
• Solution of the Robbins problem
• System for Automated Deduction (SAD): A Tool for Proof Verification
• The Derivation-Indicator View of Mathematical Practice
• The four-colour theorem
• The surveyability of mathematical proof: A historical perspective
• Toward Mechanical Mathematics

Cited in

(7)

• scientific article; zbMATH DE number 2185701 (Why is no real title available?)
• The parallel structure of mathematical reasoning
• On the shape of mathematical arguments
• The Proof Certifier Checkers
• Obvious inferences
• The verification of an inequality
• Formal and Natural Proof: A Phenomenological Approach

Describes a project that uses

Uses Software

• kepler98
• SAD
• Mizar

This page was built for publication: Checking proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2950035)