Grounding informal proof techniques in logic (read it in Portugese)
 Home Short bio texts by Gries Interactive programming exercises Teaching OO using Java Calculational logic festive occasions ABC book CS Faculty over the years CS@Cornell The Triple-I Administration How Bush Operated

One of the objects of our rigorous approach to proof is to explain how informal proof methods are grounded in logic. In Chapter 4 of A Logical Approach to Discrete Math, we explain how each informal technique has a solid foundation underneath it, in the form of a theorem or metatheorem. Here is a list of informal techniques together with the theorems on which they are based.

• Assuming the antecedent: Based on the Deduction Metatheorem.
• Case analysis: (p | q) & (p => r) & (q => r)  =>  r.
• Partial evaluation (if P[z:= true] and E[z:= false] are theorems, then so is P):

P[z:= p] == (p & E[z:= true]) & (~p & E[z:= false])
• Mutual implication: (p == q)  ==  (p => q) & (q => p).
• Proof by contradiction: ~p => false  ==  p.
• Proof by contrapositive: p => q  ==  ~q => ~p.