  Four algorithms for propositional forgetting are compared. The first performs
all possible resolutions and deletes the clauses containing a variable to
forget. The second forgets a variable at time by resolving and then deleting
all clauses that resolve on that variable. The third outputs the result of all
possible linear resolutions on the variables to forget. The fourth generates a
clause from the points of contradiction during a backtracking search. The
latter emerges as the winner, with the second and first having some role in
specific cases. The linear resolution algorithm performs poorly in this
implementation.
