See the dependency graph of all the contributions in the NASA PVS Library NASA PVS Library 6.0.9 (11/10/14).
Development  Description  Contributors 

ACCoRD (web)  Framework for the analysis of air traffic conflict detection and resolution algorithms.  AN, CM, GD, GH, JM, RB 
algebra  Groups, monoids, rings, etc.  DL, RB 
analysis  Real analysis, limits, continuity, derivatives, integrals.  AN, BD, RB 
Bernstein (web)  Formalization of multivariate Bernstein polynomials.  AN, CM 
complex  Complex numbers.  DL 
complex_alt  Alternative formalization of complex numbers.  DL 
complex_integration  Complex integration.  DL 
co_structures  Sequences of countable length defined as coalgebra datatypes.  JJ 
digraphs  Directed graphs: circuits, maximal subtrees, paths, DAGs.  AA, JS, KR, RB 
exact_real_arith  Exact real arithmetic including trig functions.  DL 
extended_nnreal  Extended nonnegative reals.  DL 
fault_tolerance  Fault tolerance protocols.  AG, JM, LP, PM 
float  Floating point numbers and arithmetic.  PM, SB 
graphs  Graph theory: connectedness, walks, trees, Menger's Theorem.  RB, JS 
groups  Group theory.  ALG 
ints  Integer division, gcd, mod, prime factorization, min, max.  AG, BD, PM, RB 
interval_arith (web)  Interval arithmetic and numerical
approximations. Includes automated strategies numerical
for computing numerical approximations and
interval for checking
satisfiability and validity of simply quantified realvalued
formulas. This development includes a formalization of Allen interval temporal logic. 
AN, CM, DS 
lebesgue  Lebesgue integral with connection to Riemann Integral.  DL 
linear_algebra  Linear algebra.  HH, GP, SO 
lnexp  Logarithm, exponential and hyperbolic functions.  DL, RB 
lnexp_fnd  Foundational definitions of logarithm, exponential and hyperbolic functions.  AN, DL, RB 
measure_integration  Sigma algebras, measures, FubiniTonelli Lemmas.  DL 
metric_space  Domains with a distance metric, continuity and uniform continuity.  DL 
numbers  Elementary number theory.  AG, AN, RB 
orders  Abstract orders, lattices, fix points.  AG, BD, JJ 
power  Generalized Power function (without ln/exp).  DL 
probability  Probability theory.  DL 
reals  Summations, sup, inf, sqrt over the reals, absolute value, etc.  AN, BDV, CM, PM, RB 
scott  Scott topology.  DL 
series  Power series, comparison test, ratio test, Taylor's theorem.  AN, DL, RB 
sets_aux  Powersets, orders, cardinality over infinite sets. Includes functional and relational facts based on Axiom of Choice and refinement relations based on equivalence relations.  BD, DL, JJ, DS 
sigma_set  Summations over countably infinite sets.  DL 
structures  Bounded arrays, finite sequences, bags, and several other structures.  CM, DG, KR, LP, RB 
Sturm (web)  Formalization of Sturm's theorem for univariate
polynomials. Includes strategies sturm and
monopoly
for automatically proving
univariate polynomial relations over a real interval.

AN, CM, AD 
Tarski (web)  Formalization of Tarski's theorem for univariate
polynomials. Includes strategy tarski for automatically proving
systems of univaraite polynomial relations on the real line.

AN, CM, AD 
topology  Continuity, homeomorphisms, connected and compact spaces, Borel sets/functions.  DL 
trig  Trigonometry: definitions, identities, approximations.  CM, BDV, DL, GD, HG, RB, VC 
trig_fnd  Foundational development of trigonometry.  AN, BDV, CM, DL, GD, HG, RB 
TRS  Term rewrite systems and Robinson unification algorithm.  AA, ALG, AR, MA 
TU_games  Cooperative TUgames.  EM 
vect_analysis  Limits, continuity, and derivatives of vector functions.  AN, CM, RB 
vectors  2D, 3D, 4D, and ndimensional vectors.  AN, BDV, CM, HG, PM, RB 
while  Semantics for the programming language "while".  DL 
Theorem  Theory  PVS Name  Author 

