Re: car color defaults: a story about Scoped Negation As Failure/log:notIncludes

> > In fact, every use of default negation *always* had a clear 
> > scope and I am not aware of anyone who (thoughtfully) advocated 
> > default negation and imagined otherwise.
> 
> I guess Dan and others are concerned about making the
> scope explicit in the object language.

Absolutely. It can't be reasonably dealt with without giving the scope in
one way or another.

> This is indeed an option that is not supported by traditional formal LP
> languages (although it is supported by Prolog's metaprogramming
> capabilities).

You can say that Prolog supports this, although in a rudimentary way.
Predicates belong to modules explicitly, and when you are negating them you
are closing off with respect to an explicit scope.

Some prologs are better than others in this respect.

What is missing is open-endedness: the ability to associate modules with
different data sources, to query over different modules, etc.

> But you (Michael) say 
> that FLORA-2 supports making the scope explicit, right? 
> Maybe you can give us an example how this looks like 
> in FLORA-2 and what it means in the underlying formal
> semantics? 

FLORA-2 has the concept of modules, which identify various pieces of the
knowledge base. Modules are dynamic - their contents can come from
anywhere, e.g., a web site.

When you call a literal (positive or negative), you have to specify the
module in which the definition of the literal exists. (If you don't
specify, then the module is the same as the caller module.)

One simple way to give this semantics is to assume that predicates in
the heads of the rules in any given module have some prefix that is unique
to that module. This disambiguates the predicates that have the same name,
but are defined in different modules.
A direct model-theoretic semantics is also easy to give.

Now, when you have something like  "not foo@bar" in the body of a rule,
it is true/false iff foo is false/true according to the KB specified in
the module bar.

So, the scope of the definition of every literal, positive or negative, is
explicit.  You can also leave the module to be a variable. In this case,
you are asking an open question. But this is not allowed for negative
calls.

Note that a similar mechanism exists in Triple, although they don't have
negation as far as I know and modules are rigidly defined there. I think
Ontobroker now also has (or is about to have) the same thing.

This mechanism is very general (both in FLORA-2 and Triple), although it
may need to be extended for the Web rules language. E.g., hierarchies of
modules. Triple already supports a simple algebra of modules (again, for
positive literals only). I am not yet sold on that idea, but these are just
details in the big schema of things.


> > Finally, I would like to say once again that the term 
> > "negation as failure" is bad and misleading. 
> > Traditionally, negation as failure meant the
> > particular strategy used in Prolog. NAF is just one 
> > of the known forms of default negation.
> 
> Why should the term "default negation" be better and 
> less misleading than the term "negation as failure"?

It is better because it doesn't identify a specific and well-defined 
concept (the NAF), which exists for over 30 years now, with a class of
concepts (which include NAF, WFS, stable models, etc.; the K operator in DL
extensions can also be said to belong here).

Perhaps a different and better term could be invented, but anything is
better than NAF.

> I think the latter says more about the meaning of NAF
> than the former.

No it doesn't. NAF is adequately describing the original NAF concept (as in
Prolog). It doesn't describe what is happening in case of WFS or stable models.
With (the original) NAF, there is an inference rule, SLD, which is being
tried, and failure to prove according to this procedure is interpreted as
negation.

With WFS and SM, there is no proof procedure of any kind.
Both of these are model-theoretic concepts -- not proof-theoretic -- concepts.
The alternating fixpoint can hardly be called "an inference rule," and
stable models are even further away in this dimension. (OK, there is also
SLG for WFS, but even that is hard to call "an inference rule.")


	--michael  


> -Gerd
> 
>

Received on Thursday, 7 July 2005 22:28:43 UTC