Abstract
This papers presents δ-resolution, a dual resolution calculus. It is based on standard resolution, and used appropriate formulae equivalent to disjunctive normal forms, instead of conjunctive normal ones, as it is the case for resolution. This duality is then useful to create a calculus for abductive process, as a way to construct a set of abductive solutions. The proposed calculus is compared to semantic tableaux, an standard logical framework, aslo illuminating when studying abduction.δ-resolution calculus is a contribution to logic programming, and it further suggests new possibilities to explore abduction at a first order level, in the lines of those proposed in [9]