A Scheduling Strategy for Parallel Proof Checking and Verification

Proof checking is one of the major concerns of many mechanized formal approaches. This paper first deals with scheduling issues related to parallel proof checking, then applies the obtained result and similar idea to parallel verifications. To facilitate understanding, the discussion is based on INCAPS, an interactive deduction system of temporal logic. This method can also be adapted for improving other mechanized formal systems.