Doctoral Dissertations

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

Download
Off-campus S&T users

Share My Dissertation If you are the author of this work and would like to grant permission to make it openly accessible to all, please click the button above.

Share

 
COinS