Re: beginner's question: Difference between CWA and NAF

Sorry, I wrote NFA twice instead of NAF :-!
Bye

"Mauro Di Nuzzo" <picorna@xxxxxxxxx> ha scritto nel messaggio
news:m9qMe.19427$HM1.549234@xxxxxxxxxxxxxxxxxxxxx
> Hi.
> I think you have to distinguish between theory (logic and programming
> languages) and practice (Prolog, in this case).
> CWA deals mostly with theory, NFA with practice. Many correct theoretical
> issues have to be modified (or even re-thought) to be implemented in
Prolog.
> This is done mostly to avoid Prolog's infinite loops.
> Consider, for example, a simple program based on the transitive rule:
>
> p(a,b).
> p(b,c).
> p(X,Y) :- p(X,Z), p(Z,Y).
>
> In this case the goal
>
> ?- p(a,c).
>
> succeeds (Z being b).
> Now consider the following goal:
>
> ?- p(u,v).
>
> According to CWA this is obviously false, but its falsity cannot be
assessed
> with NFA, because of an infinite loop.
> Prolog engine tries to prove the following:
> 1) p(u,_1), p(_1,v).
> 2) p(u, _2), p(_2, _1), p(_1,v).
> 3) and so on...
> So, it simply cannot never "decide".
> Doesnt this appear to be strange, but quite obvious?
>
> Cheers,
> M
>
>
>
> "DaMenge" <c-programming@xxxxxxxxxxxxxx> ha scritto nel messaggio
> news:1124181289.469681.224710@xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> > Hi, thanks for your answer !
> >
> > Mauro Di Nuzzo schrieb:
> > > CWA (Reiter, 1978), also called "negation as infinite failure", is a
> > > mechanism that allow us to draw negative conclusions based on the lack
> of
> > > positive information.
> > > NAF (Clark, 1978), also called "negation as finite failure", is a
weaker
> > > notion of CWA in which "false" means FINITELY failed.
> >
> > So you mean NAF is a Top-Down-progress ?
> > on every substitution given, it'll ask the SLD-tree down?
> > Then how can it decide wether it do fail finitely or not (ain't that
> > undecidable?)
> >
> > >
> > > A very very stupid example is the following.
> > >
> > > f(a).
> > > f(b).
> > > f(X) :- f(X).
> > >
> > > "not f(c)" follows from CWA, but cannot be concluded by NAF (the
> SLD-tree is
> > > infinite).
> >
> > ok, then we need a "safe" rule like:
> > p(X) :- s(X), not f(X).
> > (and another fact like s(c). )
> >
> > but this would be a program with stratifikation, therefore all provable
> > facts of f can be found by a bottom-up progress like fixpoint
> > iteration.
> > (this should be equivalent to an infinite top-down progress by CWA, or
> > am I wrong?)
> > And after that the p(x) line is computable.
> >
> > Of course - like you said : CWA is used to compute all provable facts.
> > But how can NAF work when only using a top-down SLD-tree?
> > I thought NAF was created to simply compute the given negation, but
> > isn't it undecideable ?
> >
> > >
> > > Please consider to search on the net... g**gle
> >
> > Believe me , I did...
> >
> > But thank you again for your answer - now I see some difference between
> > NAF and CWA ..
> >
>
>


.

Relevant Pages

  • Re: beginners question: Difference between CWA and NAF
    ... CWA deals mostly with theory, ... issues have to be modified to be implemented in Prolog. ... This is done mostly to avoid Prolog's infinite loops. ... > But how can NAF work when only using a top-down SLD-tree? ...
    (comp.lang.prolog)
  • Re: beginners question: Difference between CWA and NAF
    ... > notion of CWA in which "false" means FINITELY failed. ... facts of f can be found by a bottom-up progress like fixpoint ... Of course - like you said: CWA is used to compute all provable facts. ... But how can NAF work when only using a top-down SLD-tree? ...
    (comp.lang.prolog)
  • Re: beginners question: Difference between CWA and NAF
    ... CWA, also called "negation as infinite failure", is a ... notion of CWA in which "false" means FINITELY failed. ... but cannot be concluded by NAF (the SLD-tree is ... > negation then one can conclude the assumptions made by CWA" ...
    (comp.lang.prolog)
  • Re: beginners question: Difference between CWA and NAF
    ... negation then one can conclude the assumptions made by CWA" ... by checking all positive substitutes given by that s-literal in q to be ... NAF) first? ...
    (comp.lang.prolog)