Cooperating proof attempts

Abstract

This paper introduces a pseudo-concurrent architecture for first-order saturation-based theorem provers with the eventual aim of developing it into a truly concurrent architecture. The motivation behind this architecture is two-fold. Firstly, first-order theorem provers have many configuration parameters and commonly utilise multiple strategies to solve problems. It is also common that one of these strategies will solve the problem quickly but it may have to wait for many other strategies to be tried first. The architecture we propose interleaves the execution of these strategies, increasing the likeliness that these ‘quick’ proofs will be found. Secondly, previous work has established the existence of a synergistic effect when allowing proof attempts to communicate by sharing information about their inferences or clauses. The recently introduced AVATAR approach to splitting uses a SAT solver to explore the clause search space. The new architecture considers sharing this SAT solver between proof attempts, allowing them to share information about pruned areas of the search space, thus preventing them from making unnecessary inferences. Experimental results, using hard problems from the TPTP library, show that interleaving can lead to problems being solved more quickly, and that sharing the SAT solver can lead to new problems being solved by the combined strategies that were never solved individually by any existing theorem prover.