Intuitive Minimal Abduction in Sequent Calculi  

作　　者：伊波 陶先平 等 

机构地区：[1]InstituteofComputerSoftware,NanjingUniversity,Nanjing210093,P,R.China [2]StateKeyLaboratoryforNovelSoftw

出　　处：《Journal of Computer Science & Technology》1998年第3期209-219,共11页计算机科学技术学报（英文版）

摘　　要：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 papert 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.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 papert 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.

关 键 词：ABDUCTION sequent calculus ALGORITHM 

分 类 号：G434[文化科学—教育学]