** Next:** Are Humans Probabilistic Gödel
** Up:** Discussion
** Previous:** Gödel Machine vs AIXI

##

Practical Issues

We believe that Gödel machines should be built.
Some people may be sceptical about the practicality of
systematic proof technique testers as components
of general problem solvers.
But until a short while ago some people were also
sceptical about the feasibility of universal
program search methods.
Recent work [38,40],
however, already has shown that certain general methods
can indeed offer certain practical advantages over traditional
planning systems and reinforcement learners.

The well-developed field of automated theorem proving
provides a rich set of alternatives for the initial
Gödel machine set-up. Practical issues include:

- Identify a particularly convenient hardware,
presumably not based on Turing machines,
but perhaps on recurrent neural network-like parallel
systems, possibly emulated by
software for a traditional personal computer.

- Identify a particularly convenient formal language
for describing the initial axioms and the set
of possible proofs. For efficiency reasons this language
should include a calculus for shortcuts and variables
like the one informally used by mathematicians,
who rarely use truly formal
argumentation. Their papers not only abound with sentences
like
*`It is easy to see ...'*;
they almost always also use informal sentences
such as *`Let denote a function ...'*
before they reuse the symbol in more formal
statements.
To facilitate a mimicry of elegant human proof techniques,
the theorem-proving calculus should fully formalize
temporary bindings of symbols traditionally
introduced through English text
to symbols occurring in theorem sequences.

- Identify a natural
set of instructions for the programming language
used by the initial proof searcher to construct
proof techniques that calculate proofs--compare
Section 2.2.1.

- Identify potentially useful high-level theorems about
the initial proof searcher's behavior and
performance, to be added to the initial
axioms, such that the proof searcher's initial
task is facilitated because
it does not have to prove these theorems from scratch.

** Next:** Are Humans Probabilistic Gödel
** Up:** Discussion
** Previous:** Gödel Machine vs AIXI
Juergen Schmidhuber
2003-09-29

Back to Goedel machine home page