On Aug 2, 2010, at 8:54 PM, Adam Pease wrote:
> Hi Folks,
> A quick CLIF question for the experts here - The CG appendix of the CL
> standard appears to show typed quantification, although I don't see that
> defined in the CLIF appendix. Is there a definition for a sort syntax
> that I missed? (01)
Hi Adam, (02)
Quick a priori reply without checking the details of the standard: A sorted
logic is quite a different animal than the typed quantification of CGIF. Typed
quantification can be defined straightaway in any CL dialect; e.g., in CLIF: (03)
(exists (x:F) A) =df (exists (x) (and (F x) A)
(forall (x:F) A) =df (forall (x) (if (F x) A) (04)
Sorted logic, in the sense I'm familiar with, a.k.a. multi-sorted/many-sorted
logic, involves the introduction of multiple, pairwise disjoint classes of
variables and, hence, separate quantifiers for each class. Multi-sorted logic
is easily reducible to single-sorted logic, but the syntax and semantics are
rather more complex (not to say conceptually difficult) and not part of the CL
standard. (05)
-chris (06)
_________________________________________________________________
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 (07)
|