Re: A Single Foundational Logic for the Semantic Web

> >At best, certain communities can agree on some logic
> >(eg DAML+OIL) and their software can interoperate.  In some cases,
> >mappings can be made between logics, but it's probably wishful
> >thinking to expect much from that.)
> 
> No, I think that is an exact mirror of the human condition, and 
> inevitable in global forum. People talk different languages, but 
> manage to get by using patchy translations.

Well, no.  Actually, pretty much everybody on the web speaks the same
IP, TCP, HTTP, and HTML.  It's amazing.

If you want global coherence on the human experience, yes, of course
you're right.  Some of us only want global coherence among our
computerized information systems, which is perhaps a more modest goal.


> None of this [stuff about programming] has anything to do with what
> the RDF/DAML/OWL development effort is about, seems to me.

That statement is both outrageous and totally understandable.  We're
arguing with some pretty ambiguous terms here.   I'll try to be more
precise; stop me when go wrong.  (like I have to say that....)

RDF specifies an abstract, decentralized way that people can transmit
parts of databases.  It beats SQL "insert" statements and
comma-separated-values files in using a global namespace for columns
and datatypes, and in never freezing the schema.

DAML specifies ways one can encode in an RDF database that certain
transformations (commonly known as description logic inferences) can
be done on each database fragment or collection of database fragments
to generate more information which is as correct as the original
information.

Swap/log (which cwm implements) does the same thing as DAML, except it
allows a different set of transformations.  The set it allows happens
to be the same as the set of transformations that computers are in
(Church-Turing) theory capable of.

Any more expressive logic is lost on a computer.  It's useless.  Go
back to Swap/log.   What else were you trying to tell the computer?
What did you expect it to do?   Now tell it to do that in a
programming language, like Swap/log.   (Or, if it's something really
simple, you can use a not-Turing-complete language like RDFS.)

> The issue is not getting a machine to do something.

Oh!   I thought it was.  I thought the purpose of logic was to be able
to make valid inferences, and the purpose of teaching computers about
logic was to get them to help us make (only) valid inferences.

> It is finding a 
> way for websites to COMMUNICATE content to one another in a way they 
> all in some sense mutually understand. What they DO with that content 
> is their business; but in any case, the logics aren't being used to 
> communicate methods of doing things (use Java for that), but 
> propositions - facts -  about some external world.

Why?   What kind of fact would you ever want to communicate that can't
be expressed in RDF or in terms of a computer doing something?     

Here's one of my examples: an RDF vocabulary of people being in
cities.  [Cities are (amazingly!) disjoint, and a person's current
city is a unique property.  For simplicity in this example, let's also
assume an RDF vocabulary for disjunction.]  We can easily say George is
in San Francisco.  But RDF cannot say (in this vocabulary) that George
is not in San Francisco.  (It could say George is in Boston, and you
could infer the above negation, but it can't directly say the
negation.)

And you WANT to say George is not in San Francisco.  You really do!
Why?  Well, maybe someone else said that George was "either in San
Francisco or San Jose", so if you can make your negative claim, others
can infer he is in San Jose.  (You don't want to simply say he's in
San Jose, because you don't happen to trust the guy who stated the
disjunction, but you want others who trust both him and you to be able
to make the inference.)

But the W3C never recommended any vocabulary for negation, damn their
black corporate hearts, so you'll have to take your chances that maybe
someone out there read Drew's paper on logic layering and is using his
vocabulary.  That might work.  Maybe someone implemented it.  But it
did have that GPL clause, so no one using a Microsoft browser will see
it.  Darn.  What about...

You could use that silly Horn logic which everyone uses for doing
gif animation and calculating their taxes....  You think of a Horn
rule like "If George is known to be 'either in San Francisco or in San
Jose', then he's in San Jose".   You realize it will have exactly the
same effect as your negation, in this specific instance.   Well, good
enough.

Okay, not good enough.  What if someone says some other disjunction
about him?  Hrm.  Check google.  Ahhh!  Bijan ported a resolution
theorem prover, which uses Drew's vocabulary, to that silly Horn
logic.  There's the URI.  "Include" it in your posting which used
Drew's negation vocabulary, and all the silly people with a Horn
implementation will be told where George is, if they have the
information to allow a proof of the answer to be constructed.

Sorry if that's boring detail, but it seemed worth it for the
increased clarity.

> So the entire idea 
> of Turing-Equivalent logic is beside the point. (You don't need N3 to 
> do that, by the way. I think Sheffer-stroke propositional logic is 
> Turing-complete, given about eight proposition letters.)

