Combining Rank/Activity with Set of Support, Hyperresolution and Subsumption

Description

The rank/activity (R/A) restriction of binary resolution specifies that literals in clauses have ranks, and are either active (can be resolved) or inactive. When a literal is resolved, literals in the new clause, that were of lower rank in the parent clause than the resolved literal, become inactive in the child clause. Literals that merge or factor with literals from other clauses become active. Two derivations are equivalent if they consist of the same resolutions, possibly in a different order, but resulting in the same clause. It is known that with R/A, no two equivalent derivations are found (uniqueness), but that one derivation from each equivalence class is found. In !Jlls paper, R/A is combined with the set of support strategy, with hyperresolution, and also with subsumption. In the first two cases, both completeness and uniqueness are n;taintained. In the subsumption case, completeness and uniqueness can be retained if full rank/activity is kept, but subsumption of small clauses by bigger clauses is not done. With full subsumption, and a restricted version of R/A, completeness is kept but uniqueness is lost.