Bob has a collection of propositions he believes and a set of inference rules. He’d like to derive more propositions from his existing ones, but this is a computationally intensive process and he’s generally forced to just run a naive breadth-first search as a low-priority background task.
Alice has been lucky enough to derive a new proposition recently, using existing propositions that she knows Bob already has. She transmits the complete derivation process to Bob. Bob verifies the derivation process, thus arriving at the new proposition sooner than he would have gotten to it using his own thought processes.
Bob has a collection of propositions he believes and a set of inference rules. He’d like to derive more propositions from his existing ones, but this is a computationally intensive process and he’s generally forced to just run a naive breadth-first search as a low-priority background task.
Alice has been lucky enough to derive a new proposition recently, using existing propositions that she knows Bob already has. She transmits the complete derivation process to Bob. Bob verifies the derivation process, thus arriving at the new proposition sooner than he would have gotten to it using his own thought processes.