ontac-forum
[Top] [All Lists]

RE: [ontac-forum] Re: The world may fundamentally be inexplicable

To: "ONTAC-WG General Discussion" <ontac-forum@xxxxxxxxxxxxxx>
Cc: guarino@xxxxxxxxxx, CG <cg@xxxxxxxxxx>
From: "West, Matthew R SIPC-DFD/321" <matthew.west@xxxxxxxxx>
Date: Fri, 13 Jan 2006 09:18:37 -0000
Message-id: <A94B3B171A49A4448F0CEEB458AA661F02CE4F9A@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>
Dear John,    (01)

I was reflecting on what you had been saying and wondering
"Why would there even need to be ONE core?" when I read this
in your response to Barry below.    (02)

     The most general upper level would have no axioms at all,
     except perhaps the default, "There exists something."    (03)

It strikes me that we should be able to allow what turns out
to be common to float to the top, rather than have to decide
what it is at the outset. At lower levels this will even be
an important capability for a lattice of theories. So I support
a minimalist start.    (04)


Regards    (05)

Matthew West
Reference Data Architecture and Standards Manager
Shell International Petroleum Company Limited
Shell Centre, London SE1 7NA, United Kingdom    (06)

Tel: +44 20 7934 4490 Mobile: +44 7796 336538
Email: matthew.west@xxxxxxxxx
http://www.shell.com
http://www.matthew-west.org.uk/    (07)


