Intuitive Minimal Abduction in Sequent Calculi

Some computational issues on abduction are discussed in a framework of the first order sequent calculus. Starting from revising the meaning of “good” abduction, a new criterion of abduction called intuitive-minimal abduction (IMA) is introduced. An IMA is an abductive formula equivalent to the minimal abductive formula under the theory part of a sequent and literally as simple as possible. Abduction algorithms are presented on the basis of a complete natural reduction system. An abductive formula, obtained by the algorithms presented in this paper, is an IMA if the reduction tree, from which the abduction is performed, is fully expanded. Instead of using Skolem functions, a term-ordering is used to indicate dependency between terms.