High parallelism and a proof procedure I: Theoretical considerations

摘要

This paper presents the theoretical basis of a proof procedure, which allows a high degree of parallel processing. The theoretical method is based upon the works of Prawitz's improved proof procedure and Robinson's unification algorithm. The input to the method is a set of clauses (or alternatively, well-formed formulae). The output of the method is the solution to the problem, if it exists. To overcome the inefficiency of the theoretical approach, we outline the main steps of a practical proof procedure. Besides parallel processing, the proof procedure works with bit manipulation rather than symbol manipulation as found in most of the existing proof mechanisms.