Re: Explanations and Proof-Language Meeting, Follow-Up

Hi Deb,

I looked into http://www.ksl.stanford.edu/software/IW/tmp/
and thought how we (using n3 and euler) would express
that right now and I was also thinking about Tim's remark
about quoting the variables to express their binding
(and started to (mis?)use your iw:Variable).

So we would start from a couple of premises:
your facts in http://www.agfa.com/w3c/euler/deb.n3
[[
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix : <deb#>.

:Tony a :CRAB.
:CRAB rdfs:subClassOf :SEAFOOD.
]]

and something at http://www.agfa.com/w3c/euler/rdfs-rules.n3

Then we wonder wether we can prove
http://www.agfa.com/w3c/euler/debC.n3
[[
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix : <deb#>.

:Tony a :SEAFOOD.
]]

We get a single document proof argument
http://www.agfa.com/w3c/euler/debE.n3
[[
# Generated with http://www.agfa.com/w3c/euler/#R3431 on 1 May 2003
15:30:00 GMT
{
 (

<http://www.agfa.com/w3c/euler/rdfs-rules.n3>.<http://www.w3.org/2000/10/swap/log#semantics>

<http://www.agfa.com/w3c/euler/deb.n3>.<http://www.w3.org/2000/10/swap/log#semantics>
 ).<http://www.w3.org/2000/10/swap/log#conjunction> =>

<http://www.agfa.com/w3c/euler/debC.n3>.<http://www.w3.org/2000/10/swap/log#semantics>
}
<http://www.w3.org/2000/10/swap/reason#because>
{
@prefix str: <http://www.w3.org/2000/10/swap/string#>.
@prefix ns: <http://www.agfa.com/w3c/euler/rdfs-rules#>.
@prefix xsd: <http://www.w3.org/2001/XMLSchema#>.
@prefix : <http://www.agfa.com/w3c/euler/deb#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#>.
@prefix owl: <http://www.w3.org/2002/07/owl#>.
@prefix iw: <http://www.ksl.stanford.edu/software/IW/spec/iw#>.
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#>.

 {
  <http://www.agfa.com/w3c/euler/rdfs-rules#rdfs9>.
  {[ iw:Variable "?A"] = :CRAB. [ iw:Variable "?B"] = :SEAFOOD. [
iw:Variable "?A"] rdfs:subClassOf [ iw:Variable "?B"]} => {:CRAB
rdfs:subClassOf :SEAFOOD}.
  {[ iw:Variable "?S"] = :Tony. [ iw:Variable "?A"] = :CRAB. [ iw:Variable
"?S"] a [ iw:Variable "?A"]} => {:Tony a :CRAB}}  =>
{:Tony a :SEAFOOD}.

# Proof found for http://www.agfa.com/w3c/euler/debC.n3 in 45 steps
(4500000 steps/sec) using 1 engine
}.
]]


which is n3 where
{} is grouping a set of statements (triples)
= is owl:sameAs
=> is log:implies
iw: is a namespace prefix owned by www.ksl.stanford.edu
etc...
This is one document and I wonder if that is good...
it's even 1 triple
a-formula-got-from-web reason:because a-nested-proof-argument.
Yes, the proof argument is a nested {} set of statements...


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


                                                                                                                   
                    "Deborah L.                                                                                    
                    McGuinness"          To:     Sandro Hawke <sandro@w3.org>                                      
                    <dlm@ksl.Stanf       cc:     Jos De_Roo/AMDUS/MOR/Agfa-NV/BE/BAYER@AGFA, Dejing Dou            
                    ord.EDU>              <dejing.dou@yale.edu>, Deborah McGuinness <dlm@belo.Stanford.EDU>, Drew  
                                          McDermott <drew.mcdermott@yale.edu>, Jerome Euzenat                      
                    2003-04-30            <Jerome.Euzenat@inrialpes.fr>, Paulo Pinheiro da Silva                   
                    07:31 AM              <pp@ksl.Stanford.EDU>, sw-team@w3.org, www-archive@w3.org                
                                         Subject:     Re: Explanations and Proof-Language Meeting, Follow-Up       
                                                                                                                   




thanks also for your participation.
In addition to the list below, i think there is one thing we would like to
do to facilitate your usage:
(I number it 6 as an extension to sandro's list below).
6. extend the portable proof specification so that there is a uri for
premises.  (we can run a proposal by whomever is appropriate - from the
phone conversation that sound like it may be tim, sandro, and jos)

Also, as asides as a result of comments today we will add:
 - a summary listing of sources used in a proof (in addition to the summary
listing of the ground axioms used)

a few comments below:

Sandro Hawke wrote:
          Many thanks for the meeting
          http://www.w3.org/2003/04/29/swad/

          and the irc log
          http://www.w3.org/2003/04/29-sw-team-irc


     Thanks for posting those.  Thanks again to everyone who participated;
     even though we didn't cover the whole agenda, I think we got a long
     way given the subject matter and limitations of the medium.

     Moving forward, it seems like there are several mostly-separable areas
     of work:

       1.  modifications to cwm to output the language/files
       2.  write & publish the step & engine descriptions
           (perhaps via the ksl registrar, perhaps not...?)
we would like to facilitate publishing through inference web.  if there is
some resistance to this, we would like to understand so that we can update
iw to meet your needs.

       3.  dialog about modifications to the language, in general; mostly
           RDF-style issues, like adding URIs to nodes
       4.  figure out the content-language issue (KIF, RDF/XML reification,
     ...)
we have users who need the expressive power of kif.  if you can live with
less power (and we understand your language) , we can take registrations in
a less expressive language (and internally translate to kif).

       5.  (somewhat trivial) some web usability mods to IW Browser
     (cookies!)

this may need a dialog as well.  we are happy to discuss and adapt if
useful.

     It's not clear to me right now what resources are available at the
     W3C/MIT end, but hopefully we'll figure that out soon.

we are eager to collaborate so we would like to help.  we will need a
partner from your side of course so whenever you understand your resource
situation, please contact us.

thx for the great conversation.  we look forward to more.

deborah

        -- sandro

Received on Thursday, 1 May 2003 12:11:59 UTC