b'@online{TeuckeWeidenbacharXiv2015,'b"\nTITLE = {First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation},\nAUTHOR = {Teucke, Andreas and Weidenbach, Christoph},\nLANGUAGE = {eng},\nURL = {http://arxiv.org/abs/1503.02971},\nEPRINT = {1503.02971},\nEPRINTTYPE = {arXiv},\nYEAR = {2015},\nABSTRACT = {Counterexample-guided abstraction refinement is a well-established technique in verification. In this paper we instantiate the idea for first-order logic theorem proving. Given a clause set $N$ we propose its abstraction into a clause set $N'$ belonging to a decidable first-order fragment. The abstraction preserves satisfiability: if $N'$ is satisfiable, so is $N$. A refutation in $N'$ can then either be lifted to a refutation in $N$, or it guides a refinement of $N$ and its abstraction $N'$ excluding the previously found refutation that is not liftable.},\n}\n"