Re: Layering bug

I guess you meant such statements as
owl:Thing owl:equivalentClass owl:Nothing .
I'm now completely agnostic on owl:Thing as I
also can't make any sense of
owl:Thing owl:oneOf (:a :b :c).
in any global sense; same for owl:Class btw.
So Jeremy's non-mon example is for
the three cases A |= B, A* |= B, A** |= B
not provable seems to me.

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/


                                                                                                                                       
                      pat hayes                                                                                                        
                      <phayes@ihmc.us>         To:       www-webont-wg@w3.org                                                          
                      Sent by:                 cc:                                                                                     
                      www-webont-wg-req        Subject:  Re: Layering bug                                                              
                      uest@w3.org                                                                                                      
                                                                                                                                       
                                                                                                                                       
                      2003-07-02 10:19                                                                                                 
                      PM                                                                                                               
                                                                                                                                       
                                                                                                                                       





Coming rather late to this discussion, I am surprised that OWL DL
allows one to assert that the universe is empty. This would not
normally be considered to be a consistent assertion in first-order
logic (it would in a free logic, but free logics have other
unintuitive properties). Allowing the universe to be empty means that
assertions like

(forall (?x) (P(?x) and not P(?x)))

are consistent, since they are true in an interpretation with an
empty universe. In fact, any universal assertion is true in such an
interpretation, even (forall (?x) False). Is this really what one
wants to have in OWL DL? It plays havoc with most proof systems for
conventional logics, and would mean that OWL DL could not be
translated into a conventional logical notation in a conventional way.

Pat
--
---------------------------------------------------------------------
IHMC         (850)434 8903 or (650)494 3973   home
40 South Alcaniz St.           (850)202 4416   office
Pensacola                                  (850)202 4440   fax
FL 32501                                   (850)291 0667    cell
phayes@ihmc.us       http://www.ihmc.us/users/phayes

Received on Wednesday, 2 July 2003 18:18:30 UTC