Incompleteness, Undecidability and Automated Proofs

DOI10.1007/978-3-319-45641-6_10zbMath1453.03066OpenAlexW2508333642MaRDI QIDQ2829997

Declan Thompson, Cristian S. Calude

Publication date: 9 November 2016

Published in: Computer Algebra in Scientific Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-45641-6_10

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Gödel numberings and issues of incompleteness (03F40)

Uses Software

• Coq
• Isabelle
• HOL
• Matita
• LCF
• ALF
• Flyspeck
• kepler98
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Theories of computational complexity
• A proof of the Kepler conjecture
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• The Erdős discrepancy problem
• Formalizing Turing Machines
• Formalisation vs. Understanding
• Mechanised Computability Theory
• A SAT Attack on the Erdős Discrepancy Conjecture
• Every computably enumerable random real is provably computably enumerable random
• Are There Absolutely Unsolvable Problems? Godel's Dichotomy
• Formal Proof: Reconciling Correctness and Understanding
• Mechanising Turing Machines and Computability Theory in Isabelle/HOL

This page was built for publication: Incompleteness, Undecidability and Automated Proofs