%%% NAME/LOGIN-ID _____________________/______________________ %%% ACKNOWLEDGMENTS: %%% %%% =============== %%% Predicate Logic - Propositional formulas involving quantifiers %%% =============== %%% %%% Prove these using only (SPLIT), (FLATTEN), (INST) and (SKOLEM) commands %%% ~~~~ th_B: THEORY BEGIN U: TYPE+ % Arbitrary nonempty type a,b,c: U % Constants of type U x,y,z: VAR U % Variables of type U P,Q,R: [U -> bool] % Predicate names B_0: LEMMA (FORALL x: P(x)) => P(a) B_1: LEMMA ((FORALL x: P(x) => Q(x)) AND P(a)) => Q(a) B_2: LEMMA (FORALL x: P(x)) => (EXISTS y: P(y)) B_3: LEMMA (FORALL x: P(x)) OR (EXISTS y: NOT P(y)) B_4: LEMMA NOT (FORALL x: P(x)) IFF (EXISTS x: NOT P(x)) B_5: LEMMA NOT (EXISTS x: P(x)) IFF (FORALL x: NOT P(x)) B_6: LEMMA (FORALL x: P(x)) AND (FORALL x: Q(x)) IFF (FORALL x: P(x) AND Q(x)) B_7: LEMMA (EXISTS x: P(x)) OR (EXISTS x: Q(x)) IFF (EXISTS x: P(x) OR Q(x)) END th_B