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/

Received on Sunday, 28 May 2006 15:05:45 UTC