Support definitions and properties for aviation-related formalizations.
Restrictions/Assumptions:
- no roll, i.e., instantaneous change to target bank angle (from 0)
- constant ground speed, i.e., constant track rate
- constant vertical speed
Notes:
- turn dynamics are determined by the bank angle and ground speed
- turn elements: speed, bank angle, radius, track rate
- bank angles can be signed (positive:right) or unsigned
| Theorem | Location | PVS Name | Contributors |
|---|
- Radu Siminiceanu, NIA, USA
- Ricky Butler, NASA, USA
- César Muñoz, NASA, USA
- Aaron Dutle, NASA, USA
- Mariano Moscato, NIA & NASA, USA
- Sam Owre, SRI, USA
- César Muñoz, NASA, USA
