1971 ⟶ Work Begins on the Boyer-Moore Theorem Prover
Work on the Boyer-Moore theorem prover started in Edinburgh.
Year
1931
1971
♾️ Gödel Proves Limits of Algorithmic Theorem Proving
Kurt Gödel encoded mathematical statements and proofs as integers, and showed that there are true theorems that are unprovable by any consistent theorem-proving machine. Thus "he identified fundamental limits of algorithmic theorem proving, computing, and any type of computation-based AI," laying foundations of Theoretical computer science and AI theory.⟶
Gödel's incompleteness theoremsMathematicsLogicComputabilityTheorem provingLimits of computationTheoretical computer scienceFoundations
Austria
