General Stable Model Semantics and SLDNF Resolution with Non-Safe Rule for Abduction

概要

論文の詳細を見る
It is shown in an abduction framework based on a general logic program [Eshghi 89, Kakas 92] that an abductive explanation for a given sentence might be provided by negation as failure when the negation of the sentence initiates an SLD resolution deduction. However, possibly non-ground explanations have never been expected. It is mainly because the SLDNF resolution (SLD resolution with negation as failure) is often restricted to keep a safe rule. In addition, only a case as a pragmatic example is to be extracted as an explanation for a query. In this paper, adopting non-safe SLDNF resolutions, we have an abduction framework in which a maximally general extension of abducibles is defined in terms of generality regarding the extensions. A general stable model semantics is firstly presented, to demonstrate the relation between the semantics of a program and the maximally general abductive extension, in the domain containing variables. A general stable model may denote a maximally general abductive extension which satisfies a constraint in abduction framework, while if a maximally general abductive extension satisfies the constraint then it may define a general stable model. We next prove that a non-safe SLDNF resolution is sound as an abductive proof procedure with respect to the maximally general extension of abducibles.
1997-03-01