Re: Grist for layering discussion

On Fri, 2002-01-11 at 19:14, Peter F. Patel-Schneider wrote:
[...]
> > So you feel that allowing reification -- or, presumably, allowing
> > sets of statements as first class objects in the syntax -- makes the system
> > such that one can necessarily deduce a contradiction from nothing?
> > Then I need help understanding how.
> 
> Look at the spec for KIF at http://logic.stanford.edu/kif/dpans.html.  The
> section on Metaknowledge has a nice description of one such problem.

A solved problem, no?

I've looked at it... several times. It seems to be exactly
what we need. (Actually, the KIF v3 version is less constraining
and looks more useful).

But metaknowledge aside...

I'm still trying to figure out why the axiomatic semantics
for DAML+OIL isn't perfectly good basis for WebOnt. It
seems to play nicely with the RDF model theory, as far as
I can tell. That is: the RDF model theory gives
an n-triples document (and hence any RDF document)
a meaning that corresponds
directly to a KIF formula of the form

(exists (?x1 ?x2 ?x3)
  (and
    (p1 s1 o1)
    (p2 ?x1 o2)
    (?x3 s3 o3)
    ...
  )
)

I trust you'll grant me that (PropertyValue p s o) isn't
interestingly different from (p s o) with the menzel indirection trick,
no?

What's wrong with specifying ont:complementOf ala:

 (forall (?C1 ?C2)
  (iff (ont:complementOf ?C1 ?C2)
       (forall (?x)
         (iff (rdf:type ?x ?C1) (not (rdf:type ?x ?c2)))
       ) ) )

How does the model theory paradox you presented earlier show
up in an axiomatic specification like this?

> > The normal way you do it relies on the Princple of the Excluded middle,
> > which of course cannot be part of the semantic web.
> 
> Why not?  Well, of course, I don't want to deduce anything just because
> some web page says X and some other web page says not X, but there are lots of
> formalisms that don't have this property and that have the Law of the
> Excluded Middle.
> 
> Don't throw away the Law of the Excluded Middle without seeing what you are
> in for.  I spent some time working with relevance logics (that really throw
> away the Law of the Excluded Middle) and they are incredibly difficult to
> understand.  Other logics that reduce the power of the Law of the Excluded
> Middle, like intuitionistic logics, are also difficult.

I agree that it's hard to train my brain to make arguments
without using the LEM, but in my experience building
Semantic Web agents, I haven't wanted nor needed it yet.

(of course, I get along with very little use of negation
at all. I only use stuff like string-inequality
and log:notIncludes).


> > > Why is there a problem?  The problem arises, as Pat has stated, from the
> > > attempt to extend a representation formalism while not extending the
> > > syntax.  This cannot be done in many circumstances and can only be easily
> > > done in very limited circumstances.
> > 
> > I need to understand better where the problem lies.
> 
> Unfortunately, understanding the problem does require groking some
> interesting logical notions.

I think I grok the relevant stuff... from what I can tell,
you do have to be a bit careful, but it's not impossible.
KIF's wtr is an example of a solution, no?

i.e. TimBL's log:Truth is pretty much the same thing
as KIF's wtr. And log:implies works sorta like:

(defrelation (log:implies ?P ?Q) <=>
  (wtr '(implies ,?P ,?Q))

it interacts somewhat strangely with quantification.
For details, see

  a formal design for RDF/N3 context/scopes
  Dan Connolly to www-rdf-logic, Thu, Sep 06 2001
  http://lists.w3.org/Archives/Public/www-rdf-logic/2001Sep/0004.html


-- 
Dan Connolly, W3C http://www.w3.org/People/Connolly/

Received on Friday, 11 January 2002 21:47:18 UTC