Re: Open Worlds, Distribution, Delegation, Federation, Logic

> > I'm really with you on those topics, although I haven't
> > had enough chance to talk with you about those topics on the
> > technical pleanary meeting (but I have still your face
> > in front of my mind ...).

> Ah!  I never made the name/face connection for you until just now,
> looking at your web page.   I thought some more about what you asked
> after my little talk, but now I can't quite remember it.  (I've
> learned a lot more about logic this week; some of it's pretty
> tangled.)

You are right, there's a lot to be done ...
Don't worry about that question, which I think was about circular
definitions. We will certainly come back on that later.

> > With respect to negation, I don't know if we are avoiding naf
> > (negation as failure) when we are using
> >   {:subject :verb :object} log:implies <data:,>
> > which is a specific form of a nested implication (if I'm correct)
> > The <data:,> (or the "" if you want) is not the same as
> > log:Falsehood but just stands for a no-proof-found instance
> > which could be the result of any (delegated) attempt to find
> > any evidence (when using a universally quantified verb for the
> > conclusion). So I'm not sure wether that's naf or not, but it
> > certainly _opens_ the way engines can interact ...

> This is the first I've heard of this convention.  Did you come up with
> it for Euler?

Yes and let me try to explain the context ...
If we assume material implication then we can write P -> C instead
of ~P v C. Next we assume an interpretaion in which P and C are
proof-values (more or less n3 expressions with recursive log:implies).
The point now is that one can not deduce an empty proof value from
a valid proof value (in the same sense that we can not deduce
log:Falsehood from log:Truth). If we find such a deduction then P
is simply non-sense.

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

I very much like the idea of being more explicit and what you
propose here sounds very good! It's good to think about that
further and to come up with a least power proof language ...

> I think that this is all fine (and necessary), as long as we're
> careful not to conclude Falsehood when it is not warranted.  In
> particular, it may often be appropriate to infer something being false
> if a particular engine, operating on a particular data set, was not
> able to find a proof.

Exactly.

> But I think the NAF concept used more freely will lead people to
> seriously overconstrain their system, stopping it from evolving.

I fully agree with that.

> While I'm following up my earlier message, I want to mention that
> Harold Boley said my proposed system for communication with
> meta-queries sounded like a "blackboard architecture" which indeed it
> does.

I think Harold is right, but I hope that will not stop you ...

--
Jos

Received on Saturday, 3 March 2001 15:53:24 UTC