kb Scoped Negation As Failure

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
5 messages Options
Reply | Threaded
Open this post in threaded view
|

kb Scoped Negation As Failure

jos.deroo

Today I was experimenting with kb Scoped Negation As Failure
via http://eulersharp.sourceforge.net/2003/03swap/log-rules#no

[[
e:no
  rdfs:comment """kb Scoped Negation As Failure""";
  a rdf:Property;
  rdfs:domain rdf:List;
  rdfs:range log:Formula.
]]

The e:no object is a single triple that is not in the deductive
closure of the e:no subject feedlist of n3 sources.

A test case is:

given:
  http://www.agfa.com/w3c/euler/medmio.n3

query:
  http://www.agfa.com/w3c/euler/medmioF.n3

proof:
  using euler5 running on top of yap
 
http://eulersharp.cvs.sourceforge.net/eulersharp/2006/02swap/euler.yap?revision=1.37
  i.e.
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
#Processed by Id: euler.yap,v 1.37 2006/05/28 00:24:10 josd Exp

@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix owl: <http://www.w3.org/2002/07/owl#>.
@prefix str: <http://www.w3.org/2000/10/swap/string#>.
@prefix xsd: <http://www.w3.org/2001/XMLSchema#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>.
@prefix rpo: <http://eulersharp.sourceforge.net/2003/03swap/rpo-rules#>.
@prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>.
@prefix q: <http://www.w3.org/2004/ql#>.
@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <http://eulersharp.sourceforge.net/2006/02swap/med#>.
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.

(<http://www.agfa.com/w3c/euler/medic.n3>
<http://www.agfa.com/w3c/euler/medicF.n3>) e:rpn3 (
[ e:enter {:aspirinLowDose :prescribedFor :AcuteMyocardialInfarction}]
[ e:enter {(:Joe :AcuteMyocardialInfarction) rpo:mu 0.9}]
[ e:enter {0.9 math:greaterThan 0.7}]
[ e:imply {{:aspirinLowDose :prescribedFor :AcuteMyocardialInfarction.
(:Joe :AcuteMyocardialInfarction) rpo:mu 0.9. 0.9 math:greaterThan 0.7} =>
{:Joe :candidateFor :aspirinLowDose}}]
[ e:enter {(<http://www.agfa.com/w3c/euler/medic.n3>
<http://www.agfa.com/w3c/euler/medicF.n3>) e:no {:Joe :notPrescribed
:aspirinLowDose}}]
[ e:imply {{:Joe :candidateFor :aspirinLowDose.
(<http://www.agfa.com/w3c/euler/medic.n3>
<http://www.agfa.com/w3c/euler/medicF.n3>) e:no {:Joe :notPrescribed
:aspirinLowDose}} => {:Joe :isPrescribed :aspirinLowDose}}]
[ e:prove {{:Joe :isPrescribed :aspirinLowDose} => {:Joe :isPrescribed
:aspirinLowDose}}]).
:Joe :isPrescribed :aspirinLowDose.

(<http://www.agfa.com/w3c/euler/medic.n3>
<http://www.agfa.com/w3c/euler/medicF.n3>) e:rpn3 (
[ e:enter {:betaBlocker :prescribedFor :AcuteMyocardialInfarction}]
[ e:enter {(:Joe :AcuteMyocardialInfarction) rpo:mu 0.9}]
[ e:enter {0.9 math:greaterThan 0.7}]
[ e:imply {{:betaBlocker :prescribedFor :AcuteMyocardialInfarction. (:Joe
:AcuteMyocardialInfarction) rpo:mu 0.9. 0.9 math:greaterThan 0.7} => {:Joe
:candidateFor :betaBlocker}}]
[ e:enter {(<http://www.agfa.com/w3c/euler/medic.n3>
<http://www.agfa.com/w3c/euler/medicF.n3>) e:no {:Joe :notPrescribed
:betaBlocker}}]
[ e:imply {{:Joe :candidateFor :betaBlocker.
(<http://www.agfa.com/w3c/euler/medic.n3>
<http://www.agfa.com/w3c/euler/medicF.n3>) e:no {:Joe :notPrescribed
:betaBlocker}} => {:Joe :isPrescribed :betaBlocker}}]
[ e:prove {{:Joe :isPrescribed :betaBlocker} => {:Joe :isPrescribed
:betaBlocker}}]).
:Joe :isPrescribed :betaBlocker.

#ENDS 0 msec.
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Another example is Shubert's steamroller and the proof result is in
http://eulersharp.sourceforge.net/2006/02swap/etc5.ref


--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Reply | Threaded
Open this post in threaded view
|

Re: kb Scoped Negation As Failure

jos.deroo

Oops.. looking at the proof, the test case was
given:
  http://www.agfa.com/w3c/euler/medic.n3

query:
  http://www.agfa.com/w3c/euler/medicF.n3

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/




