At 07:19 AM 1/13/2006, you wrote:
>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. (01)
But these decisions are your decisions. Each of us can point to
similar stacks of accumulated wisdom. It is thus probably a good idea
if we henceforth all avoid disparaging others because they want 'to
put their own pet theories into the core'. (02)
>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. (03)
And my proposal is to find the highest common factor in all of the
sensible solutions, and to put that in the core. (04)
>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." (05)
No axioms at all?
Or when in doubt leave out? (06)
> 2. For the choice of logic, I recommend the draft ISO standard
> for Common Logic (CL):
> 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, (07)
It does not. It uses FOL, with a restricted range of predicates (all
of them are formal, like identity, part_of, instantiates, and so
forth) and uses variables ranging over both universals and
particulars. It has the standard axioms for identity, part_of,
instantiates, etc., and is consistent with both 3Dimensionalist and
4Dimensionalist and 3+4Dimensionalist doctrines as to the nature of dogs, etc.
Message Archives: http://colab.cim3.net/forum/ontac-forum/
To Post: mailto:ontac-forum@xxxxxxxxxxxxxx
Shared Files: http://colab.cim3.net/file/work/SICoP/ontac/