Part of the result of this research is expected to be 'provisos', that is, statements under which a result is valid, e.g.
f(x) provided x>0 and 'assume', e.g. assume x>0 then integrate f(x) Since every function knows its specification, pre- and post-conditions, this can be computed. And since every end-user result has that information it can be propagated for further calculations. My previous research on provisos used cylindrical algebraic decomposition (CAD) which tries to derive provisos "after the fact". CAD no longer seems necessary. Anyway, that's the plan. Tim
