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 b…