Incompleteness, Undecidability and Automated Proofs

DOI10.1007/978-3-319-45641-6_10zbMATH Open1453.03066OpenAlexW2508333642MaRDI QIDQ2829997FDOQ2829997

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

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

Mathematics Subject Classification ID

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

Cites Work

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

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

Uses Software

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

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)