Generating relevant models

Manthey and Bry's model generation approach to theorem proving for FOPC has been greeted with considerable interest. Unfortunately the original presentation of the technique can become arbitrarily inefficient when applied to problems whose statements contain large amounts of irrelevant information. We show how to avoid these problems whilst retaining nearly all the advantages of the basic approach.