We study termination properties of normal logic programs where negation as failure is interpreted as a form of abduction, as originally proposed by Eshghi and Kowalski in [EK89]. The abductive proof procedure associated with this interpretation exhibits a better behavior than SLDNF as far as termination is concerned. We first present a strong termination characterization for the Eshghi and Kowalski proof procedure for Datalog programs which is sound and complete. We then extend the characterization to the class of non-Datalog programs, and prove its soundness. Finally we present two instantiations of the general characterization and study the relationships between the classes of programs introduced in the paper.
Negation as Failure through Abduction: Reasoning about Termination
MANCARELLA, PAOLO MARIA;PEDRESCHI, DINO;RUGGIERI, SALVATORE
2002-01-01
Abstract
We study termination properties of normal logic programs where negation as failure is interpreted as a form of abduction, as originally proposed by Eshghi and Kowalski in [EK89]. The abductive proof procedure associated with this interpretation exhibits a better behavior than SLDNF as far as termination is concerned. We first present a strong termination characterization for the Eshghi and Kowalski proof procedure for Datalog programs which is sound and complete. We then extend the characterization to the class of non-Datalog programs, and prove its soundness. Finally we present two instantiations of the general characterization and study the relationships between the classes of programs introduced in the paper.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.