ontolog-forum
[Top] [All Lists]

Re: [ontolog-forum] CLIF as a sorted logic?

To: ontolog-forum@xxxxxxxxxxxxxxxx
From: "John F. Sowa" <sowa@xxxxxxxxxxx>
Date: Thu, 05 Aug 2010 08:12:18 -0400
Message-id: <4C5AAAA2.70300@xxxxxxxxxxx>
Leo, Chris, and Jawit,    (01)

I agree with Chris's comments.    (02)

LO> Is this the same as guarded quantification?    (03)

The short answer, as Chris said, is that the term 'guarded' is
usually used for somewhat different purposes.    (04)

A more accurate term is 'restricted quantification', since the
domain of the quantifier is restricted to the subset for which
some monadic relation is true.    (05)

Another term 'weak typing', since the restricting relation
specifies the type of entity, but it doesn't cause a syntactic
error if the type restriction is violated.    (06)

I often use is the following example:    (07)

    (exists (x Elephant) (= x 23))    (08)

This says that some elephant is equal to 23.    (09)

In a strongly typed language, this statement would be rejected
by the parser because it violates a type constraint.  In CL,
it is syntactically correct, but false.    (010)

The negation of the above sentence would also be rejected,
but it happens to be true:    (011)

    (not (exists (x Elephant) (= x 23)))    (012)

If you map a strongly typed language like Z to CL with restricted
quantifiers, the typing information is preserved, and the sentences
can be mapped back to Z while preserving the typing.    (013)

But the definition of strong typing varies from one language to
another.  Some strongly typed languages allow some expressions
that others would consider false.  In CL, all the type violations
are syntactically correct, but false.    (014)

JFS>>  As in KIF, the expansion for an existential quantifier has 'and'
>>     instead of 'if'.  The quantified sentence
>>
>>        (exists ((N1 T1) …) B )
>>
>>     is defined as the quantified sentence
>>
>>        (exists (N1) T ( (exists (…) (and (T1 N1) B) )
>
JK> I am not clear where the "T" in the expansion above comes from, and 
what it means.    (015)

I'm sorry.  I was trying to simplify the entries in table A.2 page 31
of the standard.  At the head of that table, it says that T[E} is
the translation of the expression E.  To avoid getting into all the
metalevel explanation, I simplified the sentence, but I forgot to
delete the T.  Just ignore that T or check the full standard.    (016)

John    (017)

_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/  
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/  
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/ 
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx    (018)

<Prev in Thread] Current Thread [Next in Thread>