A taxonomy of parallel strategies for deduction