[Top] [All Lists]

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

To: Adam Pease <apease@xxxxxxxxxxxxxxxxxxxxxx>
Cc: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Mon, 2 Aug 2010 21:19:44 +0200
Message-id: <A3C87E11-CD23-4843-9332-39B65DCE5123@xxxxxxxx>
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)

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