Parallel version of the Boyer-Moore prover. Technical report
Matt Kaufmann, Matthew Wilding · OSTI OAI (U.S. Department of Energy Office of Scientific and Technical Information) · 1989
The idea of this system is to use idle processors to increase the speed of NQTHM. There were many design considerations, including: no shared-file system; easy-to-kill jobs on a given host; easy-to-prevent job assignment on a given host; Robust; and nicer user interface. The system will be used to process an NQTHM event list in parallel, with a given granularity. Given a granularity of n, then the first job will process the first n PROVE-LEMMAs. Each subsequent job will process n PROVE-LEMMAs. Since an arbitrary subsequence of PROVE-LEMMAs may require a previous definition, each will process all previous definitions. A subsequence of PROVE-LEMMAs may also require PROVE-LEMMAs from previous subsequences, treating each PROVE-LEMMA as an ADD-AXIOM. This system allows the user to run a job on multiple machines in parallel. The issue of machine use has been discussed at Computational Logic and a preliminary policy adopted. It is the policy at Computational Logic to allow users to run parallel jobs using the dispatcher. Spawned jobs are to be run at the default (nice) priority level, and it is OK for any user to kick spawned parallel jobs off the local machine if he wishes (without feeling bad about it).