How a Surviving Proof Searcher May Use BIOPS to Solve Remaining Proof Search Tasks

In what follows we assume that the execution of the *switchprog*
corresponding to the first found target theorem has not rewritten the code of
itself--the current is still equal to --and has
reset *switchbit* and returned
control to such that it can continue where it was interrupted.
In that case the BIOPS subroutine of can use OOPS
[38,40]
to accelerate the search for the
-th target theorem () by reusing proof techniques for earlier found
target theorems where possible. The basic ideas are as follows (details
in [38,40]):

Whenever a target theorem has been proven, *freezes*
the corresponding proof technique: its code becomes non-writable
by proof techniques to be tested in later proof search tasks.
But it remains readable,
such that it can be copy-edited and/or invoked as a subprogram by future proof
techniques. We also allow prefixes of proof
techniques to temporarily rewrite the probability distribution
on their suffixes
[40,38],
thus essentially rewriting
the probability-based search
procedure (an incremental extension of Method 2.1)
based on previous experience. As a side-effect we metasearch
for faster search procedures, which can greatly accelerate the learning of
new tasks [40,38].

Given a new proof search task, BIOPS performs OOPS
[40,38]
by spending half the total search time on a
variant of
Method 2.1
that searches only among self-delimiting
[23,6] proof techniques starting with the most recently
frozen proof technique. The rest of the
time is spent on fresh proof techniques with arbitrary prefixes
(which may reuse previously frozen proof techniques though)
[38,40].
(We could also search for a *generalizing* proof technique
solving all proof search tasks so far. In the first half of the search
we would not have to test proof techniques on tasks other than
the most recent one, since we already know that their prefixes
solve the previous tasks
[38,40].)

It can be shown that OOPS is
essentially **8-bias-optimal** (see Def. 2.1),
given either the initial bias or intermediate biases due to
frozen solutions to previous tasks
[38,40].
This result immediately carries over to BIOPS.
To summarize, BIOPS essentially allocates part of the total search
time for a new task to proof techniques that exploit previous successful
proof techniques in computable ways. If the new task can be solved faster
by copy-editing / invoking previously frozen
proof techniques than by solving the new proof search task from scratch,
then BIOPS will discover this and profit thereof. If not, then
at least it will not be significantly slowed down by the previous
solutions-- BIOPS will remain 8-bias-optimal.

Back to Goedel machine home page