On Sat, Jan 21, 2006 at 03:58:15PM -0500, Michael Gruninger wrote:
> > In order to resolve a terminological question, we are in the process
> > of voting whether to use the term "Type" or "Class" to refer to
> > those intensionally-defined groupings called:
> >
> > Class in Ontolingua and Protege
> > Class in RDF and OWL
> > Class in SUMO
> > Collection in OpenCyc
> > Universal in DOLCE
> > Property in Ontology Works' IODE system
>
> A vote like this only makes sense if these concepts
> really are equivalent, and I cannot make such a judgment
> without seeing the relevant axioms.
>
> First of all, the above list contains a mix of languages (RDF, OWL)
> and ontologies (OpenCyc, DOLCE). I'm not sure what to call
> Ontolingua, Protege, and IODE.
>
> Can people from the above named ontologies please provide
> the relevant axioms for their terms?
> Common Logic axioms are preferable, but at this point,
> anything is a place to start.
> Can someone please post the axiomatic definitions of
> RDF/OWL Class in Common Logic? (01)
Geez, Michael, what's up with the eminently clear and practical
questions, eh? (02)
One will search in vain for axioms in the RDF/OWL documentation. (One
does find things that are called axioms in the OWL docs (e.g.,
http://www.w3.org/TR/owl-semantics/syntax.html#2.3), but these are
really clauses in the abstract syntax for OWL. They do have certain
semantic consequences, but they are not axioms in the standard sense at
all.) What one does get is a precise grammar that generates the complex
expressions of the languages recursively from their lexical primitives,
which are in turn provided with a model theory. (The model theories for
RDF(S) and OWL are nice and clear, thanks to their primary author, Pat
Hayes.) For reasoning, it appears that entailment questions written in
decidable versions of OWL (Lite and DL) are translated into some form of
description logic syntax and are then handed to a DL reasoner like
RACER. I haven't studied DLs enough to know exactly how that works,
e.g., if there is an underlying set of logical axioms for the DLs in
quesiton, or if it's all done via natural deduction style inference
rules. (03)
The closest one gets to axioms for RDF/OWL is the now rather outdated
"Axiomatic Semantics" document by Deb McGuinness and Richard Fikes,
which covers RDF(S) and the OWL predecessor DAML+OIL. However, Pat
Hayes and I are working on an update of this idea for RDF(S) and OWL. (04)
Re classes in OWL, the model theory for them is fairly weak. There are
the usual boolean operators, including complementation, so it's
obviously not a ZF-style theory. There is also a limited comprehension
schema for generating new classes from given classes and properties.
They are not assumed to be extensional. (05)
Re SUMO, the set/class theory follows. I wrote the original version of
this theory some years ago at the request of Adam Pease, but I don't
recognize much of it anymore. In particular, there's at least one overt
error in the current version -- the "element" relation is asserted to be
intransitive, when in fact it only fails to be transitive -- and they've
insisted on retaining the hopelessly muddled "KappaFn" operator. (06)
-chris (07)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; SUMO SET/CLASS THEORY ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (08)
;; INCLUDES 'STRUCTURAL ONTOLOGY'
;; INCLUDES 'BASE ONTOLOGY' (09)
;; The following part of the ontology covers set-theoretic predicates
;; and functions. Most of the content here is taken from the kif-sets
;; ontology (available on the Ontolingua server). (010)
(subrelation subset subclass)
(domain subset 1 Set)
(domain subset 2 Set)
(documentation subset "(subset ?SET1 ?SET2) is true just in case the
&%elements of the &%Set ?SET1 are also &%elements of the &%Set ?SET2.") (011)
(=>
(subset ?SUBSET ?SET)
(forall (?ELEMENT)
(=>
(element ?ELEMENT ?SUBSET)
(element ?ELEMENT ?SET)))) (012)
(instance element BinaryPredicate)
(instance element AsymmetricRelation)
(instance element IntransitiveRelation)
(subrelation element instance)
(domain element 1 Entity)
(domain element 2 Set)
(documentation element "(element ?ENTITY ?SET) is true just in case
?ENTITY is contained in the &%Set ?SET. An &%Entity can be an &%element
of another &%Entity only if the latter is a &%Set.") (013)
(=>
(forall (?ELEMENT)
(<=>
(element ?ELEMENT ?SET1)
(element ?ELEMENT ?SET2)))
(equal ?SET1 ?SET2)) (014)
(instance UnionFn BinaryFunction)
(domain UnionFn 1 SetOrClass)
(domain UnionFn 2 SetOrClass)
(range UnionFn SetOrClass)
(documentation UnionFn "A &%BinaryFunction that maps two &%SetOrClasses
to the union of these &%SetOrClasses. An object is an &%element of the
union of two &%SetOrClasses just in case it is an &%instance of either
&%SetOrClass.") (015)
(instance IntersectionFn BinaryFunction)
(domain IntersectionFn 1 SetOrClass)
(domain IntersectionFn 2 SetOrClass)
(range IntersectionFn SetOrClass)
(documentation IntersectionFn "A &%BinaryFunction that maps two
%SetOrClasses to the intersection of these &%SetOrClasses. An object is
an instance of the intersection of two &%SetOrClasses just in case it is
an instance of both of those &%SetOrClasses.") (016)
(instance RelativeComplementFn BinaryFunction)
(domain RelativeComplementFn 1 SetOrClass)
(domain RelativeComplementFn 2 SetOrClass)
(range RelativeComplementFn SetOrClass)
(documentation RelativeComplementFn "A &%BinaryFunction that maps two
&%SetOrClasses to the difference between these &%SetOrClasses. More
precisely, the relative complement of one class C1 relative to another
C2 consists of the instances of C1 that are instances of the
&%ComplementFn of C2.") (017)
(instance ComplementFn UnaryFunction)
(domain ComplementFn 1 SetOrClass)
(range ComplementFn SetOrClass)
(documentation ComplementFn "The complement of a given &%SetOrClass C is
the &%SetOrClass of all things that are not instances of C. In other
words, an object is an instance of the complement of a &%SetOrClass C
just in case it is not an instance of C.") (018)
(instance GeneralizedUnionFn UnaryFunction)
(domainSubclass GeneralizedUnionFn 1 SetOrClass)
(range GeneralizedUnionFn SetOrClass)
(documentation GeneralizedUnionFn "A &%UnaryFunction that takes a
&%SetOrClass of &%Classes as its single argument and returns a
&%SetOrClass which is the merge of all of the &%Classes in the original
&%SetOrClass, i.e. the &%SetOrClass containing just those instances
which are instances of an instance of the original &%SetOrClass.") (019)
(instance GeneralizedIntersectionFn UnaryFunction)
(domainSubclass GeneralizedIntersectionFn 1 SetOrClass)
(range GeneralizedIntersectionFn SetOrClass)
(documentation GeneralizedIntersectionFn "A &%UnaryFunction that takes a
&%SetOrClass of &%Classes as its single argument and returns a
&%SetOrClass which is the intersection of all of the &%Classes in the
original &%SetOrClass, i.e. the &%SetOrClass containing just those
instances which are instances of all instances of the original
&%SetOrClass.") (020)
(instance CardinalityFn UnaryFunction)
(instance CardinalityFn AsymmetricRelation)
(domain CardinalityFn 1 SetOrClass)
(range CardinalityFn Number)
(documentation CardinalityFn "(CardinalityFn ?CLASS) returns the
number of instances in the &%SetOrClass or &%Collection ?CLASS.") (021)
(instance NullSet Set)
(documentation NullSet "The &%Set that contains no instances.") (022)
(not (exists (?ELEMENT) (element ?ELEMENT NullSet))) (023)
(subclass FiniteSet Set)
(documentation FiniteSet "A &%Set containing a finite number of
elements.") (024)
(=>
(instance ?SET FiniteSet)
(exists (?NUMBER)
(and
(instance ?NUMBER NonnegativeInteger)
(equal ?NUMBER (CardinalityFn ?SET))))) (025)
(subclass PairwiseDisjointClass SetOrClass)
(documentation PairwiseDisjointClass "A &%SetOrClass of &%Classes is a
&%PairwiseDisjointClass just in case every instance of the &%SetOrClass
is either &%equal to or &%disjoint from every other instance of the
&%SetOrClass.") (026)
(=>
(instance ?SUPERCLASS PairwiseDisjointClass)
(forall (?CLASS1 ?CLASS2)
(=>
(and
(instance ?CLASS1 ?SUPERCLASS)
(instance ?CLASS2 ?SUPERCLASS))
(or
(equal ?CLASS1 ?CLASS2)
(disjoint ?CLASS1 ?CLASS2))))) (027)
(subclass MutuallyDisjointClass SetOrClass)
(documentation MutuallyDisjointClass "A &%SetOrClass of &%Classes is a
&%MutuallyDisjointClass just in case there exists nothing which is an
instance of all of the instances of the original &%SetOrClass.") (028)
(=>
(instance ?CLASS MutuallyDisjointClass)
(forall (?INST1 ?INST2)
(=>
(and
(instance ?INST1 ?CLASS)
(instance ?INST2 ?INST1))
(exists (?INST3)
(and
(instance ?INST3 ?CLASS)
(not (instance ?INST2 ?INST3))))))) (029)
(instance KappaFn BinaryFunction)
(domain KappaFn 1 SymbolicString)
(domain KappaFn 2 Formula)
(range KappaFn SetOrClass)
(documentation KappaFn "A class-forming operator that takes two
arguments: a variable and a formula containing at least one unbound
occurrence of the variable. The result of applying &%KappaFn to a
variable and a formula is the &%SetOrClass of things that satisfy the
formula. For example, we can denote the &%SetOrClass of prime numbers
that are less than 100 with the following expression: (KappaFn ?NUMBER
(and (instance ?NUMBER PrimeNumber) (lessThan ?NUMBER 100))). Note that
the use of this function is discouraged, since there is currently no
axiomatic support for it.") (030)
;; At some point we may be able to make use of 'KappaFn' by implementing
;; a macro ;; that decomposes every occurrence of 'KappaFn' into a
;; complex formula. For example the macro might replace every
;; instance of Schema 1 with an instance of Schema 2.
;; Schema 1: (KappaFn <variable> <formula>)
;;
;; Schema 2: (exists (?LIST)
;; (and
;; (instance ?LIST UniqueList)
;; (forall (<variable>)
;; (<=>
;; (inList <variable> ?LIST)
;; <formula>)))) (031)
_________________________________________________________________
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 (032)
|