Details About PVS Complex Library

The PVS dump file provides a complex numbers library. The complex numbers are defined (axiomatically) in this way so that we can conveniently use the numeric constants 0, 1, 2 etc. The alternative -- using pairs of reals to represent the real and imaginary components -- would lead to the somewhat unappealing formulation of Euler's result as "exp((0,1)*(pi,0)) = (-1,0)". As a matter of taste, we prefer the somewhat more elegant formulation: "exp(i*pi) = -1". It contains the following theories:

  complex_types,       % Basic Definitions of Complex Number Types
  polar,               % Polar coordinate complex numbers
  arithmetic,          % Basic Arithmetic on Complex Numbers
  exp,                 % Complex logarithm and exponential functions

Return to Parent Page

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