Sciweavers

BIRTHDAY
2006
Springer

Reductio ad Absurdum: Planning Proofs by Contradiction

14 years 2 months ago
Reductio ad Absurdum: Planning Proofs by Contradiction
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?
Erica Melis, Martin Pollet, Jörg H. Siekmann
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where BIRTHDAY
Authors Erica Melis, Martin Pollet, Jörg H. Siekmann
Comments (0)