Re: log:notIncludes (conclusion?)

Sandro Hawke <sandro@w3.org>:
> 
> > Actually, there is nothing really clever in what Flora-2 or Triple do. :-)
> > What they do is not a semantic trick, but a syntactic one.  They allow the
> > user to specify the scope of any inference (positive or negation)
> > explicitly, but the semantics remains like in traditional systems.
> > (Actually, Triple didn't have SNAF originally -- only positive scoped
> > inference. I am not sure if some later versions of Triple have default
> > negation, but this is not important here.)
> >
> > I already hinted at how this is done when discussing Dan's example.
> > Basically, every rule-head (or fact) defined in a particular module
> > is treated as a predicate with a prefix that is specific to that
> > module, and different modules have different prefixes. In this way,
> > if you ask a negated query against any predicate in a given module,
> > then NAF and SNAF give the same result because nothing outside of
> > the module matters due to the uniqueness of the predicate names that
> > are local to that module.
> 
> Yes, I had trouble following some of that discussion [1] yesterday,
> but with this little explanation, it all becomes much more clear.
> Flora-2's module mechanism lets you separate parts of the
> rulebase into different areas, where they don't accidentally step on
> each other, but the formulas in those areas still participate in the
> logic.  
> 
> In contrast, N3's log:notIncludes mechanism keeps formulas in a much
> more remote area -- in the Prolog sense, they're just terms.
> log:notIncludes is not a metalogic (level-crossing) predicate; in a
> reasonable language like Prolog which had terms it would not extend
> the power of the language at all -- it would be quite easy to write.
> In fact, here it is, using ordsets [2]:
> 
>   %% notIncludes(+Big, +Small)
>   %%
>   %%    Big and Small are terms which represent N3 formulas, like:
>   %%
>   %%    [rdf(s,p,o), rdf(s,p,o), ...]
>   %%
>   %%
> 
>   notIncludes(Big, Small) :-
>   	list_to_ord_set(Big, BigSet),
> 	list_to_ord_set(Small, SmallSet),
> 	\+ ord_subset(BigSet, SmallSet).
> 
> I'd guess that does the right thing as far as unification when the
> formulas include variables, but I'm not sure.   (I'm not sure about
> either what ordsets does or what notIncludes does.)
> 
> Nearby log:notIncludes, we have log:semantics which in prolog looks
> something like:
> 
>   %% semantics(+URL, -Formula)
>   %%
>   %%    Fetch the data from the URL and parse it to a formula term
>   %%    based on its Content/Type.  Only N3 and RDF/XML are supported.
> 
>   ... okay, I won't really provide an implementation; it's pretty much
>   just like SWI's load_rdf/2 [3].  (I'm not sure what RDF support XSB has
>   these days.)
> 
> and also log:conclusion:
> 
>   %% conclusion(+Premise, -Conclusion)
>   %%
>   %%    Compute the deductive closure of the Premise (an N3 formula
>   %%    term) and unify it with the Conclusion.
>   %%
>   %%    Formulas look like  [ rdf(s,p,o), ..., <rule>, ... ]
>   %%
>   %%    where rule is:   rule(Antecedent, Consequent)
>   %%
>   %%    and Antecedent & Consequent are each formulas.
>   %%
> 
>   ... and maybe I should provide an implementation of this, but
>   I think I've made the point about how the arguments to these
>   interesting N3 predicates are essentially just terms.
> 
>  (aside:
> 
>   Actually, I think N3 formulas are somewhat more complex terms,
>   because they can have existentially and universally quantified
>   variables.  Some of that seems pretty messy to me.   I'd probably go
>   with:
> 
>           n3_formula([exivar1, exivar2, ...],
>                      [element1, element2, ...])
>       where exivars were constants (NOT prolog variables),
>       where elements could be either
>                   rdf/3 or rule/2 as above.
>       There's been talk of being able to label rules,
>       which would give us rule/3 instead.
>   )
> 
> Do you see now why/how N3 has a monotonic design, even if there are no
> formal semantics so no one can mathematically prove it?
> 
>     -- sandro
> 
> 
> [1] http://www.w3.org/mid/20050825220937.C46AACB5D3@kiferserv.kiferhome.com
> [2] http://cvs.sourceforge.net/viewcvs.py/xsb/XSB/lib/ordsets.P?rev=1.7&view=auto
> [3] http://www.swi-prolog.org/packages/rdf2pl.html#sec:3
> 


I think the key is that semantics(+URL,-Formula) predicate and the fact
that you are leaving out of the picture the actual formulas that are
sitting at URL. The formula that you are getting using semantics/2 is (as I
understand) a list of terms that reify logical statements.

So, you have

formulas sitting at URL  (*)
the built-in semantics(URL,Formula)
and then you have something like
    Formula notIncludes somelist

So, adding a new formula to the set (*) can change the list Formula
and invalidate a previously true statement of the form
Formula notIncludes somelist. This is nonmonotonic.


	--michael

Received on Saturday, 27 August 2005 18:07:16 UTC