Formal Proof: Reconciling Correctness and Understanding

DOI10.1007/978-3-642-02614-0_20MaRDI QIDQ3637280zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Christine Müller, Cristian S. Calude

Publication date 9 July 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02614-0_20

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Proof and Understanding in Mathematical Practice
• Formalisation vs. understanding. A case study in Isabelle
• Types for Proofs and Programs
• scientific article; zbMATH DE number 1302064
• Proving and programming

Cites work

• A model of set-theory in which every set of reals is Lebesgue measurable
• Analogy in inductive theorem proving
• Bounded model generation for Isabelle/HOL
• Despite physicists, proof is essential in mathematics
• Diagrammatic Representation and Inference
• Every computably enumerable random real is provably computably enumerable random
• EXACT APPROXIMATIONS OF OMEGA NUMBERS
• Formal proof
• Formal proof - the four color theorem
• Formal proof -- theory and practice
• scientific article; zbMATH DE number 1629953 (Why is no real title available?)
• scientific article; zbMATH DE number 5604130 (Why is no real title available?)
• scientific article; zbMATH DE number 4002093 (Why is no real title available?)
• scientific article; zbMATH DE number 193258 (Why is no real title available?)
• scientific article; zbMATH DE number 1973375 (Why is no real title available?)
• scientific article; zbMATH DE number 1980938 (Why is no real title available?)
• scientific article; zbMATH DE number 2154400 (Why is no real title available?)
• scientific article; zbMATH DE number 1868661 (Why is no real title available?)
• scientific article; zbMATH DE number 1911266 (Why is no real title available?)
• scientific article; zbMATH DE number 1418478 (Why is no real title available?)
• scientific article; zbMATH DE number 5486212 (Why is no real title available?)
• scientific article; zbMATH DE number 5219792 (Why is no real title available?)
• scientific article; zbMATH DE number 3280051 (Why is no real title available?)
• scientific article; zbMATH DE number 3289430 (Why is no real title available?)
• Intelligent computer mathematics. 9th international conference, AISC 2008, 15th symposium, Calculemus 2008, 7th international conference, MKM 2008, Birmingham, UK, July 28--August 1, 2008. Proceedings
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Mathematical Knowledge Management
• Organization, transformation, and propagation of mathematical knowledge in mega
• Realization is universal
• Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems
• Theory Is Forever

Cited in

(11)

• Proof assistants: history, ideas and future
• Proof versus formalization
• Formality works
• Incompleteness, Undecidability and Automated Proofs
• Understanding, formal verification, and the philosophy of mathematics
• Formalisation vs. understanding. A case study in Isabelle
• Checking proofs
• scientific article; zbMATH DE number 1302064 (Why is no real title available?)
• Types for Proofs and Programs
• Mathematical Knowledge Management
• Formal and Natural Proof: A Phenomenological Approach

Describes a project that uses

Uses Software

• Archive of Formal Proofs
• OMDoc
• Proof General
• Coq
• Isar
• SPARQL

This page was built for publication: Formal Proof: Reconciling Correctness and Understanding

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