A Foundational Theory of Trigonometry, providing definitions, identities, approximations.
| Theorem | Location | PVS Name | Contributors |
|---|---|---|---|
| Law of Cosines | trig@law_cosines |
Law_Cosines |
César Muñoz |
| Trig Identities: Double Angle Formulas | trig@rig_basic |
sin2a, cos2s |
David Lester |
| Pythagorean Property - Sine and Cosine | trig@trig_basic |
sin2_cos2 |
David Lester |
| Trig Identities: Sum and Diff of Two Angles | trig@trig_basic |
sin_plus |
David Lester |
- César Muñoz, NASA, USA
- Víctor Carreño, NASA, USA
- Ricky Butler, NASA, USA
- Gilles Dowek, INRIA, France
- Alfons Geser, HTWK Leipzig, Germany
- Ben Di Vito, NASA, USA
- David Lester, Manchester University, UK
- John Siratt, University of Arkansas at Little Rock, USA
- Anthony Narkawicz, NASA, USA
- Radu Siminiceanu, NIA, USA
- Mariano Moscato, NIA & NASA, USA
- Sam Owre, SRI, USA
- César Muñoz, NASA, USA
