Abstract Conjunctive Partial Deduction Using Regular Types and Its Application to Model Checking