From: Dan Connolly (connolly@w3.org)
Date: 11/30/01
"Peter F. Patel-Schneider" wrote:
>
> From: Dan Connolly <connolly@w3.org>
> Subject: Re: querying DAML+OIL syntax
> Date: Fri, 30 Nov 2001 11:46:24 -0600
>
> [...]
>
> > I expect the "obvious extra semantic condintions" includes
> > an axiom of pairs, ala
> >
> > (forall (?f ?r)
> > (=> (list ?r) ((exist (?l) (and (first ?l ?f) (rest ?l ?r)))))
>
> [...]
>
> > > Solution:
> > >
> > > It does not entail.
> > >
> > > There are interpretations that satisfy the first knowledge base where the
> > > denotation of a is not in any list,
> >
> > not if we include an axiom of pairs ala the above.
>
> You would need to include all DAML+OIL syntax in every interpretation,
> i.e., unionOf for every list of classes, ..... I'm uncertain if this
> approach would work.
Hmm... I assumed it was already working. I suppose
I was reading more into the DAML+OIL model theory than was there.
> However, even if it would, I have severe reservations. I liken it to a
> mechanism for including disjunction in RDF that would work something like.
>
> 1/ interpretations include all possible lists
> 3/ for every list that looks a formula, l,
> < l , IS(rdfb:true) > in IEXT(IS(rdf:type))
> iff the formula is satisfied in the interpretation
> 3/ list syntax denotes the appropriate list
>
> That is
>
> the interpretation of
> [OR [p1 s1 o1] [p2 s2 p2] [p3 s3 o3]]
> is in the class extension of rdfb:true if and only if
> either <IS(s1),IS(o1)> in IEXT(IS(p1), or
> <IS(s2),IS(o2)> in IEXT(IS(p2), or
> <IS(s3),IS(o2)> in IEXT(IS(p3)
Er... ok, I'll bite... why does this sort of thing bother you?
I ask mostly because our implementation of logic on top
of RDF works pretty much exactly this way. At least: I think
it does, after interviewing TimBL about it... I'm never
quite sure what theory best explains what the code does,
but I've been reasonably confident that this theory
matches Tim's code and writings and such
since I discovered it in September:
a formal design for RDF/N3 context/scopes
Dan Connolly (Thu, Sep 06 2001)
http://lists.w3.org/Archives/Public/www-rdf-logic/2001Sep/0004.html
In N3, log:implies isn't really a logical connective;
it's a relation constant, ala
(defrelation log:implies (?P ?Q) :=
(wtr ^(=> ,?P ,?Q))
so that
{ :x :y :z. } log:implies { :p :d :q }.
pretty much means
(wtr ^(=> (y x z) (p d q)))
It's really pretty strange... it means that the universal
quantification in most N3 rules is over *terms*, not
over objects. I thought this was totally wierd,
but I've run into folks that don't think so; they
call it "schematic quantification" or something like that.
Anyway... logical disjunction is introduced similarly...
there are classes log:Truth and log:Falsehood,
and rules
this log:forAll :P, :Q, :R.
{ :P log:or :Q.
:P a log:Falsehood } log:implies
{ :Q a log:Truth }.
{ :P log:or :Q.
:Q a log:Falsehood } log:implies
{ :P a log:Truth }.
{ :P log:or :Q.
:P log:implies :R.
:Q log:implies :R. }
log:implies { :R a log:Truth }.
Our rules engine doesn't use any tactics that really
exploit the last rule -- it only does forward chaining --
but it seems to do sensible
things with the first two. Oh... actually, I think
the rules engine pays special attention to
:X a log:Truth
but I haven't really tested it.
--
Dan Connolly, W3C http://www.w3.org/People/Connolly/
This archive was generated by hypermail 2.1.4 : 04/02/02 EST