SPTHEO is a parallelization of the sequential theorem proving system SETHEO, based on the SPS model for parallel search. The SPS model has been designed to allow efficient parallel search even in comparatively low bandwidth and high latency environments, such as workstation networks. In order to obtain a portable and efficient implementation, the PVM message passing system has been used for implementing the communication part of the system. This preport describes the basic outline of the system. and presents evaluation results for the communication aspects as well as the performance as a proof system.
展开▼
