There are several researches on the parallelisms in connection graph refutation. The parallelisms identified for the connection graph refutation are: OR parallelism, AND parallelism, DC parallelism, and DCDP parallelism.
We propose a parallel proof mechanism exploiting OR parallelism and DCDP parallelism. In our parallel proof mechanism, several literals are selected, and links incident to them are resolved in parallel. As the problem of selecting optimal literals is NP-hard, a suboptimal algorithm is presented for efficency. In addition, a formal solution to the logical inconsistency occurring in theorem proving using OR parallelism and a method reducing communication between processes are presented.
It is also shown that our parallel proof mechanism is sound and logical consistent.
