Proof has been formalised into a program
Using the Boyer-Moore theorem prover, Gödel’s theorem has been derived from a basic set of axioms by a computer in basically the same way that Gödel proved it himself.
Natarajan Shankar at (1994), as articulated by Stewart Russell and Peter Norvig (1995).
CONTEXT(Help)
-
Artificial Intelligence »Artificial Intelligence
Are thinking computers mathematically possible? [7] »Are thinking computers mathematically possible? [7]
No: computers are limited by Gödel's theorems »No: computers are limited by Gödel's theorems
Improved machines »Improved machines
The Gödelian insight has already been formalised »The Gödelian insight has already been formalised
Gödelization procedure algorithmically specifiable »Gödelization procedure algorithmically specifiable
Proof has been formalised into a program
Boyer-Moore theorem prover »Boyer-Moore theorem prover
+Comments (0)
+Citations (0)
+About