Re: expressing scope of negation of failure (wasRe: Open Worlds, Distribution, Delegation, Federation, Logic, NI )

----- Original Message -----
From: "Frank Manola" <fmanola@mitre.org>
To: "Tim Berners-Lee" <timbl@w3.org>
Cc: <jos.deroo.jd@belgium.agfa.com>; "Sandro Hawke" <sandro@w3.org>;
<www-rdf-logic@w3.org>; <www-rdf-interest@w3.org>
Sent: Wednesday, March 07, 2001 3:31 PM
Subject: Re: expressing scope of negation of failure (wasRe: Open Worlds,
Distribution, Delegation, Federation, Logic, NI )


> Tim Berners-Lee wrote:
> >
> > > My approach (not yet implemented) is much more explicit: conclude
> > > (instead of a literal) something like "this engine could not satisfy
> > > this proof", which I can't think of how to express in n3 right now.
> > > "This engine" is an identifier for the running process which tried to
> > > find the proof, and "this proof" is an identifier for the proof
> > > requested.  or something like that.
> >
> > This requires a model of the knowledge  in the engine at a given time.
> > I was thinking along the lines of
> >
> > followsFromUsingXXXReasoning(expression, document)
> >
> > where document is the source of information, and expression is the
> > thing proved.
>
> I'd like to understand the simplifications in Tim's (re)formulation.
> One simplification seems to be referencing a specific document rather
> than "a model of the knowledge in the engine at a given time", right?

Yes, you can always dump an engine to a document and reference that.
The document could be a virtual document which
carries the state of an engine, but you'd have to be able to refer to it
later.

> Presumably the document is identified by a URI, so this could be
> generalized by allowing the URI to reference more complex sources of
> information (e.g., collections of documents, which seems like a likely
> requirement, or even the "model of the knowledge in the engine at a
> given time", assuming there was a definition of how to assign a URI to
> it).

Yes, or it could indeed be an asbtract set of data such as
"that which you would get if you took all these documents and merged their
data
and removed all rdfs:description properties" or whatever.

But basically, I wanted the concept fo a set of information to be
wellddefined and
in most cases reproducable.  Otherwise it makeslittle sense to refer to it.
Unless you just trust a given process.

> The second simplification seems to be using
> "followsFromUsingXXXReasoning" (e.g., "impliesByFPC" in the following
> example), rather than identifying a specific engine (or process).  Is
> the idea that "impliesByFPC" would be defined such that a piece of
> software that is not necessarily a FPC theorem-prover can verify that
> the result was indeed "implied by FPC"?

I deliberately didn't use "impleidByFOPC" inmy example because of the
obvious limitations. Basically, that in general if someone asserts such a
thing
you have to be able to ask them for a proof if you can't find it yourself.

>  (I assume that if the predicate
> were only "wasDeducedByEngineFoo", you wouldn't necessarily know what
> specific type of reasoning was used to derive the result, although this
> could be supplied as additional assertions;  or in the worst case you
> might have to decide whether or not you trusted EngineFoo?)

Yes. One has all these choices of course. In fact is is rather eay to
document
that what program make the inference, and rather easy to check it if you had
the program.
So I wouldn'tr rule that out at all, for cases where the program is trusted
by two parties.  If the program in fact contains heuristics it may be
difficult to
elaborate this criterion in termd of common logical language fo course.

Tim

> > By contrast,
> >
> > <~/calendar.rdf>   log:impliesByFPC  { :i a cal:OverCommittedPerson } .
> >
> > means that there is a forst order proof of the conclusion from the
evidence
> > in the document.
> >
>
> --Frank
>
> --
> Frank Manola                   The MITRE Corporation
> 202 Burlington Road, MS A345   Bedford, MA 01730-1420
> mailto:fmanola@mitre.org       voice: 781-271-8147   FAX: 781-271-8752
>

Received on Wednesday, 7 March 2001 18:13:00 UTC