** Next:** Important Instructions Used by
** Up:** Essential Details of One
** Previous:** Essential Details of One

##

Proof Techniques

Brute force proof searchers
(used in Hutter's work [16,17];
see Section 6.4 for a review)
systematically generate all proofs
in order of their sizes. To produce a certain proof,
this takes time exponential in proof size.
Instead our -optimal will produce many proofs
with low algorithmic complexity
[52,22,27]
much more quickly. It systematically tests (see Section 5)
programs called
*proof techniques* written in universal language
implemented within .
For example, may be a variant of PROLOG [7]
or the universal FORTH[29]-inspired
programming language used in recent work on optimal search
[47].
A proof technique is composed
of instructions that allow any part of to be read,
such as inputs encoded in variable (a substring of ) or
the code of . It may write on , a part of reserved for
temporary results. It also may rewrite *switchprog*,
and produce an incrementally growing proof placed in the
string variable *proof* stored somewhere in .
*proof* and are reset to the empty string at
the beginning of each new proof technique test.
Apart from standard arithmetic and function-defining instructions
[47] that modify ,
the programming language includes special instructions
(details in Section 3.2)
for prolonging the current *proof* by correct theorems,
for setting *switchprog*,
and for checking whether a provably optimal -modifying
program was found and should be executed now.
Certain long proofs can be produced by short proof techniques.

** Next:** Important Instructions Used by
** Up:** Essential Details of One
** Previous:** Essential Details of One
Juergen Schmidhuber
2005-01-03