tag identifies links that are outside of the NASA domain.
| Theorem | Library | Theory | PVS Name | Author |
|---|---|---|---|---|
| Cauchy-Schwarz Inequality | vectors | vectors.pvs | cauchy_schwartz | Butler |
| Derivative of a Power Series | series | power_series_deriv.pvs | powerseries_deriv | Butler |
| Fundamental Theorem of Arithmetic | number_theory | unique_factorization.pvs | Fundamental_Theorem_Arithmetic | Butler |
| Fundamental Theorem of Calculus | analysis | fundamental_theorem.pvs | fundamental | Butler |
| Infinitude of Primes | number_theory | infinite_primes.pvs | primes_infinite | Butler |
| Integral of a Power Series | series | power_series_integ.pvs | integral_powerseries | Butler |
| Intermediate Value Theorem | analysis | continuity_interval.pvs | intermeditate_value1 | Dutertre |
| Law of Cosines | trig | law_cosines.pvs | Law_Cosines | Munoz |
| Mean Value Theorem | analysis | derivative_props.pvs | mean_value | Dutertre |
| Menger's Theorem | graphs | menger.pvs | hard_menger | Sjogren |
| Order of a Subgroup | algebra | finite_group.pvs | lagrange | Lester |
| Pythagorean Property - Sine and Cosine | trig_fnd | trig_basic.pvs | sin2_cos2 | Lester |
| Ramsey's Theorem | graphs | ramsey.new.pvs | ramseys_theorem | Shankar |
| Sum of a Geometric Series | series | series.pvs | geometric_sum | Butler |
| Taylor's Theorem | analysis | taylors.pvs | Taylors | Butler |
| Trig Identities: Sum and Diff of Two Angles | trig_fnd | trig_basic.pvs | sin_plus, ... | Lester |
| Trig Identities: Double Angle Formulas | trig_fnd | trig_basic.pvs | sin2a, cos2s | Lester |
See PVS Theorem Prover Related Research for NASA Langley sponsored papers on PVS development.
Note: The
tag identifies links that are outside of the NASA domain.