Details About PVS Analysis Library



The PVS dump file contains the following theories:
   top_limits            -- Limit of a functions [T -> real] at a point
                               operations that preserve convergence, 
                               limits of operations on functions,
                               general convergence of functions 
                               limit of composition of functions
  			 
   top_sequence          -- Limits and operations on sequences of reals
                               Bolzano-Weierstrass theorem,    
                               completeness of the reals,  
                               convergence of sequence, 
                               point of accumulation,          
                               cauchy criterion,                  
                               convergent sequence,
                               limit of a sequence,           
			 
   top_continuity        -- Continuous functions [ T -> real] 
                               definition of continuity
                               continuous functions on a closed interval  
                               Intermediate value theorem
			 
   top_derivative        -- Differential Calculus  
                               definition of derivable (differentiable),
                               properties of derivatives,
                               Derivative at max and minimum of f
                               Mean value theorem
                               Chain rule of Differential Calculus


   top_integral          -- Integral Calculus
                               Riemann Integral
                               Fundamental Theorem

            fundamental_theorem,
            table_of_integrals, 
            integral_chg_var,    
            integral_diff_doms,  
            integral_mean_value, 
            integration_by_parts,
            indefinite_integral  

Return to Parent Page

Curator and Responsible NASA Official: Ricky W. Butler
larc privacy statement
last modified: 30 June 2001