Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/lnexp_fnd/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 2 kB

Quelle expt.pvs Sprache: PVS

expt: THEORY
%----------------------------------------------------------------------------
%
%  Exponentiation: a^x where both a and x are real-valued
%
%  Author:  Rick Butler     NASA Langley Research Center
%           Olga Lightfoot, QMUL
%
%  Version 1.0              8/27/04
%
%----------------------------------------------------------------------------
BEGIN

   IMPORTING ln_exp

   k,n,m: VAR nat
   x,t: VAR real

   epsilon: VAR posreal

   ^^(a: nnreal,x: {r:real | a /= 0 OR r /= 0}): nnreal = IF a = 0 THEN 0
                                                          ELSE exp(x*ln(a))
                                                          ENDIF

   a,b: VAR posreal
   px,py:  VAR posreal
   nzx: VAR nzreal

   hathat_sum   : LEMMA a^^(n + m) = (a^^n)*(a^^m)
   hathat_diff  : LEMMA a^^(n - m) = (a^^n)/(a^^m)

   hathat_to_0  : LEMMA px^^0 = 1

   hathat_to_1  : LEMMA a^^1 = a

   hathat_0     : LEMMA 0^^nzx = 0

   hathat_1     : LEMMA 1^^x = 1

   hathat_nat   : LEMMA a^^n = a^n

   hathat_lt_cross: LEMMA a^^(1/px) < b IMPLIES a < b^^px

   hathat_gt_cross: LEMMA a^^(1/px) > b IMPLIES a > b^^px

   hathat_eq_0  : LEMMA a^^nzx = 0 IFF a = 0

   hathat_eq_1  : LEMMA px^^x = 1 IFF (x = 0 OR px = 1)

   hathat_cross : LEMMA a^^(1/px)=b IMPLIES a=b^^px

   hathat_mult  : LEMMA (a^^px)^^py=a^^(px*py)

   hathat_div   : LEMMA (a/px)^^x = a^^x/px^^x

   hathat_abs   : LEMMA abs(a^^x) = abs(a)^^x

   hathat_sum_posreal: LEMMA (a^^px)*(a^^py)=a^^(px+py)

   hathat_diff_posreal: LEMMA (a^^px)/(a^^py)=a^^(px-py)

   hathat_cont  : LEMMA continuous?(LAMBDA x: a^^x)

%  hathat_cont_nn : LEMMA continuous?(LAMBDA (x: posreal): x^^t)

%  hathat_cont_nnpos : LEMMA continuous?(LAMBDA (x: nnreal): x^^a)

   AUTO_REWRITE+ hathat_to_0
   AUTO_REWRITE+ hathat_to_1
   AUTO_REWRITE+ hathat_0
   AUTO_REWRITE+ hathat_1

%  There are now multiple versions of f(x) = a^x
%  available in PVS.  The prelude provides a version for a^n where n is natural
%  This theory provides a definition for non-negative a and x real
%  The complex library provides exp(z) for complex z, from which
%  we could defined another ^ (not yet done).

%  I am not happy with naming the lemmas "hathat" but I can't think
%  of a better name.  One could explore the use of theory interpretations
%  to create an axiomatic version of ^ which is more general than
%  the current version in the prelude and use these other theories
%  to show that this axiomatic version is consistent.

END expt

quality93%

¤ Dauer der Verarbeitung: 0.5 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.