Implementaion of a parallel subsumption algorithm (abstract only)
Ralph M. Butler, Arlan R. DeKock · 1985
Many current automated theorem provers use a refutation procedure based on some version of the principle of resolution. These methods normally lead to the generation of large numbers of new clauses. Subsumption is a process that eliminates the superfluous clauses from the clause space, thus speeding up the proof. The research presented here is concerned with the design and implementation of a subsumption algorithm which exploits the parallelism provided by a multiprocessor. All coding is being done in the programming language C, for portability. Monitors [1] are used as the synchronization mechanism. Correct performance in both a multiprocessor and uniprocessor mode has been stressed. The parallel tests are run on a Denelcor HEP located at Argonne National Laboratories.