Incompleteness, Undecidability and Automated Proofs

DOI10.1007/978-3-319-45641-6_10MaRDI QIDQ2829997zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Undecidability and intuitionistic incompleteness
• Undecidability, incompleteness and Arnol'd problems
• Complexity of propositional proofs (invited talk)
• Automated proofs of Löb's theorem and Gödel's two incompleteness theorems
• An automatic proof of Gödel's incompleteness theorem
• scientific article; zbMATH DE number 1354098
• Remarks on undecidability, incompleteness and the integrability problem
• On the incompleteness theorems
• The undecidability of k-provability
• Undecidability and incompleteness results in automata theory

Cites work

• scientific article; zbMATH DE number 5604130 (Why is no real title available?)
• scientific article; zbMATH DE number 4091484 (Why is no real title available?)
• scientific article; zbMATH DE number 1955470 (Why is no real title available?)
• scientific article; zbMATH DE number 3280051 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• A SAT attack on the Erdős discrepancy conjecture
• A proof of the Kepler conjecture
• Are There Absolutely Unsolvable Problems? Godel's Dichotomy
• Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers
• Every computably enumerable random real is provably computably enumerable random
• Formal Proof: Reconciling Correctness and Understanding
• Formalisation vs. understanding. A case study in Isabelle
• Formalizing Turing Machines
• Mechanised computability theory
• Mechanising Turing machines and computability theory in Isabelle/HOL
• Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
• The Erdös discrepancy problem
• Theories of computational complexity
• Verificationism then and now

Cited in

(2)

• Formalisation vs. understanding. A case study in Isabelle
• Invited Talk: On a (Quite) Universal Theorem Proving Approach and Its Application in Metaphysics

Describes a project that uses

Uses Software

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

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

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