We present methods for automatically proving theorems in theories axio
matized by a set of Horn clauses. These methods address both deductive
and inductive reasoning. They are based on the concept of simplificat
ion and require minimal human interaction.