Semantics and Proof Procedure for Abductive Logic Programming

点击翻译按钮获取中文摘要

Semantics of general logic programs may be defined by both 2-valued stable and 3-valued stable models, while SLDNF resolution (SLD resolution with negation as failure) is adopted as a procedure for the completion of general logic programs. When SLDNF resolution was well-organized as a basis of abductive proof procedure (Eshghi and Kowalski procedure), it was firstly examined whether the procedure is sound with respect to 2-valued stable model. However, it has been proved to be sound with respect to-3-valued stable model (Dung, 1991).This research project is concerned with a generalization of negation as failure to be made use of for an abductive proof procedure, and an abduction framework in 3-valued logtic, a generalization of Eshghi and Kowalski framework.When applying negation as failure, we usually take a safe ruls :*(]SY.reverse left half-bracket.[)A suceeds if * A finitely fails, and*(]SY.reverse left half-bracket.[)A finitely fails if * A succeeds,where A is a ground atom. To ge … More t non-ground abducibles, we rather take Shepherdson's rule (a non-safe rule) :*(]SY.reverse left half-bracket.[)Arheta succeeds if * Arheta finitely fails for some substitution rheta, and*(]SY.reverse left half-bracket.[)A finitely fails if * A succeeds with the empty substitution,for an abductive proof procedure. Soundness of a refined abductive proof procedure is proven with respect to a general 3-valued stable model, which is defined over a domain containing variables.As another aspect, we have an abduction framework in 3-valued logic, where an integrity constraint is organized so that it may induce a generalized abductive proof procedure, which involves an adjustment to deal with any proposition to be neither an abducible nor derived from the theory and the abducibles. The integrity constraint is proved to be in a close relationship with a 3-valued stable model.This reoport comprises these two aspects in three parts :(1) Semantics for logic programs.(2) Refinements of SLDNF resolution.(3) Generalizations of abductive procedures and abduction framework. Less