MAYBE:

  * (VN) Page 3: "We accept conditional proofs of this goal." unclear

  * (VN) Page 3: "and some extra conditions E" vague

  * (VN) Page 5: since Def 3 is essential for understanding the rest of the
    paper, it should be made more precise, and maybe some examples be
    provided

  * (VN) page 2, Section 2 
    Perhaps the notion of terms or subterms you use could be defined 
    before giving the summation rule. In particular, what are the 
    subterms of a term of the form k \sum_{i = 1}^n t' + t'' ?

  * (VN) page 3, Section 3
    I am not sure that I understand the explanation in the paragraph 
    ``Term generalization'': The description of the heuristic you 
    define seems to be self-referential. Is this right? 

  * (VN) page 5: Please explain, for instance by giving an example, why 
    you need polynomials over non-commutative rings for modeling 
    the problems you consider.
