SWCLOS: A Semantic Web Reasoner on CLOS
OWL Subsystem
OWL Error Module
IT Program Project in Japan:
This code is written by Seiji Koide at Galaxy Express Corporation, Japan,
for the realization of the MEXT IT Program in Japan.
Copyright (c) 2003, 2004, 2006 by Galaxy Express Corporation
Copyright (c) 2007, 2008, 2009, 2010 Seiji Koide
| Top error for unsatisfiability in OWL universe |
| Top warning for unsatisfiability in OWL universe |
| unsatisfiable warning in oneOf |
| unsatisfiable in equivalentClasses |
| unsatisfiable warning in equivalentClasses |
| unsatisfiable in disjointWith |
| unsatisfiable warning in disjointWith |
| unsatisfiable in complementOf |
| unsatisfiable warning in complementOf |
| unsatisfiable warning in sameAs |
| unsatisfiable in differentFrom |
| unsatisfiable warning in differentFrom |
| unsatisfiable in cardinality |
| unsatisfiable warning in cardinality |
Seiji Koide Nov-15-2010
OWL Kernel Module
IT Program Project in Japan:
This code is written by Seiji Koide at Galaxy Express Corporation, Japan,
for the realization of the MEXT IT Program in Japan.
Copyright (c) 2003, 2004, 2006 by Galaxy Express Corporation
Copyright (c) 2007, 2008, 2009, 2010 Seiji Koide
Loading this file onto RDF modules creats the OWL universe as part of the RDF universe.
............................
: : :
rdf-node --------------------rdfs:Class --:-----owl:Class --- owl:Restriction
: / : :......: /
: ...../.......: /
: : / : /
: : / +------:-- owl:Thing
: : / / :
gnode --- rdfs:Resource --- rdf:Property
<--, / super/sub class relation, the direction of super is right to left.
..., : class/instance relation, the direction of class is upward and left to right.
Compatibility between RDF and OWL Universes in SWCLOS
W3C specifies two styles on the compatibility between RDF universe and OWL universe.
One is called OWL Full style in which rdf:Class is identical to owl:Class, rdfs:Resource is
identical to owl:Thing, and rdf:Property is identical to owl:ObjectProperty. Another is
called DL style and in which the semantics does not follow RDF semantics. The class
extensions between owl:Thing, owl:Class, and owl:ObjectProperty are mutually disjoint.
See, http://www.w3.org/TR/owl-semantics/rdfs.html.
In SWCLOS implementation, owl:Thing is a subclass of rdfs:Resource, owl:Class is a subclass
of rdfs:Class, and owl:ObjectProperty is a subclass of rdf:Property. Thus, OWL universe is
included in RDF universe, and the semantics of RDF is realized in OWL unvierse due to the
CLOS Object-Oriented ususal manner.
OWL Full Semantics (classes are also instances).
In OWL Full, every class can be an instance of metaclass(es). This is naturally realized in
SWCLOS with owl:Class subclassing to rdfs:Class (eventually to cl:standard-class). In
addition, we set owl:Class as subclass of owl:Thing (eventually to rdfs:Resource). Thus,
classes in OWL (the extension of owl:Class) inherit the slots of rdf:Resource, rdfs:label,
rdfs:comment, rdf:type, etc. from rdfs:Resource.
OWL Property Slot Definition
| Every slot of which name corresponds to RDF property is defined as an instance of
Property-direct-slot-definition. This variable is set to symbol
gx::Property-direct-slot-definition in RDFS module and set to
OwlProperty-direct-slot-definition in OWL module. |
owl:Class and owl:Thing with Houskeeping Slots
Note that the following programming style is useful to use SWCLOS as APIs for applications
that extend semantics of RDF(S) or OWL.
Before loading RDF(S) or OWL knowledge into SWCLOS, you can define the housekeeping or
application specific methods at CLOS objects and classes in the ontology of application,
then load the ontology in RDF(S) or OWL.
Adding function of SWCLOS in RDF semantics adds new definition without any collisions onto
CLOS slot definitions and methods. As a result, you can obtain ontological knowledge and
application methods around ontologies.
In case of no extension of OWL semantics, you can define application methods after loading
OWL ontologies.
We add two new slots into resource objects, funprop-inverse that is the inverse pointer of
a property of owl:FunctionProperty and inverse-funprop-inverse that is the inverse pointer
of a property of owl:InverseFunctionProperty.
| The meta class in OWL universe. This class is a subclass and instance of
rdfs:Class. |
| The top class in OWL universe. This class is a subclass of rdfs:Resource
and instance of owl:Class. |
| returns nil if no definition on owl:equivalentClass. |
| returns a list of equivalences to c. Note that this function
returns one element list of c, when no equivalences defined. |
| Is this obj an instance of owl:Class?
Note that owl:Class and owl:Restriction is not owl class. |
| If you are sure that class is a metaobject of CLOS, use this instead of
(cl:subtypep class owl:Class). |
| Is this bound value to symbol is owl class? |
| returns nil if no definition on owl:sameAs. |
| returns a list of sames as x. Note that this function
returns one element list of x, when no same individuals defined. |
| Is this obj an instance of owl:Thing?
Note that owl:Class and owl:Thing is not owl thing. |
| If you are sure that class is a metaobject of CLOS, use this instead of
(cl:subtypep class owl:Thing). |
Note the domain & range of owl:equivalentProperty is rdf:Property rather than
owl:ObjectProperty.
Object Property for owl:inverseOf Book-keeping
| This class defines an inverse slot of the inverse-of property. |
| change-class (instance
Property) (new-class
Class) &rest initargs |
[method] |
|---|
| In case that new-class is owl:ObjectProperty, the domain of instance is retrieved and
slot definitions named its domain for instance is changed to an instance of
OwlProperty-direct-slot-definition. |
Restriction Subclasses
| owl:Restriction is a metaclass a subclass of owl:Class in OWL. |
| The default direct superclass of restrictions is rdfs:Resource. |
| A class for value restrictions is a subclass of owl:Restriction. |
| name (object
allValuesFromRestriction) |
[method] |
|---|
| print-object (obj
someValuesFromRestriction) stream |
[method] |
|---|
| name (object
someValuesFromRestriction) |
[method] |
|---|
| name (object
hasValueRestriction) |
[method] |
|---|
OneOf class
Note that oneOf elements may be in the RDF universe.
Note that the domain of owl:oneOf is rdfs:Class. Namely,
The owl:oneOf slot definition is attached to rdfs:Class.
| Is this x an object that holds owl:oneOf data? |
How to Calculate a Type Value in Effective Slot Definition in OWL
After the calculation of initargs as standard slot definition and rdf property slot
definition, the type option is recalculated, if OWL module is loaded. Because, it may
include existential restriction for slot value, and it must be treated in OWL semantics.
The form of type option is one of the followings.
<fval> ::= t | <class-meta-object> | (and <fval> ...) |
(forall <slot-name> <fval>) | (exists <slot-name> <fval>) |
(fills <slot-name> <fval>)
(<= <slot-name> <fval>) | (>= <slot-name> <fval>) |
(= <slot-name> <fval>)
Here, class-meta-object is a class object which comes from direct slot definition in RDF,
(and fval ...) is computed by excl::compute-effective-slot-definition-initargs method
at standard slot definition, (forall slot-name fval) originates from owl:allValuesFrom
constraint and (exists slot-name fval) originates from owl:someValuesFrom constraint.
(fills slot-name fval) represents owl:hasValueRestriction.
On the other hand, (<= slot-name fval) is from owl:minCardinality,
(>= slot-name fval) is from owl:maxCardinality, and (= slot-name fval) is from
owl:cardinality.
To compute the most specific concepts which include the above special fval forms,
most-specific-concepts-for-slotd-type, strict-supertype-p-for-slotd-type and
strict-subtype-p-for-slotd-type are defined, which specifically process these fval
with subsumed-p and owl-equivalent-p.
If initargs in making an effective-slot-definition includes :maxcardinality or
:mincardinality keyword, the slot-definition must be OwlProperty-direct-slot-definition.
| This method calls next method if there is no :maxcardinality keyword in initargs. |
Default Super Class in OWL
If v is typed to owl:Class, then v is subtyped to owl:Thing.
In order to set up the anonymous class for (owl:Class (owl:complementOf owl:Nothing)) of owl:Thing
(owl:Class owl:Thing (rdfs:label "Thing") (owl:unionOf owl:Nothing (owl:Class (owl:complementOf owl:Nothing))))
this rule must be defined before reading the OWL file.
| change-class (from
Class) (to
Thing) &rest initargs |
[method] |
|---|
| This is happen when from is class in RDF and it is changed into OWL. |
Here OWL rdf file is read.
Note that
(rdfs:Class owl:FunctionalProperty (rdfs:subClassOf rdf:Property))
(rdfs:Class owl:InverseFunctionalProperty (rdfs:subClassOf owl:ObjectProperty))
Then, we add owl:Functional&InverseFunctionalProperty
We add some new axioms for OWL.
For OWL Full, an owl class also inherit owl:Thing
%addForm for OWL
Calling sequence: %addForm (type slots role)
When type is an undefined symbol as resource,
- If type is a symbol rdf:Description and role is a symbol owl:intersectionOf,
owl:unionOf, then owl:Class is used for type. See, rule2a and rule2b.
- If role is a symbol owl:distinctMembers or owl:oneOf, then owl:Thing is used for type.
See. rule3.
| This is same as one in RDFS module except owl:intersectionOf, owl:unionOf returns owl:Class,
and owl:oneOf returns owl:Thing instead of rdf:List. |
| change-class (from
class) (to
class) &rest initargs |
[method] |
|---|
| change-class (class
Class) (new-class
(eql
Class)) &rest initargs |
[method] |
|---|
| change-class (class
Class) (new-class
Class) &rest initargs |
[method] |
|---|
Seiji Koide Nov-15-2010
OWL Same/Different Module
IT Program Project in Japan:
This code is written by Seiji Koide at Galaxy Express Corporation, Japan,
for the realization of the MEXT IT Program in Japan.
Copyright (c) 2003, 2004, 2006 by Galaxy Express Corporation
Copyright (c) 2007, 2008, 2009, 2010 Seiji Koide
Functional Property
owl:FunctionalProperty is an instance of rdfs:Class.
(rdfs:Class owl:FunctionalProperty
(rdfs:label "FunctionalProperty")
(rdfs:subClassOf rdf:Property))
owl:FunctionalProperty does not belong to OWL universe, and an instance of
owl:FunctionalProperty may not belong to OWL universe.
| returns true if name is an owl functional property name |
| Is this obj an instance of owl:FunctionalProperty? |
Inverse Functional Property
owl:InverseFunctionalProperty is an instance of rdfs:Class.
(rdfs:Class owl:InverseFunctionalProperty
(rdfs:label "InverseFunctionalProperty")
(rdfs:subClassOf owl:ObjectProperty))
An instance of owl:InversefunctionalProperty may not be an instance of
owl:ObjectProperty. Then, the range value may not be owl:Thing and may be rdfs:Literal.
| Is this obj an instance of owl:InverseFunctionalProperty? |
sameAs
| returns true if x and y is defined as the same in OWL semantics.
x and y should be neither a symbol nor an iri. |
| returns true if x and y is defined as the same in OWL semantics.
x and y may be a symbol or an iri. |
| %owl-same-p (x
Resource) (y
Resource) &optional pairs |
[method] |
|---|
| Non-resolution version. This is used in owl-equalp and owl-equivalent-p. |
owl-different-p
| Is x different from y as individual in semantics of OWL? |
| returns true if x and y are definitely different and have no possibility of unification. |
differentFrom
Seiji Koide Nov-15-2010
OWL Equivalent/Disjoint Module
IT Program Project in Japan:
This code is written by Seiji Koide at Galaxy Express Corporation, Japan,
for the realization of the MEXT IT Program in Japan.
Copyright (c) 2003, 2004, 2006 by Galaxy Express Corporation
Copyright (c) 2007, 2008, 2009, 2010 Seiji Koide
Equivalency as Class
owl:equivalentOf, owl:intersectionOf, owl:unionOf, owl:complementOf, and owl:oneOf are
complete relation. Therefore, at these relation the equivalency as class at righthand
side implies the equivalency as class at lefthand side.
equivalentClass
| owl:equivalentClass is a subproperty of rdfs:subClassOf, so
the objects are automatically captured as subclasses in nature.
However, this characteristics is very tricky and bad for construction of stable ontology.
Therefore, the class is not asserted as subclass. |
| If both x and y have an intersection of concepts and two sets of intersection are
equivalent as class, then x and y is equivalent as class. If either or neither has an
instersection, then returns false. |
| If both x and y have an union of concepts and two sets of union are equivalent as class,
then x and y is equivalent as class. |
| If two OneOf sets are set-equal, then both are equal as class.
sets are test by owl-same-p. |
| returns true if x and y are equivalent classes. |
| returns true if x and y are equivalent classes. |
| This subsubfunction prevents recursive call for %owl-equivalent-p. |
| returns true if x and y are equivalent classes or equal literals, symbols,
and objects. At first, x and y should be a class. |
Disjointness
When equivalent classes are given for arguments as disjoint classes, the unsatisfiable error
happens. Note that two concepts in disjointness cannot make intersection, and multiple
classing.
Not only from the disjoint statement, but also owl:intersectionOf values and owl:oneOf
values decide the disjointness. Namely, if two values for such complete relational properties
are disjoint, then the arguments are disjoint.
| special rules of disjointness in OWL.
This function is used internally in routines of default reasoning for disjointness.
Namely, it returns nil nil if the disjointness is explicitly not stated. |
| simply checks the satifiability among supers of class. |
| This predicate cannot be applicable to slot type option. |
| simply checks the satifiability among slot type option types of class. |
| This should be called in computation of slot type option inheritance. So,
the role or owl:onProperty of c1 and c2 must be equal. |
| returns true if xinter and yinter are disjoint.
This function returns true if either of args has intersection,
and returns unknown if neither of args has intersection. |
disjointness in OWL universe is ????
| returns true if c and d are disjoint in OWL. |
NNF transformation module
This program is borrowed from AIMA
2008, 2009 (c) Seiji Koide
| Return a list of the conjuncts in this sentence. |
| Return a list of the disjuncts in this sentence. |
| An atomic clause has no connectives or quantifiers. |
| A literal is an atomic clause or a negated atomic clause. |
| A negative clause has NOT as the operator. |
| Return a CNF expression for the disjunction. |
| ->cnf p &optional vars |
[function] |
|---|
| Convert a sentence p to conjunctive normal form [p 279-280]. |
| Convert a sentence p to implicative normal form [p 282]. |
| logic sentence |
[function] |
|---|
| Canonicalize a sentence into proper logical form. |
| Is x a variable (a symbol starting with ?)? |
| Create a new variable. Assumes user never types variables of form $X.9 |
| Concatenate the args into one string, and turn that into a symbol. |
| Within the proposition P, replace each of VARS with a skolem constant,
or if OUTSIDE-VARS is non-null, a skolem function of them. |
| Return a unique skolem constant, a symbol starting with '$'. |
Followings are by Seiji
Unification with Type
This program is encoded by Seiji Koide based non-typed unifier of
"Paradigms of AI Programming: Case Studies in Common Lisp",
by Peter Norvig, published by Morgan Kaufmann, 1992.
This program is integrated to SWCLOS, an OWL processor on CLOS.
2008,2009 (c) Seiji Koide
| Indicates unification failure |
| Indicates unification success, with no variables. |
| Find a (variable . value) pair in a binding list. |
| Get the variable part of a single binding. |
| Get the value part of a single binding. |
| lookup var bindings |
[function] |
|---|
| Get the value part (for var) from a binding list. |
| Add a (var . val) pair to the head of a binding list. |
| Does var occur anywhere inside x? |
| Substitute the value of variables in bindings into x,
taking recursively bound variables into account. |
- variable is a lisp symbol with starting '?' character.
- constant is a lisp symbol without starting '?' character.
- skolem function is a conce cell.
- individual is a resource object as individual.
- class is a resource object as class.
- metaclass is a resource object as metaclass.
This bindings simulate the environment for lisp symbol bindings.
The virtual value of this bindings supersedes the actual symbol value.
| simulates 'symbol-value' in lisp with bindings. |
| name+ object bindings |
[function] |
|---|
| simulates class-of but cbindings is prior to actual class. |
A variable is a symbol whose name starts with character #\?.
See also NNF for variable? and new-variable.
| Return a list of all the variables in EXP. |
| Return a list of leaves of tree satisfying predicate,
with duplicates removed. |
| Does predicate apply to any atom in the tree? |
| Replace all variables in x with new ones. |
Followings are simulate owl-same-p, different-p, owl-equivalent-p,
subtypep, disjoint-p on bindings and cbindings. These functions
are used in the typep unification program.
| can x and y be regarded as same with bindings? |
| can x and y be regarded as different with bindings? |
| can c and d be regarded as equivalent class with cbindings? |
| is c a subtype of d with cbindings?
Note that cl:subtypep is used. |
The bindings in lisp provide the base level bindings in unification.
The bindings in unification provides situated bindings that change in situation.
The unify implementation in "Paradigms of AI Programming" is just same as the symbol
bindings in old lisp system by association list. So, the mechanism of old lisp
binding is utialized for situated binding and classing in unification.
Typed Unification
| unify x y &optional bindings cbindings kbindings |
[function] |
|---|
| tunify c d &optional cbindings kbindings |
[function] |
|---|
| ttunify c d &optional kbindings |
[function] |
|---|
| unify-var var x bindings cbindings kbindings |
[function] |
|---|
| Both x and y are skolem function that originate existential quantification.
In SWCLOS, it represents a successor in a binary relation of (role predecessor successor). |
| unify-xskolem x y bindings cbindings &optional kbindings |
[function] |
|---|
| Only x is a skolem function that originate existential quantification. |
| unify-yskolem x y bindings cbindings &optional kbindings |
[function] |
|---|
| Only y is a skolem function that originate existential quantification. |
| Return something that unifies with both x and y (or fail). |
Subsume Module
This code is written by Seiji Koide.
Copyright (c) 2009 Seiji Koide
Subsumption
| tests whether c is subsumed by d in OWL semantics. |
| subsumtion test without class equivalency of cc and dd for CLOS objects. |
| returns unfolded concepts of conj, if conj is an intersection in OWL,
otherwise returns conj itself. |
Models
models := ( model* )
model := ( bindings cbindings . cmax cmin atoms )
atoms := ( atom* )
atom := ( role predecessor successor )
predecessor and successor is a var.
- models are disjunction of models.
- atoms are conjunction of atomic formula in logic.
- atom may be general logical form, but should be a binary form in this program.
- cbindings provides concept (class) bindings for logical variable.
- bindings is usual one.
- role is a lisp symbol.
- class is a resource object.
| var is a role-predecessor. |
| creates a model from universal var and restriction conjuncts.
Note that all properties in conjuncts are is role. |
| clash-p bindings cbindings conjuncts |
[function] |
|---|
| tests conjuncts clashing or not. |
| adds a new atom of (role predecessor successor:exist) into model,
and returns a satisfiable model. Note this function is applied for existential
quantification of successor. |
| imposes a new atom of (role predecessor successor:type) onto each atom in atoms
and returns a satisfiable model for bindings, cbindings, and atoms.
Note that the cardinality of atoms do not increased but bindings may be extended and
cbindings are extended. If the conjunction is clashed, this function returns nil. |
| generates updated models for var and role onto models with constraint
cmax, cmin, types, alls, exists, and fillers of role-successor. |
| generates updated models for var and role onto models with constraint
max caridinality cmax, types, alls, exists, and fillers of successor
of var for role. If var is nil, then new-var is created inside. |
| exists are a list of types for (role var y1:type1), (role var y2:type2) ... |
Transitive Property
| Is this obj an instance of owl:TransitiveProperty? |
| same prodedure as %rdf-subtypep but calls subsumed-p instead-of %rdf-subtypep or
%owl-subtypep. Conjuction is specially treated as same way of subsumed-p. |
OWL Module
IT Program Project in Japan:
This code is written by Seiji Koide at Galaxy Express Corporation, Japan,
for the realization of the MEXT IT Program in Japan.
Copyright (c) 2003, 2004, 2006 by Galaxy Express Corporation
Copyright (c) 2007, 2008, 2009 Seiji Koide
owl-equalp checks the equality of objects in OWL, namely it returns t, if
- owl-equivalent-p holds, if args are property.
- if args are restrictions, then if both of owl:onProperty values are equal and values are
equal as owl:allValuesFrom or owl:someValuesFrom or owl:hasValue,
and either both or neither cardinality restriction are also equal.
- owl-same-p holds.
- otherwise equal in the sense of rdf-graph equality.
| returns true if x and y is equal in semantics of RDF(S) superimposed by OWL.
This predicate checks x and y in classes as individuals. |
Subsumption
(subsumed-p vin:DryWhiteWine vin:WhiteNonSweetWine) -> t
(subsumed-p food:Fruit food:EdibleThing)
| This function directly computes conjuncts instead of C's intersection. This is useful to compute
conjunction (and) without creating an intersection class. |
| This function is used for shared-initialize. |
| returns a set of subclasses of all member of intersections, removing duplicates and
ones that has same intersection as class. |
| returns a set of superclases of all member of unions, removing duplicates and
ones that has same union as class. |
owl:complementOf
intersectionOf
| returns most specific concepts that include subs of classes as intersection's sub.
Note that return values include initial values and newly added values. |
unionOf Shared Initialize After Action
After defining a class with owl:unionOf slot,
- If the defined class class is a subclass of a superclass sib of a union member,
class is inserted between the superclass sib and the union member.
- If the defined class class is not a subclass of a superclass sib of a union member,
class is a sibling of sib.
| change-class (instance
Thing) (new-class
(eql
Class)) &rest initargs |
[method] |
|---|
| change-class (instance
Thing) (new-class
Class) &rest initargs |
[method] |
|---|
Shared-initialize Before for owl:Class
Shared-initialize After for owl:Class
update-instance-for-different-class is called in change-class.
Usually change-class is invoked by ensure-class without initargs.
So, direct-superclasses is set by reinitialize-instance in ensure-class
after change-class. The following routine is prepared only for direct
invocation of change-class by users.
| ensures owl:Thing as superclasses in OWL universe. This routine is effective
only if a user designates :direct-superclasses but no inheritance of owl:Thing. |
Symmetric Property
| Is this obj an instance of owl:SymmetricProperty? |
| book-keeping for reification |
Shared-initialize After for owl:Thing
Warning: Entailed in refining: #vin:WhiteWine vin:StGenevieveTexasWhite
to vin:WhiteNonSweetWine.
owl:equivalentClass is a subproperty of rdfs:subClassOf, so
the objects are automatically captured as subclasses in nature.
However, this characteristics is very tricky and bad for construction of stable ontology.
Because rdfs:subClassOf is substantial relation, but equivalentClass is temporal one.
We treat equivalentClass in inference instead of subproperty of rdfs:subClassOf
or superclass-subclass relation.
| returns an append list of MSCs of restrictions and MSCs of non restrictions in old-users and new-supers. |
Transitivity
Here after Bookkeeping Facilities
owl:AllDifferent
owl:Restriction again
| Is this obj an instance of owl:Restriction? |
owl:intersectionOf is translated to super/subtype relation.
hasValue Restriction sets up an initial value of the slot.
| shared-initialize (class
someValuesFromRestriction) slot-names &rest initargs |
[method] |
|---|
| shared-initialize (class
allValuesFromRestriction) slot-names &rest initargs |
[method] |
|---|
For owl:equivalentProperty
| Are x and y equivalent property in semantics of OWL? |
owl:inverseOf
Property in OWL
We construct every inference upon subsumption-basis.
Subsumption is infered by structural subsumption algorithms, here.
Membership in OWL
The following is taken from http://www.w3.org/TR/owl-ref/#equivalentProperty-def.
"Property equivalence is not the same as property equality. Equivalent properties have the same "values"
(i.e., the same property extension), but may have different intensional meaning (i.e., denote different concepts).
Property equality should be expressed with the owl:sameAs construct. As this requires that properties are
treated as individuals, such axioms are only allowed in OWL Full."
Since we consider the domain and range constraint and OWL onPorperty restrictions are intensional data of properties.
we do not treat here the equivalent property.
We do not implement sameAs functions for properties.
| object and type is an object in RDF universe. |
| This is sub-subfunction for typep. This is only invoked in %%typep.
This function tests type relation for each member of owl:sameAs group. |
| object and type are in RDF universe and no direct class-instance relations.
type may be a complex concept. |
| when every element in intersections satisfies a type of object then true.
If any element does not satisfy obviously, then imediately returns with false.
Otherwise, finally the result for all of intersections is true or unknown. |
slot-value
Cardinality check
| simply checks value with cardinality constraint without models and returns true if no problems.
It is expected that elements in value will be unified if false is returned. |