Barry, (01)
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. (02)
JS>> I am trying to keep as much as possible *out* of the core. (03)
BS> A priori; and drawing conclusions as to what is possible
> on the basis of whose theory of what should be on it? (04)
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. (05)
To keep the ontology as general as possible, I recommend
the following two principles: (06)
1. The required core should avoid any commitment that might
be inconsistent with future scientific discoveries or new
mathematical, computational, and engineering techniques. (07)
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. (08)
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). (09)
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. (010)
Following are some related considerations that we should discuss: (011)
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." (012)
2. For the choice of logic, I recommend the draft ISO standard
for Common Logic (CL): (013)
http://cl.tamu.edu/docs/cl/32N1377T-FCD24707.pdf (014)
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. (015)
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. (016)
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: (017)
http://www.jfsowa.com/pubs/laws.htm (018)
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. (019)
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. (020)
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.) (021)
There is a lot more to be said about these and other issues, but I'll
stop here for now. (022)
John Sowa (023)
_________________________________________________________________
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 (024)
|