> -----Original Message-----
> From: ontac-forum-bounces@xxxxxxxxxxxxxx
> [mailto:ontac-forum-bounces@xxxxxxxxxxxxxx]On Behalf Of John F. Sowa
> Sent: 13 January 2006 06:20
> To: ONTAC-WG General Discussion
> Cc: guarino@xxxxxxxxxx; CG
> Subject: Re: [ontac-forum] Re: The world may fundamentally be
> inexplicable
> 
> 
> Barry,
> 
> We agree on a number of important points:  the need for clear
> distinctions of type/subtype, type/instance, part/whole, and
> the use of formal logic for expressing the definitions and
> axioms of an ontology.  But there are many issues about how
> much to include in the upper levels, how to organize them,
> and what version of logic to use.
> 
> JS>> I am trying to keep as much as possible *out* of the core.
> 
> BS> A priori; and drawing conclusions as to what is possible
> > on the basis of whose theory of what should be on it?
> 
> Not a priori.  The decisions should be based on fundamental
> principles of logic, linguistics, physics, and philosophy
> together with considerations of the accumulated wisdom by
> the software development community over the past fifty years.
> 
> To keep the ontology as general as possible, I recommend
> the following two principles:
> 
>   1. The required core should avoid any commitment that might
>      be inconsistent with future scientific discoveries or new
>      mathematical, computational, and engineering techniques.
> 
>   2. Detailed methods of analysis and reasoning are the most
>      likely to introduce inconsistencies with other detailed
>      techniques.  Therefore, they should be kept in optional
>      modules that may be used, as needed, for specific problems
>      or application areas.
> 
> The recent exchange of notes between Michael Gruninger and
> me illustrates the kinds of things that are likely to create
> inconsistencies.  Michael wants the Process Specification
> Language (PSL) and the associated reasoning method of situation
> calculus to be included in the core, but I maintain that it
> should not be in the core because it is inconsistent with the
> more general pi calculus (and related special cases, which
> include Petri nets and UML activity diagrams).
> 
> Although I prefer the pi calculus, I would recommend that my
> preference, Michael's preference, and many other versions should
> *all* be put in optional modules, *not* in the core.  The reason
> for excluding all of them from the core is that any of them could
> be a reasonable choice for some problem, but their conjunction
> is inconsistent.  Therefore, *none* of them belong in the core.
> 
> Following are some related considerations that we should discuss:
> 
>   1. Adding axioms to a theory makes it more specialized and
>      enables more theorems to be proved.  The ability to prove
>      more theorems is often useful, but one unfortunate axiom
>      can create inconsistencies with entire branches of science.
>      The most general upper level would have no axioms at all,
>      except perhaps the default, "There exists something."
>      More would be useful, but it is always easier to add axioms
>      than to delete any that have been in use for some time.
>      Therefore, I would suggest, "When in doubt, leave it out."
> 
>   2. For the choice of logic, I recommend the draft ISO standard
>      for Common Logic (CL):
> 
>      http://cl.tamu.edu/docs/cl/32N1377T-FCD24707.pdf
> 
>      CL is a very general version of first-order logic, which also
>      supports quantification over relations while still preserving
>      a first-order model theory (see the document for details).
>      It includes the semantics of RDF and OWL as proper subsets, and
>      it supports most common versions of FOL, including typed or
>      sorted versions, such as Z, conceptual graphs, and many others.
> 
>   3. Although I have been on the committee that developed the CL
>      standard and I wrote Appendix B, which maps the CL semantics
>      to conceptual graphs, the version of semantics adopted for CL
>      was not my first choice.  It was developed by Pat Hayes and
>      Chris Menzel, and it's very different from the typed CG semantics
>      I had been using for many years.  But after working with the
>      CL semantics for some time, I became convinced that both Z and
>      something similar to, but more general than my original CG
>      semantics could be defined on top of CL.  In Appendix B, I
>      defined both a typeless core notation and an extended typed
>      version of CGs.  The method used to define typed CGs on top
>      of the typeless core could also be used to support Z and many
>      other typed or sorted versions of FOL.
> 
>   4. I realize that BFO uses modal logic, and so do the research
>      versions of conceptual graphs, which support a rich variety
>      of intensional logics for representing natural language
>      semantics.  Since those are still research topics, I would
>      not suggest that they be included in the CL standard.
>      However, it is possible to define a variety of modal and
>      intensional logics (in any notation for logic, graphic or
>      linear) on top of CL by the methods of the following paper:
> 
>         http://www.jfsowa.com/pubs/laws.htm
> 
>   5. In any case, there are serious questions about how any version
>      of modal logic should be incorporated into an ontology.  In
>      that laws.htm paper, I adopt a version of Dunn's semantics for
>      modal logic, which is formally equivalent to the possible worlds
>      semantics of Kripke, Montague, and others, but instead of using
>      possible worlds, it partitions the propositions into a set of
>      facts and a set of laws, which are a privileged subset of the
>      facts.  For any proposition p, (Necessary p) means that p is
>      provable from the laws, and (Possible p) means that p is
>      consistent with the laws.
> 
>   6. In the KL-ONE predecessor to the modern description logics, there
>      was a clear distinction between the T-Box 
> (Terminological component)
>      and the A-Box (Assertional component).  In effect, the T-Box used
>      an early version of description logics for defining an ontology,
>      and the A-Box used the terms (or predicates) defined in the T-Box
>      to make assertions.  Many people who talked about description
>      logics said that they had a "modal effect", but it was not the
>      DLs themselves that introduced modality, but the fact that the
>      T-Box had a privileged (or more deeply entrenched) role with
>      respect to the A-Box.  In effect, they were using a version of
>      Dunn's semantics in which the T-Box specified the laws, and the
>      A-Box was required to be consistent with the laws.  Therefore,
>      there was an implicit necessity operator in front of every T-Box
>      statement.
> 
>   7. I would claim that the distinction between an ontology and any
>      application that uses the ontology establishes a distinction of
>      the same kind as Dunn's semantics of laws and facts or the KL-ONE
>      T-Box and A-Box.  Therefore, every proposition p in an ontology
>      has an implicit modal operator (Necessary p) in front of it.
>      Adding another operator in the form (Necessary (Necessary p))
>      would imply (Necessary p) in all versions of modal logic, and
>      it would be exactly equivalent to (Necessary p) in many versions.
>      Therefore, I do not believe that there is a need to use explicit
>      modal operators in the ontology.  (Although I believe that it
>      would be useful to use various modal operators in other areas.)
> 
> There is a lot more to be said about these and other issues, but I'll
> stop here for now.
> 
> John Sowa
> 
>  
> _________________________________________________________________
> Message Archives: http://colab.cim3.net/forum/ontac-forum/
> To Post: mailto:ontac-forum@xxxxxxxxxxxxxx
> Subscribe/Unsubscribe/Config: 
> http://colab.cim3.net/mailman/listinfo/ontac-forum/
> Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
> Community Wiki: 
> http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCo
ordinatingWG    (08)



_________________________________________________________________
Message Archives: http://colab.cim3.net/forum/ontac-forum/
To Post: mailto:ontac-forum@xxxxxxxxxxxxxx
Subscribe/Unsubscribe/Config: 
http://colab.cim3.net/mailman/listinfo/ontac-forum/
Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/
Community Wiki: 
http://colab.cim3.net/cgi-bin/wiki.pl?SICoP/OntologyTaxonomyCoordinatingWG    (09)
<Prev in Thread] Current Thread [Next in Thread>