Jos De Roo/AMDUS/AGFA@AGFA
Sent by: [hidden email]
28/05/2006 17:05
 
        To:     [hidden email]
        cc:     (bcc: Jos De Roo/AMDUS/AGFA)
        Subject:        kb Scoped Negation As Failure



Today I was experimenting with kb Scoped Negation As Failure
via http://eulersharp.sourceforge.net/2003/03swap/log-rules#no

[[
e:no
  rdfs:comment """kb Scoped Negation As Failure""";
  a rdf:Property;
  rdfs:domain rdf:List;
  rdfs:range log:Formula.
]]

The e:no object is a single triple that is not in the deductive
closure of the e:no subject feedlist of n3 sources.

A test case is:

given:
  http://www.agfa.com/w3c/euler/medmio.n3

query:
  http://www.agfa.com/w3c/euler/medmioF.n3

proof:
  using euler5 running on top of yap
 
http://eulersharp.cvs.sourceforge.net/eulersharp/2006/02swap/euler.yap?revision=1.37

  i.e.
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
#Processed by Id: euler.yap,v 1.37 2006/05/28 00:24:10 josd Exp

@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix owl: <http://www.w3.org/2002/07/owl#>.
@prefix str: <http://www.w3.org/2000/10/swap/string#>.
@prefix xsd: <http://www.w3.org/2001/XMLSchema#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.
@prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>.
@prefix rpo: <http://eulersharp.sourceforge.net/2003/03swap/rpo-rules#>.
@prefix e: <http://eulersharp.sourceforge.net/2003/03swap/log-rules#>.
@prefix q: <http://www.w3.org/2004/ql#>.
@prefix math: <http://www.w3.org/2000/10/swap/math#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <http://eulersharp.sourceforge.net/2006/02swap/med#>.
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.

(<http://www.agfa.com/w3c/euler/medic.n3>
<http://www.agfa.com/w3c/euler/medicF.n3>) e:rpn3 (
[ e:enter {:aspirinLowDose :prescribedFor :AcuteMyocardialInfarction}]
[ e:enter {(:Joe :AcuteMyocardialInfarction) rpo:mu 0.9}]
[ e:enter {0.9 math:greaterThan 0.7}]
[ e:imply {{:aspirinLowDose :prescribedFor :AcuteMyocardialInfarction.
(:Joe :AcuteMyocardialInfarction) rpo:mu 0.9. 0.9 math:greaterThan 0.7} =>

{:Joe :candidateFor :aspirinLowDose}}]
[ e:enter {(<http://www.agfa.com/w3c/euler/medic.n3>
<http://www.agfa.com/w3c/euler/medicF.n3>) e:no {:Joe :notPrescribed
:aspirinLowDose}}]
[ e:imply {{:Joe :candidateFor :aspirinLowDose.
(<http://www.agfa.com/w3c/euler/medic.n3>
<http://www.agfa.com/w3c/euler/medicF.n3>) e:no {:Joe :notPrescribed
:aspirinLowDose}} => {:Joe :isPrescribed :aspirinLowDose}}]
[ e:prove {{:Joe :isPrescribed :aspirinLowDose} => {:Joe :isPrescribed
:aspirinLowDose}}]).
:Joe :isPrescribed :aspirinLowDose.

(<http://www.agfa.com/w3c/euler/medic.n3>
<http://www.agfa.com/w3c/euler/medicF.n3>) e:rpn3 (
[ e:enter {:betaBlocker :prescribedFor :AcuteMyocardialInfarction}]
[ e:enter {(:Joe :AcuteMyocardialInfarction) rpo:mu 0.9}]
[ e:enter {0.9 math:greaterThan 0.7}]
[ e:imply {{:betaBlocker :prescribedFor :AcuteMyocardialInfarction. (:Joe
:AcuteMyocardialInfarction) rpo:mu 0.9. 0.9 math:greaterThan 0.7} => {:Joe

:candidateFor :betaBlocker}}]
[ e:enter {(<http://www.agfa.com/w3c/euler/medic.n3>
<http://www.agfa.com/w3c/euler/medicF.n3>) e:no {:Joe :notPrescribed
:betaBlocker}}]
[ e:imply {{:Joe :candidateFor :betaBlocker.
(<http://www.agfa.com/w3c/euler/medic.n3>
<http://www.agfa.com/w3c/euler/medicF.n3>) e:no {:Joe :notPrescribed
:betaBlocker}} => {:Joe :isPrescribed :betaBlocker}}]
[ e:prove {{:Joe :isPrescribed :betaBlocker} => {:Joe :isPrescribed
:betaBlocker}}]).
:Joe :isPrescribed :betaBlocker.

#ENDS 0 msec.
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -

Another example is Shubert's steamroller and the proof result is in
http://eulersharp.sourceforge.net/2006/02swap/etc5.ref


--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/




Reply | Threaded
Open this post in threaded view
|

Re: kb Scoped Negation As Failure

Dan Connolly
In reply to this post by jos.deroo


On May 28, 2006, at 10:05 AM, [hidden email] wrote:

