We propose a new negation rule for logic programming which derives existentially closed negative literals, and we define a version of completion for which this rule is sound and complete. The rule is called "Negation As Instantiation" (NAI). According to it, a negated atom succeeds whenever all the branches of the SLD-tree for the atom either fail or instantiate the atom. We formalize this way of handling negation in terms of SLDNI-resolution (SLD-resolution with Negation as Instantiation). Finally, we amalgamate SLDNI-resolution and SLDNF-resolution, thus obtaining a new resolution procedure which is able to treat negative literals with both existentially quantified variables and free variables, and we prove its correctness.
Negation as Instantiation
DI PIERRO, ALESSANDRA;
1995-01-01
Abstract
We propose a new negation rule for logic programming which derives existentially closed negative literals, and we define a version of completion for which this rule is sound and complete. The rule is called "Negation As Instantiation" (NAI). According to it, a negated atom succeeds whenever all the branches of the SLD-tree for the atom either fail or instantiate the atom. We formalize this way of handling negation in terms of SLDNI-resolution (SLD-resolution with Negation as Instantiation). Finally, we amalgamate SLDNI-resolution and SLDNF-resolution, thus obtaining a new resolution procedure which is able to treat negative literals with both existentially quantified variables and free variables, and we prove its correctness.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
