Paper Info
Title
Implementaion of a parallel subsumption algorithm (abstract only)
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 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.
Year
DOI
Venue
1985
10.1145/320599.322473
ACM Conference on Computer Science
Keywords
Field
DocType
parallel subsumption algorithm,new clause,correct performance,denelcor hep,argonne national laboratories,programming language c,parallel test,clause space,large number,subsumption algorithm,current automated theorem provers,syntax,theorem prover,error correction,grammars,compilers,semantics,portability,programming language
Rule-based machine translation,Synchronization,Uniprocessor system,Programming language,Computer science,Algorithm,Multiprocessing,Theoretical computer science,Error detection and correction,Coding (social sciences),Compiler,Software portability
Conference
ISBN
Citations 
PageRank 
0-89791-150-4
0
0.34
References 
Authors
1
2
Name
Order
Citations
PageRank
Ralph M. Butler118811.39
Arlan R. DeKock200.68