Top File of PVS lnexp Library
top: THEORY
%------------------------------------------------------------------------
% Axiomatic Version of Logarithm and Exponential functions (lnexp)
%
% Version 1.0 4/15/05
%
% 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