The point PatH raises is interesting - I haven't seen that raised before.
In mulling it over, I have a concern similar to that raised by Bill
For my own purposes I have found it convenient to use a general "The"
function, which can take several patterns, the most common being ternary.
One such pattern:
(The ?ROLE of ?INDIVIDUAL)
. . . can be used to reify (The Mother of John) or (The Parent of John) or
(The President of IBM) and return an individual or a more restricted ROLE
(if the ROLE can only take one value at any given time, then the ROLE could
be interpreted as an individual, If a single time point was specified or
If we then use it as PatH suggests, we should get an assertion of the form: (03)
(isTheFatherOf (The Father of ?Person) ?Person)) (04)
At first, this looks like saying (in English paraphrase)
"The father of ?P is the father of ?P"
. . . which appears to be redundant unless, as Bill mentions, the
"isTheFatherOf" relation is actually inverse-functional, with a min and max
cardinality of 1 for argument 1 (at one time point, for traditional
families). Then the "existential" part of the assertion would in fact be
present, but as the cardinality constraint on the isTheFatherOf relation.
In that case the assertion would not be a redundancy, since the
isThefatherOf relation would add information not present in the "The"
function, which can serve for relations that are not unique. In fact, I was
thiking of (but haven't done anything about) having the system automatically
generate a relation of the form "isThefatherOf" when confronted with an
instance of the "The" relation of the form (The Father of ?P), and that
would in effect create the assertion above, on the fly. The determiner of
whether that can be done legally would have to be contained in the
definition of the ROLE that is the first argument. Perhaps the effect of an
'AE assertion' would then be included in the meaning of the ROLE entity; if
it can be used in a "The" function as above, it would necessarily imply the
existence of the filler of the role, but wouldn't show up as an 'AE
assertion' and wouldn't bugger up the implementation of the logic until it
is actually needed with the appearance of the function. (05)
Not clear to me at this point what happens if the relation is not unique.
I also use functions that return 'Groups' of individuals, and a 'Group' in
this case is defined so that a 'Group' with one member is identical to that
member (somewhat reminiscent of a mereological sum). Perhaps one can find a
way to use such assertions so that existence is guaranteed at least for a
Group of one or more individuals. (06)
This looks like an interesting line of thought to pursue seriously. Is
there already a discussion of the pros and cons, nuances and potential
pitfalls out there somewhere? (07)
> -----Original Message-----
> From: ontolog-forum-bounces@xxxxxxxxxxxxxxxx [mailto:ontolog-forum-
> bounces@xxxxxxxxxxxxxxxx] On Behalf Of Bill Andersen
> Sent: Monday, December 17, 2007 10:29 PM
> To: [ontolog-forum]
> Subject: Re: [ontolog-forum] brainwaves (WAS: to concept or not to
> concept, is this a question?)
> Hi Pat..
> On Dec 17, 2007, at 22:03 , Pat Hayes wrote:
> > All of which suggests to me that any KR system
> > that has to resort to Skolemization is not
> > providing the proper engineering support for good
> > ontology construction.
> > Comments?
> I like the principle on its face, but what about this example AE
> (forall ((x person)) (exists (y) (and (has x y) (not (part y
> True when every person has something that isn't part of the Empire
> State Building. The function introduced in the form you suggest would
> look pretty contrived -- or at least not so natural as 'fatherOf'. It
> seems to me the seemingly "natural" cases arise when we're not talking
> about mere existence claims but rather about unique existence claims,
> but that's just a guess.
> Bill Andersen (andersen@xxxxxxxxxxxxxxxxx)
> Ontology Works, Inc. (www.ontologyworks.com)
> 3600 O'Donnell Street, Suite 600
> Baltimore, MD 21224
> Office: 410-675-1201
> Cell: 443-858-6444
> Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
> Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-
> Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
> Shared Files: http://ontolog.cim3.net/file/
> Community Wiki: http://ontolog.cim3.net/wiki/
> To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (011)