The University of Sussex

Relevant constraints in model elimination

Allan Ramsay

The theorem proving technique for first-order predicate calculus (FOPC) proposed by Manthey and Bry (1988) is extremely effective for a class of "hard" problems in FOPC. Their basic algorithm, however, performs very poorly if the premises from which a goal is to be derived contain large amounts of irrelevant information. The author shows how to improve Manthey and Bry's algorithm so that the presence of irrelevant premises does not destroy its effectiveness.

This paper is not available online