Assignment 6

1 files changed, 58 insertions, 0 deletions

diff --git a/assignment6/A.pvs b/assignment6/A.pvs
new file mode 100644
index 0000000..844e867
--- /dev/null
+++ b/assignment6/A.pvs
@@ -0,0 +1,58 @@
+%%%
+%%%    NAME/LOGIN-ID _____________________/______________________
+%%%
+%%%    ACKNOWLEDGMENTS:
+%%%      * List the names of people whom you worked with or who helped you
+%%%        with this assignment
+%%%      * Cite any references you used to complete this work
+%%%
+%%%    ===================
+%%%    Propositional Logic
+%%%    ===================
+%%%    
+%%%    Prove these theorems using only the (SPLIT) and (FLATTEN) commands
+%%%                               ~~~~
+
+th_A: Theory
+
+BEGIN
+
+%%% Elementary propositions.
+%%%
+
+p,q,r: bool
+
+%%% 
+%%% Propositional Formulas
+%%%
+%%%   (CLAIM, CONJECTURE, ..., THEOREM all mean the same thing)
+%%% 
+
+A_0: CLAIM  ((p => q) AND p) => q
+
+A_1: CONJECTURE  ((p AND q) AND r) => (p AND (q AND r))
+
+A_2: COROLLARY  NOT (p OR q) IFF (NOT p AND NOT q)
+
+A_3: FACT  NOT (p AND q) IFF (NOT p OR NOT q)
+
+A_4: FORMULA  (p => (q => r)) IFF (p AND q => r)
+
+A_5: LAW  (p AND (q OR r)) IFF (p AND q) OR (p AND r)
+
+A_6: LEMMA  (p OR (q AND r)) IFF (p OR q) AND (p OR r)
+
+A_7: PROPOSITION  ((p => q) AND (p => r)) IFF (p => (q AND r))
+
+A_8: SUBLEMMA  ((p => q) => (p AND q)) IFF ((NOT p => q) AND (q => p))
+
+A_9: THEOREM  ((p OR q) AND r) => (p AND (q AND r))
+
+A_10: CLAIM p => (q => p)
+
+A_11: CLAIM ((p => (q => r)) => ((p => q) => (p => r)))
+
+A_12: CLAIM ((NOT q) => (NOT p)) => (((NOT q) => p) => q)
+
+END th_A
+