Bias-Optimal Proof Search (BIOPS)

Here we construct an initial that is -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
(for example, the of equation (1) neither mentions
nor cares for -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 (e.g., inputs)
that change as the machine's life proceeds.

- Online Universal Search in Proof Space
- How a Surviving Proof Searcher May Use the Optimal Ordered Problem Solver to Solve Remaining Proof Search Tasks

Juergen Schmidhuber 2005-01-03