From 09a4e4438c7a834df9b44c134cbdacc040411c59 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Fri, 11 Mar 2016 15:26:17 +0100
Subject: Assignment 6

---
 assignment6/B.pvs | 44 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 44 insertions(+)
 create mode 100644 assignment6/B.pvs

(limited to 'assignment6/B.pvs')

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
-- 
cgit v1.2.3