** Next:** Limitations of Gödel Machines
** Up:** Overview / Basic Ideas
** Previous:** Basic Idea of Gödel

Section 5 will present an -optimal
initialization of the proof searcher,
that is, one with an optimal *order* of complexity
(Theorem 5.1). Still, there will remain a lot of
room for self-improvement hidden by the -notation.
The searcher
uses an online extension of *Universal Search*
[24,26]
to systematically test *online
proof techniques*, which are proof-generating programs that
may read parts of state
(similarly, mathematicians are often more interested in
proof techniques than in theorems).
To prove target theorems as above,
proof techniques may invoke special instructions
for generating axioms and applying inference rules to prolong the
current *proof* by theorems. Here
an axiomatic system
encoded in
includes axioms describing **(a)** how any instruction invoked
by a program running on the given hardware will change
the machine's state
(including instruction pointers etc.)
from one step to the next (such that proof techniques can reason
about the effects of any program including the proof searcher),
**(b)** the initial program itself (Section 3 will show
that this is possible without introducing circularity),
**(c)** stochastic environmental properties,
**(d)** the formal utility function ,
e.g., equation (1),
which takes into account
computational costs of all actions including proof search.

** Next:** Limitations of Gödel Machines
** Up:** Overview / Basic Ideas
** Previous:** Basic Idea of Gödel
Juergen Schmidhuber
2005-01-03