Abstract
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.
Recommended Citation
Butler, Ralph M. and Dekock, Arlan R., "An Algorithm for Parallel Subsumption" (1985). Computer Science Technical Reports. 89.
https://scholarsmine.mst.edu/comsci_techreports/89
Department(s)
Computer Science
Report Number
CSc-85-1
Document Type
Technical Report
Document Version
Final Version
File Type
text
Language(s)
English
Rights
© 1985 University of Missouri--Rolla, All rights reserved.
Publication Date
May 1985
Comments
This report is substantially the Ph.D. dissertation of the first author, completed May, 1985.