Issues in instantiating Refineplan
Although a planner can use multiple different refinements, most implementations stick to a single refinement
Although refinement can be used along with any type of correctness check, there is affinity between specific refinements and proof technqiues (support finite differencing)
- FSR and Progression based proof
- BSR and Regression based proof
- PSR and Causal proof
Although it is enough to check if any one of the safe linearizations are solutions, most planners refine a partial plan until all its linearizations are safe
- Tractability refinements (pre-order, pre-satisfy)
With these changes, an instantiated and simplified planner
may “look” considerably different from the general template