Formal Details of a Particular Gödel Machine

Unless stated otherwise or obvious, throughout the paper newly introduced variables and functions are assumed to cover the range implicit in the context. denotes the binary alphabet , the set of possible bitstrings over , denotes the number of bits in a bitstring ; the -th bit of ; the empty string (where ); if and otherwise (where ). Occasionally it may be convenient to consult Figure 1 below.

- Overview of Hardware and Initial Software / Proof Searcher
- How Online Proof Techniques Connect Syntax and Semantics
- Instructions/Subroutines for Making & Verifying Axioms & Theorems and for Initiating Online Self-Improvements
- Globally Optimal Self-Changes: The Self-Improvement Strategy is not Greedy!

- Bias-Optimal Proof Search (BIOPS)

Juergen Schmidhuber 2003-10-28

Back to Goedel Machine Home Page