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? 
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). 

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 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?)

> 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 15:36:42 UTC