The Four Colour Theorem: Engineering of a Formal Proof
From MaRDI portal
Publication:3598006
DOI10.1007/978-3-540-87827-8_28zbMath1166.68346OpenAlexW1503170941MaRDI QIDQ3598006
Publication date: 29 January 2009
Published in: Computer Mathematics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-87827-8_28
Related Items
How Hard Is Positive Quantification?, A proof system for graph (non)-isomorphism verification, A fully automatic theorem prover with human-style output, Tests and proofs for custom data generators, Proof checking and logic programming, Formalizing Physics: Automation, Presentation and Foundation Issues, A Brief Overview of Agda – A Functional Language with Dependent Types, Computational logic: its origins and applications, Hammer for Coq: automation for dependent type theory, Proof-Producing Reflection for HOL, Working with Mathematical Structures in Type Theory, Formalising Mathematics in Simple Type Theory, What is the point of computers? A question for pure mathematicians, Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project, Unnamed Item, Pure Pointer Programs with Iteration, Applications of real number theorem proving in PVS, A Compiled Implementation of Normalization by Evaluation, Incorporating quotation and evaluation into Church's type theory, Pollack-inconsistency, Proof Checking and Logic Programming, Towards Formal Proof Script Refactoring, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, Constructive Mathematics and Functional Programming (Abstract), Tests and Proofs for Enumerative Combinatorics, Proof Auditing Formalised Mathematics, Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
Uses Software