CauchySchwarz Inequality 
vectors@vectors  cauchy_schwartz  RB 
Derivative of a Power Series 
series@power_series_deriv  powerseries_deriv  RB 
Fundamental Theorem of Arithmetic  numbers@unique_factorization 
Fundamental_Theorem_Arithmetic  RB 
Fundamental Theorem of Calculus  analysis@fundamental_theorem 
fundamental  RB 
Fundamental Theorem of Interval Arithmetic  interval_arith@interval_expr 
Eval_fundamental  CM, AN 
Inclusion Theorem of Interval Arithmetic  interval_arith@interval_expr 
Eval_inclusion  CM, AN 
Infinitude of Primes 
numbers@infinite_primes  primes_infinite  RB 
Integral of a Power Series 
series@power_series_integ  integral_powerseries  RB 
Intermediate Value Theorem  analysis@continuity_interval  intermeditate_value1
 BD 
Law of Cosines 
trig_fnd@law_cosines  Law_Cosines  CM 
Mean Value Theorem 
analysis@derivative_props  mean_value  BD 
Matel's Theorem  graphs@mantel  Mantel  AD 
Menger's Theorem  graphs@menger  hard_menger  JS 
Order of a Subgroup  algebra@finite_group  lagrange  DL 
Pythagorean Property  Sine and Cosine  trig_fnd@trig_basic  sin2_cos2  DL 
Ramsey's Theorem 
graphs@ramsey 
 NS 
Sum of a Geometric Series  series@series  geometric_sum  RB 
Taylor's Theorem  analysis@taylors  Taylors  RB 
Trig Identities: Sum and Diff of Two Angles  trig_fnd@trig_basic  sin_plus , ...  DL 
Trig Identities: Double Angle Formulas  trig_fnd@rig_basic  sin2a, cos2s  DL 
SchroederBerstein Theorem  orders@set_antinsymmetric  inj_inj_bij  JJ 
Denumerability of the Rational Numbers  sets_aux@countable_set  countable_rat  JJ 
Heine Theorem and Multiary Variants  analysis@uniform_continuity  Heine , multiary_Heine  AN 
FubiniTonelli Lemmas  measure_integration@fubini_tonelli  fubini_tonelli_*  DL 
KnuthBendix Critical Pair Theorem 
TRS@critical_pairs  CP_Theorem  ALG, MA 
ChurchRosser Theorem  TRS@results_confluence  CR_iff_Confluent  ALG, MA 
Newman Lemma  TRS@newman_yokouchi  Newman_lemma  ALG, MA 
Yokouchi Lemma  TRS@newman_yokouchi  Yokouchi_lemma  ALG, MA 
Robinson Unification  TRS@robinsonunification  completeness_robinson_unification_algorithm  AA, MA 
Confluence of Orthogonal TRSs  TRS@orthogonality  Orthogonal_implies_confluent  AR, MA 
Sturm's Theorem  Sturm@sturm  sturm  AN 
Tarski's Theorem  Tarski@sturmtarski  sturm_tarski_unbounded  AN, AD 
AA  Andreia Avelar Borges, University of Brasilia, Brazil 

AD  Aaron Dutle, NASA, USA 
AG  Alfons Geser, HTWK Leipzig, Germany 
ALG  André Galdino, Federal University of Goiás, Brazil 
AN  Anthony Narkawicz, NASA, USA 
AR  Ana Cristina Rocha Oliveira, University of Brasilia, Brazil 
BD  Bruno Dutertre, SRI, USA 
BDV  Ben Di Vito, NASA, USA 
CM  César Muñoz, NASA, USA 
DG  David Griffioen,CWI, The Netherlands 
DL  David Lester, Manchester University, UK 
DS  Dragan Stosic, Ireland 
EM  Érik MartinDorel, U. Montpellier 2 & U. of Perpignan (formerly), France 
HH  Heber HerenciaZapana, NIA, USA 
JJ  Jerry James, Utah State University (formerly), USA 
JM  Jeff Maddalon, NASA, USA 
JS  Jon Sjogren, Department of Defense, USA 
KR  Kristin Rozier, NASA, USA 
GD  Gilles Dowek, INRIA, France 
GH  Geroge Hagen, NASA, USA 
GP  Gilberto Perez, University of La Coruña, Spain 
HG  Hanne Gottliebsen, NIA (formerly), USA 
LP  Lee Pike, Galois, USA 
MA  Mauricio AyalaRincón, University of Brasilia, Brazil 
NS  Natarajan Shankar, SRI, USA 
PM  Paul Miner, NASA, USA 
RB  Ricky Butler, NASA, USA 
SB  Silvie Boldo, INRIA, France 
SO  Sam Owre, SRI, USA 
VC  Víctor Carreño, NASA (formerly), USA 
If we have incorrectly attributed a PVS development, please let us know.
The tag identifies links that are outside the NASA domain