The formalization of abductive reasoning has received increasing attention from logicians. However, few work is found beyond abduction in propositional logic, given that in a first order formalism, the undecidability problem naturally appears, and therefore an abductive problem cannot even be appropriately formulated. Still, many applications in artificial intelligence allow finite domains to work with, and this gives an opportunity to apply abduction in first order logic with restricted domains. In this paper, we present an approach to abductive reasoning in (...) C-structures, first order structures with a finite domain in which each of its elements has a corresponding constant representing its interpretation. By using semantic tableaux with bounded depth, that is, C-tableaux (a modification of N-tableaux, introduced by the authors in previous papers) and δ-resolution calculus, we build an effective procedure for the searching of minimal abductive solutions within the proposed semantics. (shrink)

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]. (shrink)