Formal Proof: Reconciling Correctness and Understanding
From MaRDI portal
Publication:3637280
DOI10.1007/978-3-642-02614-0_20zbMath1247.03017DBLPconf/mkm/CaludeM09OpenAlexW1575371466WikidataQ57001574 ScholiaQ57001574MaRDI QIDQ3637280
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
Related Items (2)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Organization, transformation, and propagation of mathematical knowledge in \(\Omega \)mega
- 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
- Analogy in inductive theorem proving
- Despite physicists, proof is essential in mathematics
- A model of set-theory in which every set of reals is Lebesgue measurable
- Every computably enumerable random real is provably computably enumerable random
- EXACT APPROXIMATIONS OF OMEGA NUMBERS
- Supporting User-Defined Notations When Integrating Scientific Text-Editors with Proof Assistance Systems
- Realization is universal
- Diagrammatic Representation and Inference
- Theory Is Forever
- Mathematical Knowledge Management
This page was built for publication: Formal Proof: Reconciling Correctness and Understanding
