Re: SUO: NTH
Chris, Pat et al,
----- Original Message -----
From: "Chris Menzel" <cmenzel@philebus.tamu.edu>
To: "pat hayes" <phayes@ai.uwf.edu>
Cc: "Ian Niles" <iniles@teknowledge.com>;
<standard-upper-ontology@majordomo.ieee.org>
Sent: Friday, February 09, 2001 3:27 PM
Subject: Re: SUO: NTH
<snip>
----- Original Message -----
From: "pat hayes" <phayes@ai.uwf.edu>
To: <standard-upper-ontology@majordomo.ieee.org>
Sent: Saturday, February 10, 2001 2:38 PM
Subject: Re: SUO: NTH
<snip>
> >Correct. The language in question, again, is not syntactically
> >sorted (better, I think, "typed").
>
> Yes, I understand. However, I suspect that many people were thinking
> of this kind of construction to actually be something like an
> assignment of a syntactic sort, as it is in CYCL (where, I believe,
> this usage originates from.) Robert Kent was understanding it that
> way, for example. My point was only to make it clear that this would
> be a mistake, since it in fact doesn't do that.
What I really want is a semantic type restriction. However, if I can type
check it syntactically, all the better. I have constructed an ontology for
Category Theory, and it seems that over half my KIF expressions are these
type restrictions. OK, let's cut to the chase. Here is an example of what I
want to do (I am very naughty and am using the future SUO-KIF capability to
put predicate and function terms in predicate and function positions ;^).
The goal is to define the "source" or "domain" of a morphism in a category.
Here I am defining 'source' to be a unary KIF function
1. (KIF$UnaryFunction source)
that maps a category '?c' to a unary KIF function '(source ?c)'.
2. (forall (?c ?s)
(=> (= (source ?c) ?s)
(and (Category ?c) (KIF$UnaryFunction ?s))))
Here 'Category' is a previously defined KIF class (I am using 'Class' as a
synonym for 'UnaryRelation').
The KIF function '(source ?c)' should only be applied to morphisms of the
category '?c' and should only return objects of the category '?c'.
3. (forall (?c ?m ?o)
(=> (= ((source ?c) ?m) ?o)
(and ((morphism ?c) ?m) ((object ?c) ?o))))
Here '(morphism ?c)' and '(object ?c)' are a previously defined KIF classes.
I have attempted to use the recommended expression of the 'nth-domain' macro
here. Is this correct for the future SUO-KIF? Or should I be using the
'nth-domain' predicate in both 2 and 3. Or should I use the intended
'SortOf' predicate?
I have even more complicated type constraints.
Robert E. Kent
rekent@ontologos.org