In this paper we present an abstraction-refinement framework for reasoning with large theories. We consider several types of abstractions based on over and under approximations of first-order theories. We implemented the proposed approached in a theorem prover iProver and evaluated over the TPTP library.