comments

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).
RELATED ARTICLESExplain
⌅
Artificial Intelligence
⌃
Are thinking computers mathematically possible? [7]
⌃
No: computers are limited by Gödel's theorems
⌃
Improved machines
⌃
The Gödelian insight has already been formalised
⌃
Gödelization procedure algorithmically specifiable
■
Proof has been formalised into a program
↳
Boyer-Moore theorem prover
□
Gödelian insight is a slippery character
□
Graph of this discussion
Enter the title of your article


Enter a short (max 500 characters) summation of your article
Enter the main body of your article
Lock
+Comments (0)
+Citations (0)
+About
Enter comment

Select article text to quote
welcome text

First name   Last name 

Email

Skip