Richard Fateman  wrote:   
   >   
   > There is a community of academics who work with theorem proving and   
   mathematical representation -- look up the CICM conferences.  The overlap   
   between this community and the CAS community should be substantial, but for   
   some reason it is not. I would    
   expect that the representation of assumptions is presumably solved in the CICM   
   community. Probably solved many times.   
      
   Clearly there are systems each applying some method.  And there is a lot   
   of papers.  But bare-bone nature of Open Math (basically everthing   
   interesting is delegated to specilized dictionaries that depend   
   on common agreement of interested parties) clearly shows that   
   there are no "accepted" solution.   
      
   >   
   > It may be that the category-based computational model does not so much   
   substitute for assumptions, as legislates against the existence of assumptions.   
      
   At fundamental level category model in Scrachpad II is agnostic to   
   assumptions.  Existing categories indeed are somewhat hostile   
   to assumptions.  But nothing fundamentaly is against categories   
   that support assumptions.   
      
   >   If your model is (say) the integers only, it is not necessary to provide   
   for  assume(2>1).   If your model is (say) polynomials in one or more   
   variables  x1, x2, ... then something like assume(x2>0) is not necessary for   
   arithmetic of polynomials.     
   Some additional structure may allow for assumptions, but that structure    
   ("evaluation") is perhaps not part of the model.   
      
   Basic thing is failure: current categories in FriCAS assume that   
   failure will happen only in some well-defined circumstances like   
   division by 0.  This allows relativly simple way of computing   
   things that otherwise would be hard to compute.   
      
   Assumptions are closely related to partial functions and failure.   
   Namely, when assumptions are used to decide something lack of   
   assumptions does not mean that negation of assumption is true.   
   Simply, whithout assumptions we can not decide.  Of course, there   
   is old trick of keeping things unevaluated.  But it affects   
   control flow quite a lot.   
      
   > As for Sage/python -- I entirely agree that Sage is a composition of many   
   programs and many capabilities not written in Python.  However, there is some   
   kind of main-line constructive framework that has been put together in Python.   
      
   IIUC Sage without external components can do so little that  I would   
   not call it a CAS.  There are external components written in Python,   
   notably Sympy, but I suspect that with non-Python components removed   
   Sage would be essentially non-functional.   
      
   > I do agree that Maxima internals are complicated --  more so than they   
   should be.  You can start from scratch and build a less complicated system.   
   But can it do the same thing as Maxima?   
      
   Can Maxima do something special?  AFAICS core functionality of   
   various CAS-es is similar (polynomial operations, equation   
   solving, limits, integration, etc.) and in Maxima case this   
   part seem to be rather dated.  It was stat of the art in 1980,   
   but there was (IMO significant) progress after that.   
      
   Of course, Maxima user language is specific to Maxima and   
   various user "tactics" may work quite differently.  But those   
   are "legacy" aspects.  Clearly, new systems are not 100% compatible,   
   but if on average they provide more/better functionality   
   then it is worth switching to new system.   
      
   --   
                                 Waldek Hebisch   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)