Goal: specify refinement operator such that each
hypothesis is generated only once.
Approach:
construct an ordering of refinement operations
Optimal refinement operator ropt:
ropt:={h' Î
r(h)|o(h') > o(h)}.
allows to avoid duplication simply by knowing current hypothesis
and position in refinement ordering
reduces subsumption tests with previous hypotheses
good for parallelization
N.B. This ordering just ensures we generate each node
only once - it does not necessarily have to be ordering in which we explore
nodes (i.e., we do not have to do depth-first along this ordering).
