Bias-Optimal Proof Search (BIOPS)

Here we construct an initial $p(1)$ that is $O()$-optimal in a certain limited sense to be described below, but still might be improved as it is not necessarily optimal in the sense of the given $u$ (for example, the $u$ of equation (1) neither mentions nor cares for $O()$-optimality). Our Bias-Optimal Proof Search (BIOPS) is essentially an application of Universal Search [24,26] to proof search. One novelty, however, is this: Previous practical variants and extensions of Universal Search have been applied [38,40,50,47] to offline program search tasks where the program inputs are fixed such that the same program always produces the same results. In our online setting, however, BIOPS has to take into account that the same proof technique started at different times may yield different proofs, as it may read parts of $s$ (e.g., inputs) that change as the machine's life proceeds.