Details About PVS lnexp Library



    Definition of Logarithm and Exponential functions

    ln_exp              -- Foundational definitions
    ln_exp_ax           -- Axiomatic version (created from ln_exp)
    ln_exp_series       -- Representation as infinite series
    hyperbolic          -- e.g. sinh cosh functions
Return to Parent Page

Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 30 June 2001