** Next:** How a Surviving Proof
** Up:** Bias-Optimal Proof Search (BIOPS)
** Previous:** Bias-Optimal Proof Search (BIOPS)

##

Online Universal Search in Proof Space

BIOPS starts with a probability distribution
(the initial bias) on the proof techniques that
one can write in ,
e.g.,
for programs composed from
possible instructions [26].
BIOPS is *near-bias-optimal*
[47]
in the sense that it will not spend
much more time on any proof technique than it deserves,
according to its probabilistic bias,
namely, not much more than its probability times the total search time:

A proof technique can interrupt Method 5.1
only by invoking instruction *check()* (Item 5),
which may transfer
control to *switchprog* (which possibly
even will delete or rewrite Method 5.1).
Since the initial
runs on the formalized hardware, and since proof techniques
tested by can read and other parts of , they
can produce proofs concerning the (expected)
performance of and BIOPS itself.
Method 5.1 at least has the
optimal *order* of computational complexity in the following
sense.

**Theorem 5.1**
If independently of variable

*time(s)* some unknown
fast proof technique

would require at most

steps to produce
a proof of difficulty measure

(an integer depending on
the nature of the task to be solved), then
Method

5.1
will need at most

steps.

**Proof.**
It is easy to see that
Method 5.1 will need at most
steps--the constant factor does not depend on .
*Q.E.D.*
Note again, however, that
the proofs themselves may concern quite
different, arbitrary formalizable notions of optimality
(stronger than those expressible in the -notation)
embodied by the given, problem-specific, formalized
utility function .
This may provoke useful, constant-affecting rewrites of
the initial proof searcher despite its limited (yet popular
and widely used)
notion of -optimality.

** Next:** How a Surviving Proof
** Up:** Bias-Optimal Proof Search (BIOPS)
** Previous:** Bias-Optimal Proof Search (BIOPS)
Juergen Schmidhuber
2005-01-03