COSC5100 Validity Checker Examples 1/22/2003 EX1: (A->B->C) -> (A->(B->C)) The number in parenthesis indicates the number of parts of the formula, either Anti or Cons. Parts in Anti are really their conjunctions while parts in Cons are their disjunctions, of course. A. Anti(0) Cons(1): (A->B->C) -> (A->(B->C)) B. CIMP Anti(1): A->B->C Cons(1): A->(B->C) C. AIMP: 2 implications (Their conjunction) 1. Anti(1): C Cons(1): A->(B->C) 2. Anti(0): Cons(2): A->(B->C) A->B D. Now consider just the first implication Anti(1): C Cons(1): A->(B->C) E. CIMP: Anti(2): C A Cons(1): B->C F. CIMP: Anti(3): C A B Cons(1): C At this time, the first implication's elimination is done. So, we check if any one variable occurs in both Anti and Conseq. The variable C does. So, it is valid. Now, we check go ahead to check for the second implication. Of course, if the first implication were not valid, we would be done as the whole formula is found not to be VALID. G. Anti(0) Cons(2): A->(B->C) A->B CIMP: Anti(1): A Cons(2): B->C A->B H. CIMP: Anti(2): A B Cons(2): C A->B I. CIMP: Anti(3): A B A Cons(2): C B Now, the second implication is done. And, as we check to see if a variable occurs in both Anti and Cons, it is 'B' that does occur in both. As all implications (2 of them, in this case) are Valid, the original formula is found to be valid. EX2: (A->B) AND (B->C) -> (A->C) A. Anti(0) Cons(1): (A->B) AND (B->C) -> (A->C) B. CIMP: Anti(1): (A->B) AND (B->C) Cons(1): A->C C. AAND: Anti(2): A->B B->C Cons(1): A->C D. AIMP: We get 2 implications. 1. Anti(2): B B->C Cons(1): A->C 2. Anti(1): B->C Cons(2): A->C A E. Again, we consider the first implication: Anti(2): B B->C Cons(1): A->C F. AIMP: So, we get two implications: 1-1. Anti(2): B C Cons(1): A->C 1-2. Anti(1): B Cons(2): A->C B G. Consider 1-1 above. Anti(2): B C Cons(1): A->C G1. CIMP: Anti(3): B C A Cons(1): C G2. Now this implication is over and it is VALID H. Now consider 1-2 above. Anti(1): B Cons(2): A->C B H1. CIMP: Anti(2): B A Cons(2): C B H2. Now this implication is over and VALID. I. Now consider the second implication of step D above. Anti(1): B->C Cons(2): A->C A CIMP: (Although it is also a case of AIMP) Anti(2): B->C A Cons(2): C A J. AIMP: So we get 2 implications. 2-1: Anti(2): C A Cons(2): C A 2-2: Anti(1): A Cons(3): C A B K. From inspection, we see that both implications, 2-1 and 2-2, are done and they are both VALID. So, the original formula, EX2, is VALID, as we expect.