N3 is a convenience syntax for RDF; Swap/log is my name for TimBL's a
Horn-style logic with a bunch of stuff we dont need like, um, a truth
predicate.  :-) I don't have a horn-logic in RDF vocabulary I'd
recommend right now, because I haven't figured out where to make some
engineering tradeoffs.

Okay.  End of part 1.  On to paradoxes....

> >So the layering looks like this:
> >
> >    Layer 3: Any logic for which an effective inference procedure is known
> >    Layer 2: A Turing-Equivalent Logic (such as TimBL's swap/log [1])
> >    Layer 1: RDF (Pat's MT, more or less)
> >
> >So: we can and should pick a Turing-Equivalent logic (with an RDF
> >syntax) and recommend it as a foundational part of the Semantic Web.
> >If we do this, new logics can be defined and used interoperabily at
> >will.  Some logics (eg DL, arithmetic) can be recognized by some
> >reasoners and handled with better performance.
> >
> >I think this view helps explain why some of us keep being unconcerned
> >by PFPS's red flags about paradoxes.  The paradoxes do not seem to
> >appear at the Turing-Equivalent level (which has no real negation or
> >notion of falsehood), and we view paradoxes in Layer 3 as just another
> >programming problem.  From a Layer 2 perspective, the worst these
> >paradoxes produce is an all-too-familiar non-terminating process.
> >(This does not mean the paradoxes are not a big problem, just that
> >they're a problem in Layer-3 logics, and some of us are still busy on
> >layers 1 and 2.  And....  I'm not convinced Layer 3 will be very
> >important.)
> 
> Sandro, I just don't know how to tell you this politely, sorry. You 
> are confused.

I'll grant that I am confused from time to time, and quite possibly
even mistaken, but I don't see how that's true here.   It looks to me
like you misunderstood me.

> Look, the paradoxes are not a programming problem, and they don't 
> have anything to do with non-termination. (A non-terminating process 
> corresponds to something that is undecideable, roughly, not to a 
> paradox.) If the SW tried to do reasoning in the presence of 
> paradoxes, the problem would not be that code fails to terminate. All 
> the reasoning engines would work fine, and if they were using 
> DL-style logic then they would probably work quite efficiently and 
> rapidly, producing correct, checkable proofs using semantically 
> correct inference rules. However, the conclusions would all be 
> worthless, because that perfectly valid logic would be able to prove 
> that 2+2=5 and the Pope was both a Roman Catholic and also not a 
> Roman Catholic, and so on. The problem would not be in the code, but 
> in the content of the expressions manipulated by the code. The 
> correctness of the code would not guarantee that the conclusions made 
> any sense (in fact, it would guarantee that they *didnt* make sense.) 
> The conclusions produced by any reasoner are only as good as the 
> information it is given. In the presence of paradoxes it can produce 
> nonsense all by itself, so any information it handles is potentially 
> corrupted.

I do understand all that.  Please re-read my last quoted paragraph
above.  I'm addressing why some of us aren't so worried about
paradoxes, not saying that paradoxes are not a big problem.  ("This
does not mean the paradoxes are not a big problem.")  I read PFPS's
writing about when paradoxes occur to suggest that a Horn logic can
skirt the issue.  Perhaps I'm misreading it; if someone can present a
paradox using only log:forSome, log:forAll, and log:implies, then I
think I (and I'll venture TimBL and others) will be very interested.
[Hrm, I guess you'll have trouble until an n3->n-triples conversion is
written down.  It's in public e-mail between me and Tim; I'll dig it
up if anyone seriously wants to try.  The idea is to use
log:Conjunction and daml:List to assemble an n3 Formula.]

I would also argue with your phrasing, "All the reasoning engines
would work fine."  Yes, all the reasoning engines would conform to
their formal specifications, but they would of course not work "fine"
in the sense any decent programmer or paying customer would use the
word.  Rather they would conform to a lousy incompletely-thought-out
specification.  Lousy specifications are not new, and thinking things
out completely is often impossible [halting problem!].  Much of the
software development process is about debugging the specification
itself (if you even have one) and turning it into something which can
be implemented as a useful system.  The paradox red flags are people
saying "you'll never be able to implement this (as a useful system)"
which is wonderfully helpful at this early stage, if they're right.

In my layering scheme, paradoxes in a layer 3 logic would lead one to
be unable to write a correct/useful layer 2 inference procedure.  I
imagine the actual failure modes might vary in frequency and severity,
like many other software bugs.  Certainly if you knew the logic had a
paradox, you'd want to steer your billions of dollars per second far
away from it, but you might still play chess against programs using it.

     -- sandro

Received on Monday, 29 April 2002 14:40:37 UTC