Parallel theorem proving with connection graphs

Abstract

In general, theorem provers are relatively slow. Speed up can be achieved by directing the search towards finding a proof and by using parallelism. The parallelisms identified in connection graph refutations are: or parallelism, and parallelism, and dcdp parallelism. In dcdp parallelism, the links (edges) incident to distinct clauses and edge disjoint pairs are resolved in parallel. Optimally selecting potential parallel links is equivalent to solving the optimal graph coloring problem. Fortunately, however, optimal solutions to this NP-hard problem are not crucial. We describe a parallel solution of a sub-optimal graph coloring algorithm In and parallelism, all literals in the sun clause are resolved concurrently and all the resolvents obtained. The resolvents, along with their inherited links, are inserted into the graph. The sun clause, and all the links connected to it, are removed from the graph. Because shared variables are restricted to have the same instantiation when there are shared variables in the sun clause, resolving literals concurrently becomes difficult. We discuss different approaches for performing this and parallelism.