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 in this thesis is concerned with the design and implementation of a subsumption algorithm which exploits the parallelism provided by a multiprocessor. For portability, all coding is done in the programming language C. Monitors are used as the synchronization mechanism. Correct performance in both a multiprocessor and uniprocessor mode is stressed. The parallel tests are run on a Denelcor HEP located at Argonne National Laboratory.
Butler, Ralph M. and Dekock, Arlan R., "An Algorithm for Parallel Subsumption" (1985). Computer Science Technical Reports. 89.
© 1985 University of Missouri--Rolla, All rights reserved.