next up previous
Next: Limitations of Gödel Machines Up: Overview / Basic Ideas Previous: Basic Idea of Gödel

Proof Techniques and an $O()$-Optimal Initial Proof Searcher

Section 5 will present an $O()$-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 $O()$-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 $s$ (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 $\cal A$ encoded in $p(1)$ includes axioms describing (a) how any instruction invoked by a program running on the given hardware will change the machine's state $s$ (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 $p(1)$ itself (Section 3 will show that this is possible without introducing circularity), (c) stochastic environmental properties, (d) the formal utility function $u$, e.g., equation (1), which takes into account computational costs of all actions including proof search.


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