(forall (c y ...)(iff
((OR c ...) y)
(or (c y)((OR ...) y))
Notice the null case: it takes a little care to get these right.
(AND) is the universal class, i.e. the universally true predicate, corresponding to
owl:Thing (although with a somewhat wider scope in IKL than in OWL-DL) and
(OR) is the universally false predicate, the empty class. Notice that if we assert that
(ListableRelation AND OR)
then we get the equivalence of
(AND a b ...
(AND(list a b ...
)), corresponding exactly to the OWL use of RDF lists to attach arguments to
owl:intersectionOf and, similarly,
(forall (c y)(iff ((NOT c) y)(not (c y)) ))
In fact, we can mirror all the connectives as similarly named operations on classes, for example
***???*** (forall (c d z)(iff ((IF c d) z)(if (c z)(d z)) ))
although in OWL this particular pattern is described as a relation
owl:subClassOf between classes, rather than as a function on relations. Cyc uses 'genls' for this relationship:
(forall (c d z)(iff (SUBCLASS c d)(if (c z)(d z)) ))
The similar OWL term for
IFF, whose defining axiom is left as an exercise for the reader, is
Description logic restrictions can be similarly seen as packaged pieces of quantifier and connective usage. For example,
owl:allValuesFrom can be rendered as the operator
ALLARE, which takes a binary and a unary relation to a unary relation:
(forall (p c z)(iff ((ALLARE p c) z)(forall (u)(if (p z u)(c u)) ))
(ALLARE BrotherOf Canadian) is a predicate which is true of things all of whose brothers are Canadian. (To illustrate the potential pitfalls of description logic reasoning, this includes cauliflowers, integers and very short pieces of string.) The related OWL construct
owl:someValuesFrom corresponds to this:
(forall (p c z)(iff ((SOMEARE p c) z)(exists (u)(and (p z u)(c u)) ))
These can then be used to construct quite elaborate expressions corresponding to DL class definitions, such as this example taken from the OWL wine ontology [Wine]:
(= WhiteNonSweetWine (AND WhiteWine (ALLARE hasSugar (OR Dry OffDry))))
Another useful DL construct is the explicitly listed class,
owl:oneOf. This is best represented in IKL using a membership operator on an explicit list:
(forall (x y)(iff (member x (list y ...))(or (= x y)(member x (list ...))) ))
(forall (x)(not (member x (list))))
(forall (x (L isList))(iff ((ONEOF L) x)(member x L)))
Finally, DLs provide cardinality restrictions, which can be used to define things like people who have two children and have visited Paris more than once. These operators can be axiomatized in IKL by using numerical quantifiers and one simple arithmetic relation. (With more effort, they can be axiomatized without using numerical quantifiers: see [SW2CL] for details.)
(forall (p x (n ikl:number))(iff
((ATLEAST n p) x)
(exists ((m ikl:number)) (and
(ikl:lesseq n m)
(exists m (y)(p x y))
(forall (p x (n ikl:number))(iff
((ATMOST n p) x)
(exists ((m ikl:number)) (and
(ikl:lesseq m n)
(exists m (y)(p x y))
(forall (p x (n ikl:number))(iff
((EXACTLY n p) x)
(exists n (y)(p x y))
The property mentioned above could then (assuming a suitable basic vocabulary) be described by a single term::
(AND (EXACTLY 2 hasChild)
(ATLEAST 2 (AND isTravelEvent (ALLARE mainDestination (ONEOF (list Paris)))))
All the rest of the OWL vocabulary can be straightforwardly transcribed into IKL: full details are in [SW2CL].
Description languages often use pre-defined datatypes to distinguish constant values of various categories. This can be reproduced in IKL in various ways, but one way is recommended, in which the datatype name plays three roles: as a predicate, to mark lexical welformedness, as a function on strings, and as an identifier. We will illustrate this with the primitive datatypes from the XML Schema datatype specification.
A datatype is thought of as a function, called the lexical-to-value mapping, from a set of character strings, called lexical forms, to a value space. When the datatype name is used as a function name, it denotes the lexical-to-value mapping function: when used as a class name, it indicates the value space. In IKL all functions are total, so a datatype mapping has a value even when applied to a character string (or indeed anything) which is not in its domain. By convention, we require that in this case the value of the datatype function is not in the value space. Thus for example the string '
abc' is not a numeral, so
(xsd:number 'abc') is not an integer, so
(xsd:number (xsd:number 'abc')) is false; similarly,
(xsd:number (xsd:number x)) is false if
x denotes anything other than a character string.
As noted, IKL has special syntax for numerals and character strings, both of which can be regarded as built-in datatypes. IKL uses the reserved names
ikl:string as the names for these datatypes. Thus,
(ikl:number 346) and
(ikl:string '346') are true with any numeral replacing
346 and any quoted string replacing
'346'. If we define
(forall ((x ikl:datatype) (s ikl:string))(iff (LegalStringOf x s)(x (x s))))
LegalStringOf is the relationship between a datatype and its legal lexical forms. Lexical forms are always character strings:
(forall (x (d ikl:datatype))(if (d (d x)) (ikl:string x))
One can think of a datatype D as a name with three roles a function on strings, a predicate on values and a network identifier whose meaning is determined by two infinite but R.E. sets of axioms which determine, for any character string s, either
(D (D s)) or
(not (D (D s))); and for each pair of strings
(D (D s1)) and
(D (D s2)), either
(= (D s1)(D s2)) or
(not (= (D s1)(D s2))). Certain datatypes may provide other extra information also, e.g. the integers in IKL are ordered by
Datatypes are first-class entities in IKL, so can be quantified over, have properties, etc.. For example, one might reasonably assert any of the following:
(= ikl:number xsd:number)
(forall ((x ikl:string))(and (= x (ikl:string x))(= x (xsd:string x)) ))
(forall ((d ikl:datatype) x)(if (d (d x))(ikl:string x) ))
(forall ((d ikl:datatype))(Predicative d) )
The last, in particular, allows one to classify a whole list of things using a single atomic assertion.
As noted, IKL sentences in IKL text are understood as timeless assertions made outside of any particular context. To support the common use of contextual or temporal assertions, understood as being true 'in' a context or 'at' a time, IKL users should treat such sentences as propositions which are asserted to be suitably related to entities such as time-intervals or contexts, and write suitable axioms using propositional terms of the form
) rather than simply <sentence>. IKL imposes no logical constraints on entities such as time-intervals or contexts, nor on the nature or number of the relations which can hold between them and propositions.
Common examples of such relations include ist, a relation between a context and a proposition whose intuitive reading is "is true throughout"; holds, a similar relation between a temporal proposition and a time-interval, and occurs, a relation between (a proposition understood as describing) an action and the interval which exactly contains the action. As with most axiom-writing, IKL can support a large variety of possibilities, so the examples below should be taken as illustrative rather than normative.
[Makarios] distinguishes various cases of how ist might distribute over propositional structure. One way to describe this in IKL would be to use several ist relations, but another is to classify types of context by how they support distribution. (We will state this only for the binary case of conjunction and disjunction, for simplicity: it is easy to show as a meta-theorem that it also follows for the general case.)
(forall (c) (iff
(forall (p q)(iff
(ist c (that (and p q)))
(and (ist c (that p)) (ist c (that q)))
(forall (c) (iff
(forall (p q)(iff
(ist c (that (or p q)))
(or (ist c (that p)) (ist c (that q)))
(forall (c) (iff
(ist c (that (not p)))
(not (ist c (that p)))
The usual convention for holds is that it applies only to atomic sentences. There is no way to easily represent this restriction explicitly in IKL, but the same effect is obtained by allowing holds to distribute freely over the connectives:
(forall ((i timeinterval) p q) (and
(iff (holds i (that (and p q)))(and (holds i (that p))(holds i (that q))))
(iff (holds i (that (or p q)))(or (holds i (that p))(holds i (that q))))
(iff (holds i (that (not p)))(not (holds i (that p))
Other properties of these relationships can be established by suitable axioms, e.g. that holds is preserved over sub-time-intervals:
(forall ((i timeinterval)(j timeinterval) p) (if
(and (holds i (that p))(subintervalOf j i))
(holds j (that p))
When describing contexts involving possible re-interpretations of textual meaning, such as subjective reports of beliefs or overheard conversations, it is important to bear in mind that in IKL names are not re-interpreted in different contexts. A name in IKL text refers to the same 'real' thing wherever it occurs in the text, even inside a proposition name that is being used to represent someone's false beliefs, and even when those false beliefs involve the name itself. If one reads such contextual assertions in the commonly used de dicto way, which is often done, the results can seem unintuitive. To illustrate with a familiar fictional example, Lois Lane knows one person by the names 'Clark Kent' and 'Superman', but believes, wrongly, that these names refer to two different people. We say, informally, Lois doesn't know that Clark is Superman, and it is tempting to render this into IKL by positing a belief-context for Lois in which Clark is not Superman. To do this in IKL, however, requires care over reference. It would be a mistake to assert this:
***WRONG*** (ist LoisBelief (that (not (= Clark Superman)))) ***
since it would follow from this, and the fact
(= Clark Superman) that
(ist LoisBelief (that (not (= Clark Clark))))
and Lois is not that confused.
The first claim seems reasonable because if one were to ask Lois, is it true that Clark is different from Superman?, she would say, yes: so, one feels, she believes it, surely. The IKL view, however, is that she would assent to it not because she believes what it actually says (that someone is not identical to himself), but because she is confused about what it says, and so is in fact agreeing to a different proposition, which could be expressed in IKL as
(that (not (=
which, note, does not use 'Clark' and 'Superman' as logical names. Put another way, in order to adequately describe Lois' confusion, we have to speak explicitly about what she thinks (wrongly) that the names refer to: and to do that, we cannot simply use the names as names which would get to the real referents, not Lois' confused notions of what the referents are but must take a step back away from the actual referents, talk about the names as character strings, and refer to what these strings might denote if the world were really the way that Lois believes it to be.
This suggests a strategy for handling such opaque belief contexts in a referentially transparent logic such as IKL: when a name, when used in some contextual assertion, might refer there to anything other than what it refers to in the actual logical text, the safe strategy is to treat the name as a character string (thereby removing its logical association with its actual referent) and replace uses of the name with a literal term in which the context is used similarly to a datatype, applied to the name string. Such a term can be thought of exactly as a kind of literal, with the context playing the role of a datatype, i.e. as a function on lexical strings which maps them to referents in a fixed way (in this case, determined by the context). We will refer to this as contextual typing or contextual reference. Lois's state of mind can then be described thus:
(ist LoisBelief (that (not (= (LoisBelief 'Clark')(LoisBelief 'Superman')))))
or, assuming that she really does know who Clark Kent, her office colleague, is:
(ist LoisBelief (that (not (= Clark (LoisBelief 'Superman')))))
Although contextual typing imposes a notational burden when writing axioms describing opaque contexts (which are usually related to states of belief in some way), it yields several compensatory benefits. The referential transparency of the overall language simplifies the logic and leads to more coherent reasoning, since equality reasoning can be used throughout all contexts; moreover, these context-reference terms are meaningful outside of their original context, and can be used directly to refer to the (possibly imaginary) entity that Lois believes Superman to be. This enables one to say, for example
(taller (LoisBelief 'Superman') Superman)
One can say Lois knows who Clark is by a simple equation:
(= Clark (LoisBelief 'Clark'))
which is the assumption which justified our re-writing the sentence above.
A similar strategy can be applied to temporal reference, if required. (This is a large topic, here only brief reviewed.) Consider Arthur, a growing boy, and the assertion that he is taller now, in September of 2005, than he was the same time last year in 2004. Such changing facts about an individual, or facts about a changing individual, can be rendered as contextual assertions of time-dependent propositions about Arthur, using holds, or can be stated in terms of 'fluents', a term introduced by McCarthy [SACL] to refer to a relation between things and times, or by using a simple non-temporal relation between temporal 'slices' of Arthur (or, if one prefers this way of talking, of Arthur's lifetime). The latter is similar in spirit to the contextual-reference device described above in that it is the reference to Arthur that is made time-relative, rather than the relation itself, or the assertion of its application to Arthur.
The three styles can be illustrated thus, using a suitable XML schema literal to denote time-intervals, each of a single 24-hour day. The first relativizes propositions to intervals, using holds and that (one could also use ist, as above, provided that intervals are regarded as a type of context):
(exists (x y)(and
(holds (xsd:date '2004-09-01') (that (= (height Arthur) x)))
(holds (xsd:date '2005-09-01') (that (= (height Arthur) y)))
(less x y)
Note that the temporal relativity here is on the proposition, and we are obliged to quantify into it in order to refer to the things it mentions. An accurate English rendering might be: The height that it was true in 2004 that Arthur was, is less than the height it is true in 2005 that he is.
The second uses fluents, by putting the time-interval as an extra argument to the relation, by common convention the last:
(exists (x y)(and
(= (height Arthur (xsd:date '2004-09-01')) x)
(= (height Arthur (xsd:date '2005-09-01')) y)
(less x y)
Note that contextual assertions are no longer required, and this does not use explicit refernces to propositions. In English, roughly: Arthur's height in 2004 is less than Arthur's height in 2005. (The lack of tense in this English rendering is deliberate.)
The third uses temporally qualified references to refer to Arthur at different times. In this case we can dispense with the quantifiers:
(height (during (xsd:date '2004-09-01') Arthur))
(height (during (xsd:date '2005-09-01') Arthur))
during' here plays only a dummy role, in fact, and we could eliminate it and use the date directly as the 'time-slicing' function. The resulting convention is similar to that used earlier for contextual reference, where a context name (here, a term denoting a time-interval) is used to indicate a function which indicates a temporally sensitive reference to its argument:
(height ((xsd:date '2004-09-01')Arthur))
(height ((xsd:date '2005-09-01')Arthur))
and an English rendering might be: Arthur in 2004 is less high than Arthur in 2005.
This last is, as noted above, similar to the technique used for describing Lois' beliefs. It differs however in using the name itself rather than a term constructed from the quoted name. This is appropriate for simple temporal slicing since the plain name Arthur refers to a 'continuant', i.e. something which retains its identity through time, so there is no need to make special accomodation here for the possibility that the name means differnt things at different times. If we were to use a name like PresidentOfTheUSA, intending that to refer to different people when used at different times, then issues of temporal identity would have to be dealt with more explicitly. The 'datatyped' technique used for the earlier Superman example, where a simple name is replaced by a term built from the quoted name, is robust enough to handle any kind of identity condition, but more awkward to axiomatize.
The merits (or otherwise) of these various axiomatic styles, and their relationship to various philosophical views on existence and time, have been extensively debated elswhere. Our main point here is that IKL is ecumenical enough to use them all, and even to state conditions under which they are equivalent :
(forall ((t timeInterval)(r temporallySliceableFunction)(x continuant)(z continuant))
(iff (holds t (that (= (r x) z))) (= (r x t) z)
(forall ((t timeInterval)(r temporallySliceableFunction)(x continuant))
(= (r x t)(r (during t x)))
Both of the above are examples of a general technique for referring to an 'aspect' of a thing, which we tentatively call viewing. The general case is that one has an entity which can be identified as extending through a variety of partial or complete 'worlds'. These worlds might be contexts, time-intervals, possible worlds, mental perspectives, points of view, etc.., and different philosophical terms are typically used in the various cases: but the logical point is, that one wishes to identify a single thing across a variety of such 'worlds', while allowing for this one single thing to have different properties in those different worlds. The viewing technique, then is to consider the 'world' as defining a viewing function from the entity to those parts or aspects of it which give it an identity in that world, ignoring any other aspects or parts. If we think of entities as being some kind of whole or sum of all their aspects in every world, then this function can be viewed as a kind of selector, which filters out aspects which do not belong in the world in question, leaving a kind of reduced entity to which properties and relations can be attributed without having these attributions contaminated or confused by other aspects of the entity which arise only in other perspectives. The most appropriate way to describe this in less abstract language depends on the particular kind of 'world' and 'entity' one is talking about. Thus, for worlds defined by times, it is usual to distinguish event-like occurrents which can be said to have temporal parts, so the time-interval worlds simply contain the contemporary parts from object-like continuants, which go on from day to day, getting a little older but retaining their essential identity, and are not thought of as having temporal parts. Nevertheless, we can clearly distinguish a continuant at one time from the same continuant at a different time, even though these are not thought of as temporal parts of the continuant: the logical/representational technique applies to continuants and occurrents with equal correctness, since both of them can have temporally changing properties. As the Superman example illustrates, the view need not be temporal in nature: it hardly seems appropriate to call Lois' view of Superman a part of Superman in any mereological sense. Nevertheless, it is possible to think of the name "Superman" as attached to a kind of informational complex which includes Lois' distorted view of reality, and which therefore has an imaginary entity, a kind of ur-Superman doppelganger, as a part or aspect of it. (We might perhaps identify this informational complex with the set of all relations in which Superman takes part, since it is a genuine fact about Superman, the real guy, that Lois believes, of him, that he is not Clark Kent.) The use of a viewing technique raises the obvious question of what it means to simply assert something about an object simpliciter, with no reference to a view. Again, the answer seems to depend upon circumstances. For temporal views, it seems natural to assume that a bare assertion applies to all possible views, i.e. it is true of the entity regardless of when it is viewed: (forall (r x (t isTimeInterval))(if (r x) (r (t x))) Such properties seem to include essential or 'rigid' properties [ref OntoClean] , i.e. properties which cannot be rendered false of a thing without it ceasing to exist or to lose its identity, such as being in a certain basic ontological category, e.g. being human. In fact, we might define a rigid property as one which, if it applies to any temporal view of anything, must apply to the thing directly (and hence to all other temporal view): (forall (r)(iff
(forall (x)(if (exists ((t isTimeInterval))(r (t x)))(r x) ))
Note, this must be restricted to temporal viewing, since there could be someone who thinks that "Superman" refers to a vegetable (http://www.saturdaymarket.com/kiwi1.htm).
@@ Quantifiers very broad, use of local restrictions and guards: need to get recursions right: contexts and holdings; importing of standardized packages; publishing useful packages.
No truth-function: limitations.
Coding alternatives with triggers (Jerry); coding restrictions as bullets, eg with Ab., eg of deontic actions/events for business rules.
Handling sorts. Sortal organization vocabulary.
Handling arities, other structural constraints. Structural vocabulary? Needs some ideas on handling orthogonal contexts/namespaces.
Richard's examples, Cyc versions of OWL primitives. @@
IKL reserved and built-in vocabulary listing, and useful axioms.