Corollary 1 (Soundness of PbR Search) The optimization search of PbR is sound.

Proof: By induction. Assume an initial valid plan and a single step rewriting search.

By Theorem 1, the output is either a valid rewritten plan or failure. If the output is failure, the search is trivially sound. Assume there is a valid plan P n –1 after n - 1 rewriting steps.

According to Theorem 1, applying a single rewriting rule to plan P n –1 produces a valid plan P n or failure. Thus, an arbitrary number of rewritings produces a valid plan (or no plan), so PbR's search is sound.  □
Although RewritePlan is sound, it may certainly produce plans that do not have the minimal number of steps when faced with arbitrary rules. For example, imagine that the consequent of a rewriting rule specified two identical steps s1 and s2 (both having as only effects e1 and e2) and that the only flaws in P i were exactly the open conditions e1 and e2. Then, a sound but non step-minimal plan would be using s1 to satisfy e1 and using s2 to stisfy e2 (although each step by itself could satisfy both open conditions). PbR does not discard this plan because we do not make any restriction on the types of acceptable cost functions. If we had a cost function that took the robustness of the plan into account, a plan with both steps may be desirable.

We cannot guarantee that PbR's optimization search is complete in the sense that the optimal plan would be found. PbR uses local search and it is well known that, in general, local search cannot be complete. Even if PbR exhaustively explores the space of plan rewritings induced by a given initial plan and a set of rewriting rules, we still cannot prove that all solution plans will be reached. This is a property of the initial plan generator, the set of rewriting rules, and the semantics of the planning domain.  The rewriting rules of PbR play a similar role as traditional declarative search control where the completeness of the sseerch may be traded for efficiency. Perhaps using techniques for inferring invariants in a planning domain (Gerevini & Schubert, 1998; Fox & Long, 1998; Rintanen, 2000) or proving convergence of term and graph rewriting systems (Baader & Nipkow, 1998), conditions for completeness of a plan-rewriting search in a given planning domain could be obtained.

The design of a plan-rewriting algorithm depends on several parameters:  the language of the operators, the language of the rewriting rules, the choice of full-specification or partialspecification rewriting rules, and the need for all rewritings or one rewriting as required by the search method.

The language of the operators affects the way in which the initial and rewritten plans are constructed. Our framework supports the expressive operator definition language described in Section 2.1.  We provide support for this language by using standard techniques for causal link establishment and threat checking like those in Sage (Knoblock, 1995) and UCPOP
(Penberthy & Weld, 1992).

The language of the anteced ents of the rewriting rules affects the efficiency of matching.

Our system implements the conjunctive query language that was described in Section 3.1.1. However, our system could easily accommodate a more expressive query language for the rule antecedent, such as a relationally complete language (i.e., conjunction, disjunction, and sfe negation) (Abiteboul, Hull, & Vianu, 1995), or a recursive language such as datalog with stratified negation, without significantly increasing the computational complexity of the approach in an important way, as we discuss in Section 3.1.4.

The choice of fully versus partially specified rewriting rules affects the way in which the replacement plan is embedded into the current plan. If the rule is completely specified,