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 $O()$-optimal $p(1)$ 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 $\cal L$ implemented within $p(1)$. For example, $\cal L$ 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 $s$ to be read, such as inputs encoded in variable $x$ (a substring of $s$) or the code of $p(1)$. It may write on $s^p$, a part of $s$ reserved for temporary results. It also may rewrite switchprog, and produce an incrementally growing proof placed in the string variable proof stored somewhere in $s$. proof and $s^p$ 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 $s^p$, the programming language $\cal L$ 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 $p$-modifying program was found and should be executed now. Certain long proofs can be produced by short proof techniques.