Incompleteness, Undecidability and Automated Proofs

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

Cristian S. Calude, Declan Thompson

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)

Cites Work

• A proof of the Kepler conjecture
• The Erdös discrepancy problem
• Formalizing Turing Machines
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (1)

• 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

Recommendations

• Title not available (Why is that?) 👍 👎
• Undecidability and intuitionistic incompleteness 👍 👎
• On the incompleteness theorems 👍 👎
• Remarks on undecidability, incompleteness and the integrability problem 👍 👎
• The undecidability of \(k\)-provability 👍 👎
• Automated proofs of Löb's theorem and Gödel's two incompleteness theorems 👍 👎
• Complexity of Propositional Proofs 👍 👎
• Undecidability, incompleteness and Arnol'd problems 👍 👎
• An automatic proof of Gödel's incompleteness theorem 👍 👎
• Undecidability and incompleteness results in automata theory 👍 👎

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)