The report describes Omega's multi-strategy proof planner Multi.  After the introduction of the different
components of Multi, the application to the domain of epsilon-delta proofs/limit problems, is described. An
emphasis is put on the meta reasoning and failure reasoning capabilites of the architecture of Multi. The
benefits of this architecture is compared with the former proof planner of Omega and motivated by theorems in
the limit domain, which require failure reasoning.  The report concludes with a comparison to other theorem
provers for limit problems, and especially the critc mechanism of the Clam proof planner. Finally an analysis
of the implementation of reasoning techniques in the frame work of Multi is given.

This report is interesting for everybody who wants to know about the current state of the art of proof
planning in the Omega system. It is helpful for the comprehension of Multi that the description of the
architecture comes along with examples of the different components and is elaborated on a concrete case study.
The report also addresses the criticism brought up against proof planning with a critical analysis of the
approach and is therefore also important for people outside of the proof planning community.

The report is sound and complete, and I strongly recommend publication as Seki report,
when the following comments are considered.  
--------------- 

Section 5.3: From the description on page 38 it becomes very obscure what consistency of
constraints means.  Consistency (1) and existence of witnesses (2) of meta-variables are
different. The use of Tell-CS in the sections before suggests that you expect witnesses
from a consistent constraint store, if not the test for Tell-CS should be (2)? What is
consistency exactly?  You didn't make explicit if the extension of Cosie is obvious or a
bears some conceptional problems.  If you can extend Cosie this way, couldn't you extend
Cosie to reject the constraints of the first run directly? Even if you don't know whether
Cosie will be able to solve the remaining problem, you can make explicit that your failure
reasoning patches an unsolvable situation to a situation, where you have a chance to find
a solution. In the final constraints store I could not figure out why (c_e * mv_f)/2 > 0
holds under the instantiation.


Minor inconsistencies:
-p3,par2: "introduced in [1]" I think this kind of linearised ND goes back to Suppes 1957, you could say as 
 "as used in [1]" or "as defined in [1]"
-p3,par3: "Since methods are also tactics" This could confuse the readerm, I suggest to say 
 "Since an action justifies a line"
-p9, tasks: Are there other tasks than line and inst (first line)? 
            "Relevant for the application ..." this sounds as if inst-tasks are only used for the limit domain, 
            I think they are useful in other domains, too.
-p10,par2: "A strategy can change ... the history of strategies" sounds like you could have a strategy, which activeley 
           manipulates history information, I thought history is a side effect of strategies/proof planning.
-p16,line1: Where is "form-conjunction"?
-p16,par3: Where is "constraints slot"?
-p16,last par: if TellCS-F is analogous to TellCS-B, why can it accept 0<\delta_1 without MVs?
-p16,last par: min(\delta_1,\delta_2) violates MV < \delta_i, you probably mean MV <= \delta_i
-p26,par3, and several times later: SetFocus-B is applied but does not appear in the Figure of the PDS?
-p33,CPlanner: it is somewhat strange that one case is done by analogy but not the other. How can you distinguish 
	       this case. Do you explicitly control this, or is CPlanner tried but fails?
-p35,par2 from bottom: "application condition unify", the unify is not introduced. 
-p36,par3: =Subst*-B could be confused with =Subst-B, maybe you could mention that =Subst*-B is like =Subst-B
           and then explain the differences. 
-p46,par2 from bottom: Sounds like you can really measure complexity of a term. 
                       You have some heuristic measure for this?

Language, typos and suggestions:
-Because of the size of the report I suggest a table of contents
-p2,par2: "Omega previous" -> "Omega's previous"
-p4,par1: premises, conclusions, ... seems to use a very small font
-p4,par5: "that employ the equality =. Essentially, the method performs" ->
             "that performs"
-p5,par3: "knowledge of the true nature of the witness" -> "knowledge about the witness"
-p5,notation: you introduce notation and violate it at the same time with =Subst-B which is not in \sc
-p6,par2: comma between "attempts" and "etc"
-p9,tasks,par2: "can to tackle" -> "can be used to tackle"
-p12,par2 from bottom: space in "prefer-demand-satisfying- offer" 
-p17,par2: ! in "c!\not\in MV"
-p18,par2 from bottom: "The formulas of the former three tasks" sounds ambigious with "new tasks" before, 
 probably "The formulas of the first three (new) tasks"
-p24,backtrack: You only say that the action computes the line task, you could add that this line task is 
                computed to be backtracked.
-p30,footnote: "allows" -> "allow"
-p37,par before 5.3: "The Unwrapping" -> "The unwrapping" or just "Unwrapping"
-p37,par1 of 5.3: "achieve given goals" -> "achieve the given goals"
-p41,par1: simple version of LIM+: I thought there is only one theorem LIM+. Probably simple formalisation, or 
	   adjusted formalisation.
-p41,par1: "that could be formulated" sounds strange. 
-p43,par2 from bottom: "the Multi approach" -> "Multi's approach", "matching" not mentioned before. You don't 
	               have to reference the conrete appl cond, but can just say appl. conds which check 
                       matching or unif.
-par47,par2 and par3 of Failure Reasoning: "maybe provide" -> "may need"