Assignment 6

1 files changed, 44 insertions, 0 deletions

diff --git a/assignment6/B.pvs b/assignment6/B.pvs
new file mode 100644
index 0000000..d4aad00
--- /dev/null
+++ b/assignment6/B.pvs
@@ -0,0 +1,44 @@
+%%%    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