hide
Free keywords:
Computer Science, Logic in Computer Science, cs.LO
Abstract:
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.
