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

[Jawit Kien <jawit.kien@xxxxxxxxx>]

On Mon, Aug 2, 2010 at 5:11 PM, John F. Sowa <sowa@xxxxxxxxxxx> wrote:

Adam,

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.

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.

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

Following is an excerpt from Section 6.3:

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

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.

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.

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 '=>'.

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

   (forall ((N1 T1) …) B )

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

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

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

John

I am not clear where the "T" in the expansion above comes from, and what it means.

I think that 

(forall (N1) (if (T1 N1) B) )

means
 
It is true that there are some things in the domain (of discourse ?) 

if you bind the variable "N1" to each of these things in turn,

and you have a predicate T1 that when given each of these things
as an argument will produce either the value of true or false,

then for only those values of N1 where the predicate T1 is "true",
then the _expression_ B (presumably which may use the variable N1)
is also true.

for those values of N1 where the predicate T1 is "false", the
_expression_ B may be true or may be false.

But what role does the "T" play in this "meaning" ?

Similarly, I could explain what I think (forall (N1) (and (T1 N1) B)) means,
but I don't know what a variable "T" might mean for it as well.

JK

_________________________________________________________________
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    (01)