© 1993 by Oxford University Press
Original Articles |
First order abduction via tableau and sequent calculi
Dipartimento di Informatica e Sistemistica, Università di Roma "La Sapienza" via Salaria 113, 00198 Roma, Italia E-mail: cialdea.pirri{at}assi.ing.uniromal.it
The formalization of abductive reasoning is still an open question: there is no general agreement on the boundary of some basic concepts, such as preference criteria for explanations, and the extension to first order logic has not been settled.
Investigating the nature of abduction outside the context of resolution based logic programming still deserves attention, in order to characterize abductive explanations without tailoring them to any fixed method of computation. In fact, resolution is surely not the best tool for facing meta-logical and proof-theoretical questions.
In this work the analysis of the concepts involved in abductive reasoning is based on analytical proof systems, i.e. tableaux and Gentzen-type systems. A proof theoretical abduction method for first order classical logic is defined, based on the sequent calculus and a dual one, based on semantic tableaux. The methods are sound and complete and work for full first order logic, without requiring any preliminary reduction of formulae into normal forms. In the propositional case, two different characterizations are given for abductive explanations, each of them being the declarative counterpart of a different algorithm for the generation of explanations. The first one corresponds the generation of the whole set of minimal and consistent explanations, where minimality is checked by comparison with the other elements of the set. The second characterization corresponds to a (non-deterministic) algorithm for generating a single minimal explanation that is consistent with the theory.
The first order versions of the abductive systems make use of unification and dynamic herbrandization/skolemization of formulae. The construction of the abduced formula is pursued by means of de-skolemization. The first order methods are very loose in discarding explanations that are not minimal In fact, the question of minimality in first order abduction is a main issue. As usually defined, minimality is undecidable, for two different reasons: (i) determining whether an explanation is better than another one is in general undecidable; (ii) the set of explanations may be infinite. Moreover, because of (ii), a minimal element may not exist. Such problems suggest that the minimality requirement should be relaxed, possibly defining it w.r.t. a stronger relation than logical consequence.