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