[Top] [All Lists]

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

To: ontolog-forum@xxxxxxxxxxxxxxxx
From: "John F. Sowa" <sowa@xxxxxxxxxxx>
Date: Mon, 02 Aug 2010 18:11:57 -0400
Message-id: <4C5742AD.8020402@xxxxxxxxxxx>
Adam,    (01)

I agree with Chris's comments about the differences between a sorted
logic and the kind of weak typing that is used in both CLIF and CGIF.    (02)

I'd just like to point out where the type restrictions on quantifiers
are mentioned in both the draft ANSI specification for KIF and in
the ISO standard 24707 for CLIF.    (03)

The use of type restrictions on quantifiers was introduced into the
draft ANSI standard for KIF:  http://logic.stanford.edu/kif/dpans.html    (04)

Following is an excerpt from Section 6.3:    (05)

> Quantified sentences with complicated variable specifications can
> be converted into simple quantified sentences by replacing each
> complicated variable specification by the variable in the specification
> and adding an appropriate condition into the body of the sentence.
> Note that, in the case of a set restriction, it may be necessary to
> rename variables to avoid conflicts. The following pairs of sentences
> show the transformation from complex quantified sentences to simple
> quantified sentences.
>     (forall (... (?x r) ...) s)
>     (forall (...  ?x    ...) (=> (r ?x) s))
>     (exists (... (?x r) ...) s)
>     (exists (...  ?x    ...) (and (r ?x) s))    (06)

As these examples show, the monadic relation r is used to restrict
the range of the quantified variable ?x.  This is a kind of
"weak" typing, since a type mismatch does not make a statement
ungrammatical.    (07)

In a strongly typed language such as Z, a type mismatch would cause
a syntax error.  But in KIF, CLIF, or CGIF, a type mismatch just
causes the offending sentence to be false.    (08)

But the weak typing introduced into KIF (which was equivalent
to the typing in CGs) was carried over to CLIF with a similar
definition.  The main differences are the absence of the prefix "?"
on variables and the keyword 'if' instead of the arrow '=>'.    (09)

The typed syntax for CLIF is defined in table A2, page 31 of ISO 24707,
which states that a quantified sentence of the form    (010)

    (forall ((N1 T1) ) B )    (011)

is defined by expanding the type constraint T1 to a monadic relation
T1 and an if statement:    (012)

    (forall (N1) T ( (forall () (if (T1 N1) B) )    (013)

As in KIF, the expansion for an existential quantifier has 'and'
instead of 'if'.  The quantified sentence    (014)

    (exists ((N1 T1) ) B )    (015)

is defined as the quantified sentence    (016)

    (exists (N1) T ( (exists () (and (T1 N1) B) )    (017)

John    (018)

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    (019)

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