Resumen
This article relates to automated reasoning strategies that help in fast and flawless logical reasoning. The author holds that imperfect reasoning gives rise to many problems like bugs in computer programs, flaws in chip designs and errors in mathematical proofs. Automated reasoning, according to the author, is a one step solution to all these problems. The focus of automated reasoning is the design and implementation of computer programs that flawlessly apply logical reasoning to reach the objective, irrespective of the area of interest. The significance of reasoning programs like OTTER, an automated reasoning program, can be easily determined by the fact that they have also been used by educators in undergraduate logic courses and in graduate level courses for interactive theorem proving, besides their being, by their very nature, a perfect assistant in puzzle solving. Further, automated reasoning programs don't use instantiation to draw conclusions but logical unification always remains at the core of these programs.