Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: atan.pvs Sprache: PVS

Original von: PVS^©

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

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.