%%%%%% % Assignment: PVS exercises; Deadline: Dec, 7th, 2007. %%%%%% simple : THEORY BEGIN p,q,r: bool % Proposition names arb: TYPE+ arb_pred: TYPE = [arb -> bool] a,b,c: arb x,y,z: VAR arb % Variables of type arb P,Q,R: arb_pred %%% Questions %%% %%% Section 1: %%% % Use the typecheck command M-x tc. Correct the following mistakes %%% % error_1: LEMMA (P AND q) => (p and q) % error_2: LEMMA ((not p => q) => r %% Section 2: % Prove all of the following using only flatten and split. %%% section2_1: LEMMA (( p=>q ) AND p) => q section2_2: LEMMA ((p AND q) AND r) => (p AND (q AND r)) section2_3: LEMMA (p => (q => r)) IFF (p AND q => r) section2_4: LEMMA (p AND (q OR r)) IFF (p AND q) OR (p AND r) section2_5: LEMMA (p OR (q AND r)) IFF (p OR q) AND (p OR r) section2_6: LEMMA ((p => q) => (p AND q)) IFF ((NOT p => q) AND (q => p)) section2_7: LEMMA ((p AND q) AND ((p => r) OR (q => r))) => r section2_8: LEMMA ((NOT p => q) AND (NOT q => NOT p) AND (q => p)) => (p AND q) %%% % Section 3: % Prove using only flatten, split, skolem and inst % Do NOT use (skosimp*) or (inst?). You can use previously proven lemmas, %i.e. if you have a proof of quant_0 you can use it for quant_3. Using %lemmas unnecesarily complicates your proof. %%% quant_0: LEMMA (FORALL x: P(x)) => P(a) quant_1: LEMMA ((FORALL x: P(x) => Q(x)) AND P(a)) => Q(a) quant_2: LEMMA (FORALL x: P(x)) => (EXISTS y: P(y)) quant_3: LEMMA (FORALL x: P(x)) OR (EXISTS y: NOT P(y)) quant_4: LEMMA NOT (FORALL x: P(x)) IFF (EXISTS x: NOT P(x)) quant_5: LEMMA NOT (EXISTS x: P(x)) IFF (FORALL x: NOT P(x)) quant_6: LEMMA (FORALL x: P(x)) AND (FORALL x: Q(x)) IFF (FORALL x: P(x) AND Q(x)) quant_7: LEMMA (EXISTS x: P(x)) OR (EXISTS x: Q(x)) IFF (EXISTS x: P(x) OR Q(x)) quant_8: LEMMA ((FORALL x: P(x) OR Q(x)) AND (EXISTS x: NOT Q(x))) => EXISTS x: P(x) END simple