%%%        Aircraft Landing Weather Model
%%%     Examples and exercises for basic prover commands
%%%       (propositional formulas only)

landing_weather: THEORY
BEGIN

% Weather conditions near the ground

clear:  bool    % Minimal cloudiness
cloudy: bool    % Mostly cloudy skies
rainy:  bool    % Steady rainfall
snowy:  bool    % Includes sleet, freezing rain, etc.
windy:  bool    % Moderate wind speed

%  Relationships among conditions (use "lemma" command in proofs)

cond_ax1: AXIOM  rainy => cloudy
cond_ax2: AXIOM  snowy => cloudy
cond_ax3: AXIOM  clear IFF NOT cloudy

%  Definitions of landing conditions (use "expand" command in proofs)

ideal:     bool = clear AND NOT windy
favorable: bool = NOT rainy AND NOT snowy
adverse:   bool = rainy OR snowy

%%%   Propositional Formulas to prove  (for Exercise 3)

% Use the commands split, flatten, lemma, and expand to prove these lemmas.
% You could also try the support commands help, postpone, and undo.  You
% may use any of these lemmas in the proofs of lemmas appearing later in
% the theory.

weath_1: LEMMA  rainy => NOT clear

weath_2: LEMMA  snowy => NOT clear

weath_3: LEMMA  clear => favorable

weath_4: LEMMA  NOT cloudy => NOT snowy

weath_5: LEMMA  rainy => NOT ideal

weath_6: LEMMA  snowy => NOT ideal

weath_7: LEMMA  NOT cloudy => favorable

weath_8: LEMMA  ideal => favorable

weath_9: LEMMA  adverse => NOT favorable

weath_10: LEMMA  NOT adverse => favorable

weath_11: LEMMA  favorable IFF NOT adverse

weath_12: LEMMA  favorable OR adverse

END landing_weather