Sometimes it is pragmatically useful to prove a theorem by contradiction rather than finding a direct proof. Some reductio
ad absurdum arguments have made mathematical history and the general issue if and how a proof by contradiction can be replaced
by a direct proof touches upon deep foundational issues such as the legitimacy of tertium non datur arguments in classical
vs. intuitionistic foundations.
In this paper we are interested in the pragmatic issue when and how to use this proof strategy in everyday mathematics in
general and in particular in automated proof planning. Proof planning is a general technique in automated theorem proving
that captures and makes explicit proof patterns and mathematical search control. So, how can we proof plan an argument by
reductio ad absurdum and when is it useful to do so? What are the methods and decision involved?