CIS301 Friday, March 7 Write a proof of this sequent: (p ^ q) -> r, q |- p -> r 1. (p ^ q) -> r premise 2. q premise +--------------------------------- | 3. p assumption | 4. p ^ q ^i 3,2 | 5. r ->e 1,4 +-------------------------------- 6. p -> r ->i 3-5 Tactic: Goal was p -> r , so we need a box with assumption p and we try to prove r at the end of the box. Finish with ->i on the last line. The above proof is a program! To see why, let: p == int q == string r == bool Then, from the library components (global vars), public bool doStuff(int x, string y) // (int ^ string) -> bool, and string data // string // |- we built this program: public bool myProc(int z) // int -> bool The code/proof: // 1. presume doStuff is a global var // 2. presume data is a global var public bool myProc(int z) { // 3. assume you have an int param, z Tuple args = (z, data) // 4. introduce a pair/tuple (^i) bool ans = doStuff(args) // 5. call doStuff with the pair (->e) return ans // and get the bool, ans } // 6. end function def (->i) THE C# TYPE CHECKER IS A PROOF CHECKER FOR PROPOSITIONAL LOGIC.