  We present a modification of the superposition calculus that is meant to
generate explanations why a set of clauses is satisfiable. This process is
related to abductive reasoning, and the explanations generated are clauses
constructed over so-called abductive constants. We prove the correctness and
completeness of the calculus in the presence of redundancy elimination rules,
and develop a sufficient condition guaranteeing its termination; this
sufficient condition is then used to prove that all possible explanations can
be generated infinite time for several classes of clause sets, including many
of interest to the SMT community. We propose a procedure that generates a set
of explanations that should be useful to a human user and conclude by
suggesting several extensions to this novel approach.
