| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/lnexp/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 976 B |
|
Quelle top.pvs Sprache: 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.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28