Automatic Generation of Concurrent Provers.
Raul Lopes · 2000
Introduction A framework is outlined that combines automatic generation of proof search strategies for theorem provers with concurrent proof search. The framework consists of two programs: P 2 , that implements an algorithm that generates prioritized logic programs, representing proof search strategies; and P 2 -frame, a proof search engine that can use strategies generated by P 2 to drive concurrent provers. P 2 has been applied to generate provers for Intuitionistic Propositional Calculus (IPC), modal logics T, S4, and S5, and for classical second-order logic (see, for example, [4].) Figure 1 shows a few dicult theorems proved by a concurrent prover, using a proof search strategy generated by P 2 . Particularly interesting are the automatic proofs obtained for the problems 1 to 4 (taken from [1]) and for Cantor's theorem that the pow