Four algorithms for propositional forgetting
This addresses the problem of efficiently forgetting variables in propositional logic, which is incremental as it compares existing algorithmic approaches.
The paper compared four algorithms for propositional forgetting, finding that the backtracking-based algorithm emerged as the winner, while the linear resolution algorithm performed poorly in this implementation.
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.