Towards better simplification of elementary functions

Abstract

We present an algorithm for simplifying a large class of elementary functions in the presence of branch cuts. This algorithm works by:(a) verifying that the proposed simplification is correct as a simplification of multi-valued functions;(b) decomposing C (or Cn in the case of multivariate simplifications) according to the branch cuts of the relevant functions;(c) checking that the proposed identity is valid on each component of that decomposition.This process can be interfaced to an assume facility, and, if required, can verify that simplifications are valid "almost everywhere".