On 8/6/2010 10:01 AM, Rick Murphy wrote:
> Would you be able to provide a pointer to additional information
> on the use of optional types in CGIF? (01)
Conceptual graphs have always had a type hierarchy. At the top
of the hierarchy, the universal type is true of everything.
If you omit the type label, the default is to assume the universal
type, which is equivalent to an untyped quantification. (02)
The ISO standard is silent about whether the types are organized
in a hierarchy. A sorted logic with disjoint types would correspond
to a one-level hierarchy with each type immediately below the universal
and no use of the untyped option. (03)
For a brief overview of conceptual graphs, CGIF, and CLIF, see (04)
http://www.jfsowa.com/cg/cg_hbook.pdf (05)
> I don't see optional types in 24707 Appendix A. (06)
The only mention is in Table A.2 on p. 31 of ISO 24707. There really
should be more examples and explanation. I included some examples
at the beginning of Annex B, which show the informal display form
of CGs, the translation to CGIF, and the translation to CLIF. The
cg_book.pdf article includes more examples and explanations for
both CGIF and CLIF. (07)
Following is an excerpt from an earlier email note. (08)
John
______________________________________________________________________ (09)
The use of type restrictions on quantifiers was introduced into the
draft ANSI standard for KIF: http://logic.stanford.edu/kif/dpans.html (010)
Following is an excerpt from Section 6.3: (011)
> 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)) (012)
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. (013)
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. (014)
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 '=>'. (015)
The typed syntax for CLIF is defined in table A2, page 31 of ISO 24707,
which states that a quantified sentence of the form (016)
(forall ((N1 T1) …) B ) (017)
is defined by expanding the type constraint T1 to a monadic relation
T1 and an if statement: (018)
(forall (N1) (forall (…) (if (T1 N1) B)) (019)
As in KIF, the expansion for an existential quantifier has 'and'
instead of 'if'. The quantified sentence (020)
(exists ((N1 T1) …) B) (021)
is defined as the quantified sentence (022)
(exists (N1) (exists (…) (and (T1 N1) B))) (023)
_________________________________________________________________
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 (024)
|