>
> Today I was experimenting with kb Scoped Negation As Failure
> via http://eulersharp.sourceforge.net/2003/03swap/log-rules#no

Interesting... if I understand correctly, we have...

  { ?FORMULAS e:no ?CONCLUSION }
   <=> { ?FORMULAS.log:conclusion log:notSupports ?CONCLUSION }.

where log:notSupports is the oppositve of log:supports; it's not
something
we've implemented so far, I think.

It makes sense except for this part of the proof:

> [ e:imply {{:Joe :candidateFor :betaBlocker.
> (<http://www.agfa.com/w3c/euler/medic.n3>
> <http://www.agfa.com/w3c/euler/medicF.n3>) e:no {:Joe :notPrescribed
> :betaBlocker}} => {:Joe :isPrescribed :betaBlocker}}]

I see the corresponding rule in http://www.agfa.com/w3c/euler/medic.n3 
...

{?W :candidateFor ?M. ?M :excludedFor ?D. ?U e:no {(?W ?D) rpo:mu ?V}}
=> {?W :notPrescribed ?M}.

but I don't see how ?U gets bound to
(<http://www.agfa.com/w3c/euler/medic.n3>
<http://www.agfa.com/w3c/euler/medicF.n3>). Does the e:no built-in have
access to the command-line args?
>


--
Dan Connolly, W3C http://www.w3.org/People/Connolly/


Reply | Threaded
Open this post in threaded view
|

Re: kb Scoped Negation As Failure

jos.deroo

Dan Connolly wrote:

> On May 28, 2006, at 10:05 AM, [hidden email] wrote:
>
>>
>> Today I was experimenting with kb Scoped Negation As Failure
>> via http://eulersharp.sourceforge.net/2003/03swap/log-rules#no
>
> Interesting... if I understand correctly, we have...
>
>   { ?FORMULAS e:no ?CONCLUSION }
>    <=> { ?FORMULAS.log:conclusion log:notSupports ?CONCLUSION }.
>
> where log:notSupports is the oppositve of log:supports; it's not
> something
> we've implemented so far, I think.

I was not aware of log:notSupports but now see tests
in http://www.w3.org/2000/10/swap/test/supports/
and I will try it that way :-)

The e:no implementation we have is a single prolog line
'e:no'(U,lf(Y)):- (X==>Y), X, !, fail; \+Y, feed(U).
and see below for that feed predicate...

> It makes sense except for this part of the proof:
>
>> [ e:imply {{:Joe :candidateFor :betaBlocker.
>> (<http://www.agfa.com/w3c/euler/medic.n3>
>> <http://www.agfa.com/w3c/euler/medicF.n3>) e:no {:Joe :notPrescribed
>> :betaBlocker}} => {:Joe :isPrescribed :betaBlocker}}]
>
> I see the corresponding rule in http://www.agfa.com/w3c/euler/medic.n3 
> ...
>
> {?W :candidateFor ?M. ?M :excludedFor ?D. ?U e:no {(?W ?D) rpo:mu ?V}}
> => {?W :notPrescribed ?M}.
>
> but I don't see how ?U gets bound to
> (<http://www.agfa.com/w3c/euler/medic.n3>
> <http://www.agfa.com/w3c/euler/medicF.n3>). Does the e:no built-in have
> access to the command-line args?
>>

It looks for feed(U) and will find one in the engine kb
as during aggregation of n3 sources (done via euler1)
we assert a fact such as
feed(['<http://www.agfa.com/w3c/euler/medic.n3>','<http://www.agfa.com/w3c/euler/medicF.n3>']).

Thanks for your prompt reply, esp. while it is Sunday :-)

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Reply | Threaded
Open this post in threaded view
|

Re: kb Scoped Negation As Failure

jos.deroo
In reply to this post by Dan Connolly

[some more after test last night..]
Dan Connolly wrote:

>On May 28, 2006, at 10:05 AM, [hidden email] wrote:
>
>>
>> Today I was experimenting with kb Scoped Negation As Failure
>> via http://eulersharp.sourceforge.net/2003/03swap/log-rules#no
>
> Interesting... if I understand correctly, we have...
>
>  { ?FORMULAS e:no ?CONCLUSION }
>   <=> { ?FORMULAS.log:conclusion log:notSupports ?CONCLUSION }.
>
> where log:notSupports is the oppositve of log:supports; it's not
> something
> we've implemented so far, I think.

medic test case [1] is now running [2] with

{?W :candidateFor ?M. ?U!e:scope log:notIncludes {?W :notPrescribed ?M}}
    => {?W :isPrescribed ?M}.

where [3]

e:scope
  rdfs:comment """relationship between the asserted n3 formulae and their
log:conclusion""";
  rdfs:subPropertyOf log:conclusion;
  rdfs:domain log:Formula;
  rdfs:range log:Formula.


--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

[1] http://www.agfa.com/w3c/euler/medic.n3
[2] http://eulersharp.sourceforge.net/2006/02swap/etc5.ref
[3] http://eulersharp.sourceforge.net/2003/03swap/log-rules