Top File of PVS lnexp_fnd Library

 
top: THEORY
%------------------------------------------------------------------------
%   Definition of Logarithm and Exponential functions (lnexp_fnd)
%
%   Version 1.0    12/3/03 
%   Version 1.1    8/25/04  
%   Version 1.2    10/27/04        added exp_approx, ln_approx
%   Version 1.3    3/29/05         infinite series for ln completed
%   Version 1.4    4/10/05         ln_exp_series_alt, ln_exp_ineq added
%
%   Authors:  Ricky W. Butler              NASA Langley Research Center
%             David Lester                 Manchester University
%
%------------------------------------------------------------------------------
BEGIN
    IMPORTING ln_exp,              % Foundational definitions
              expt,                % a^x where x real and a >= 0
              hyperbolic,          % e.g. sinh cosh functions
              exp_series,          % exp as infinite series
              ln_series,           % ln  as taylor series
              exp_approx,          % exp approximation
              ln_approx,           % ln aproximation
              ln_exp_series_alt,   % alternate ln/exp series formulation
              ln_exp_ineq          % inequalities involving ln/exp

END top

The tag identifies links that are outside the NASA domain