Inductive theorem proving via abstraction