Thanks for the reference to the Guarded Expression in Practice paper. That's a really pretty piece of work they've done. I like it a lot. I'll have to get a copy of REDLOG/GUARDIAN and try it. This is a very readable paper and they make a lot of good points.
Instead of wandering off into the sorted-order logic wilderness they did manage to stay algebraic in their approach. They did ask the question: When designing a new CAS based on guarded expressions, how should the knowledge be distributed between the algebraic side and the logic side? Their problems are similar to the ones I encountered and their solutions are similar. The one glaring difference is that I spent a lot of time reducing the expressions into interval notation. The interval notation for x <> 0 becomes [x <> 0] which can be expanded (by POLY(INT), since it is domain specific) to [x < 0] [x = 0] [x > 0] Other domains, say one that has OnePointCompletion (that is, infinity), might put further cases into play: [x = %minusInfinity] [x < 0] [x = 0] [x > 0] [x = %plusInfinity] Another difference is that rather than using a global simplifier and global quantifier eliminator, the process is distributed across the category/domain hierarchy. The intervals are called Constraints, which are collected into SuchThat clauses, and you would have signatures like: and(a:Constraint(POLY(INT)),b:Constraint(POLY(INT)) -> Constraint(POLY(INT)) so that POLY(INT) would get involved in simplifying expressions and constraints which are over that domain. Expressions over other domains, e.g Constraint(POLY(COMPLEX(INT)))) would simplify based on knowledge from that domain instead. Thus each domain would know special information that could be brought forward to help the simplification. But you would expect that kind of architecture decision in Axiom. Major kudos to Dolzmann and Sturm. Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer
