COSC3302	    		Program-2
	                    Propositional Logic Validity Checker 		
								Due: Part-I: 2/26/2013  
							     	     Final:  3/7/2013.

	Consider a set of WFF's of Propositional Logic consisting of
		NOT
		AND
		OR
		->
		Predicate Symbols (where each symbol consists of
		                    one or more capital letters)

	Task:
	Write a well-documented program to check the validity (i.e.,
	whether a tautology or not) of each input formula and print out
	the input formula and the result.

	Requirements:

	1. For each input formula, output the following:
		The input formula.
		Indication of whether the formula is valid or invalid.
	2. Use the following input formulas for the PART-I Results:
		A AND B AND C AND NOT A -> D OR E OR F
		A AND B AND C -> D OR E OR NOT F 
	   (So, for PART-I, the only eliminations you may be concerned with include
		a. NOT occurring on either side of an implication
		b. AND occurring on the antecedent
		c. OR occurring on the consequent and
		d. IMPLICATION occurring on the consequent.)
	3. Use the following input formulas for the Final Results:
		(W OR S) AND (W ->M) AND (S -> B) AND NOT B -> M
		(A OR B) AND (A -> C) AND (B -> D) -> (C OR D)
		(A AND B) AND (A -> C) AND (B -> D) -> (C AND D)
		(A OR B) AND (A -> C) OR  (B -> D) -> (C OR D)
		(A -> B -> C->D) AND NOT F  -> ((A->B->C) -> D)
		(( X -> Y -> Z))  -> ((( X  -> (Y->Z) )))
   		((X->(Y->Z)))   -> ((X->Y) -> Z)
	
	Elimination rules:

	1. NOT(A).B ---> C
		B ---> C + A
	2. (A.B).C ---> D
		A.B.C ---> D
	3. (A+B).C ---> D
		(A.C ---> D).(B.C ---> D)
	4. (A ---> B).C ---> D
		(C--->D+A).(C.B--->D)
	5. A ---> NOT(C) + B
		A.C ---> B
	6. A ---> B.C + D
		(A ---> B + D) . (A ---> C + D)
	7. A ---> (B ---> C) + D
		A.B ---> C + D
	8. A ---> (B + C) + D
		A ---> B + C + D