Distributed models for deduction allow for more powerful proof systems, but also lead to new problems. In particular, the analysis of the deduction process becomes harder, as a number of largely independent agents may contribute to the proof. In a system including cooperating agents timing considerations can lead to further problems.
In this paper we first introduce the TEAMWORK method and the DISCOUNT system for distributed equational reasoning. We point out the difficulties in obtaining a detailed representation of the proofs generated by a distributed system with completely distributed memory and present our solution for the TEAMWORK approach. Using this solution we are able to explain some of the speedups DISCOUNT was able to obtain in distributed mode. We also show how the representation of an equational proof as a listing of inferences can be transformed into a proof easily readable by human beings. Finally, pruned proof protocols (containing only facts contributing to the proof) also enable us to develop new, adaptive strategies for the proof search.
Generated: 29/10/99