First order abduction via tableau and sequent calculi

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 stdl 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 fai-iwg meta-logical and proof-theoretical questions. In this work the analysis of the concept * 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 prepositional case, two Hiff ̂ ^nt. rhjrrjfci-t ̂ rj'rjit.jffm * are given for abductive ^^rhniti""*! ~T^h of tr»»ra being the declarative counterpart of a different algorithm for the generation of explanations. The first one corresponds t