A choice of control strategy affects both
EFFICIENCY and COMPLETENESS
Consider a resolvent Rij (descendent) of parent clauses Ci & Cj
all n-level resolvents are computed first - complete but very inefficient
one parent is taken from the negated goal clauses or descendents
complete if used in a breadth-first manner
more efficient than unrestricted breadth first
modified (more focussed) strategy to set of support
select for preference a single literal clause (unit) for a parent
a goal clause or its descendent is resolved with a clause from base set
only complete for HORN clauses - with at most one positive literal
| Previous slide | Next slide | Back to first slide | View graphic version |