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