Re: log:notIncludes (conclusion?)

Sandro Hawke <sandro@w3.org>:
> 
> > > > This is nonmonotonic.
> > > 
> > > I'm not sure I know the right words for this, but that stuff sitting
> > > at that URL is considered immutable within one inference run.  cwm
> > > makes no attempt to read it more than once; any change in it would go
> > > along with an overall change in the state of the world.  A
> > > long-running N3-based agent would have to start everything over each
> > > delta-t (or cleverly act like it did).  Each time something observable
> > > about the universe changes, we're talking about a new set of models
> > > and interpretations.
> > 
> > Yes, but this is no different from the way Prolog (without assert/retract)
> > works. You read the KB only once and then make NAF-based inferences. The KB
> > doesn't change.
> > 
> > Nonmonotonicity doesn't mean that you are going to change the KB during the
> > run.  It means that you make your inferences on a static KB with one set of
> > models and observe the results. Then, some time later (after you are done
> > with the inference) the KB changes. You reload your KB (or whatever the
> > mechanism is for becoming aware of the change; it is more efficient in
> > Prolog, of course) and recompute your models (again, assuming that the KB
> > doesn't change during the inference). Then you observe the results again.
> > Nonmonotonicity means that it is possible that when you observe the result
> > the second time you may not find some inferred formulas that you saw when
> > you observed the result the first time.
> 
> I think you left out the restriction that the only changes to the KB
> made between runs are to add formulas.

Yes, sorry.

> Adding to a document which is
> referred to via log:semantics and then log:notIncludes is not adding
> to the KB.  Unfortunately, I'm not sure what exactly it is, logically
> speaking. 

This is related to this message:
http://lists.w3.org/Archives/Public/public-rule-workshop-discuss/2005Aug/0112.html

There is no semantics for log:semantics, and I was trying to bring a
semantics one step closer. Otherwise, there is no point discussing whether
N3 is monotonic or not.


> Logically speaking, how do you talk about XSB's
> file_exists/1 or cputime/1 ?

Oh, these can be defined easily. file_exists/1: you can think of a file
system as a database that describes the status of various files.
Then file_exists/1 is just a very simple query.
cputime/1: this is related to the dynamics of execution and therefore
requires a logic that can deal with such things. It can be formalized using
Transaction Logic or Temporal Logic.

Of course, probably nobody did such a formalization before (certainly not
the Prolog standard), but then I am free to invent my own formalization,
which agrees with the observable behavior of these predicates. I was trying
to do the same with your semantics/2 predicate.


> > > Going back to the definition of monotonicity you and DanC were using
> > > [1], the stuff sitting at that URL isn't part of A or B.  Nothing is
> > > entailed by that stuff at the URL.  To be slightly silly, adding a
> > > formula to it is no more relevant to the notion of monotonicity than
> > > is adding characters to the end of some constant symbol in an FOL
> > > formula.
> > 
> > If nothing is inferred from formulas at URL then you are not dealing with
> > semantics or logic. You are just manipulating lists and checking for their
> > inclusion.
> 
> I think it's pretty fair to say N3/cwm is just manipulating lists and
> checking for their inclusion with this stuff.

Well, then there is no point talking about NAF, SNAF, or anything like
that.  You simply have a concrete domain of lists, and log:includes and
log:notIncludes are simply built-in predicates, i.e., predicates with one
fixed (unchangeable) interpretation.  There is no "failure to prove" in
log:notIncludes, and calling it SNAF is misleading.

> There are some other features which are more logical, like telling it
> to automatically load the data from URIs it sees in certain contexts,
> and log:definitiveDocument which says that all true atomic formulas
> using a given predicate are in the data returned from a given web
> address.   Perhaps that's what we should focus on.   (Or maybe we
> should move back to what the charter can or should say about all
> this.) 

It seems that this definitiveDocument thing leads to SNAF, and exhibits
nonmonotonic behavior. I am not quite sure how to make a correct use of
this predicate, but I assume that if p/1 is defined by a definitive document
then not p(X) is a SNAF. Then I can write

    q(X) :- not p(X).

and we get nonmonotonicity: if we add something to p/1 then we might loose
something about q/1.


> > But I don't believe that nothing is entailed from those formulas.  What
> > about your pharmacy example? You have two sets of rules sitting at two
> > different sites that describe two different medicines. (Or whatever it
> > was.) You pull those rules together and make inference that tells you that
> > there is a possible side effect. So, these formulas at A and B are used as
> > logical formulas and you are making inference from them.
> 
> That's not done with any of these features.  That's most simply done
> by running cwm like
> 
>   bash$  cwm http://pharma-data-1.example.com http://pd2.example.com $Q
> 
> (where $Q will be inference-control and query parameters)
> 
> Of course that's conceptually the same as 
> 
>   bash$  cat http://pharma-data-1.example.com http://pd2.example.com | cwm $Q
> 
> except that of course cat doesn't handle URLs, and the information for
> handling relative URIs in the content would be lost.

OK. I thought that you meant to use something like log:semantics.

By the way, the above use of cwm to merge rules clearly shows that the
issue has nothing to do with the presence or absence of monotonicity.


> There's probably a way to use log:semantics and de-reify and assert
> the retrieved data, but I'm not sure.   I should say that I'm
> not arguing that cwm is better than runflora or anything, I'm just
> hoping that we can identify the features and use cases causing some
> apparent disagreements about the charter.  I think we're close.

Sure. I think we are making progress. The issue was really reaching a
high-level technical consensus. My point was that SNAF is nonmonotonic, if
you give it a logical semantics, and therefore the draft was contradictory.
Your additional examples make me even more convinced that cwm/N3 is
nonmonotonic (in its informal semantics) even though you may not have
realized that. Since cwm, Flora-2, Prolog, etc., are real practical
languages, it seems a clear indication that nonmonotonicity is an important
feature of a web rule language.


	--michael

Received on Saturday, 27 August 2005 21:45:42 UTC