An algorithm for parallel subsumption

Author

Ralph Milton Butler

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"--Abstract, page ii.

Advisor(s)

Dekock, Arlan R.
Metzner, John R.

Committee Member(s)

Stigall, Paul D.
Metzner, Henry
Sager, Thomas J.

Department(s)

Computer Science

Degree Name

Ph. D. in Computer Science

Publisher

University of Missouri--Rolla

Publication Date

Spring 1985

Pagination

vi, 134 pages

Note about bibliography

Includes bibliographical references (pages 87-93).

Rights

© 1985 Ralph Milton Butler, All rights reserved.

Document Type

Dissertation - Restricted Access

File Type

text

Language

English

Thesis Number

T 5082

Print OCLC #

13141426

Link to Catalog Record

Electronic access to the full-text of this document is restricted to Missouri S&T users. Otherwise, request this publication directly from Missouri S&T Library or contact your local library.

Recommended Citation

Butler, Ralph Milton, "An algorithm for parallel subsumption" (1985). Doctoral Dissertations. 568.
https://scholarsmine.mst.edu/doctoral_dissertations/568