[Top] [All Lists]

Re: [ontolog-forum] Reducing IKL to CL

To: tara_athan@xxxxxxxxxx
Cc: "[ontolog-forum]" <ontolog-forum@xxxxxxxxxxxxxxxx>, Fabian Neuhaus <fneuhaus@xxxxxx>
From: Pat Hayes <phayes@xxxxxxx>
Date: Sun, 22 Jun 2014 22:32:07 -0500
Message-id: <796C0CB7-607E-491F-85EA-523C4796B86F@xxxxxxx>
Tara,    (01)

It occurs to me that the mapping from IKL to CL can be simplified. The current 
algorithm takes a term (that S) to the CL term (R N1 ... Nn) where the Ni are 
all the names free in S, which might be quite a lot of parameters when S is a 
large text. However, these parameters are really only needed for the case when 
one of those names is bound by a quantifier outside the (that S) term, so we 
can restrict to those cases.     (02)

Suppose a text T contains a name N. Then say that N is *skewered* in the term 
(that S) when:
1. (that S) occurs in T
2. N occurs free in S
3. That occurrence of N is bound in T.    (03)

Then (that S) can be mapped into (R N1 ... Nn) where the Ni are all the 
*skewered* names in (that S); and if there are no such names, then R can be 
simply a new constant name rather than a zero-ary function term, ie (that S) 
maps simply to R rather than (R) in this case.     (04)

This cuts down on the number of parameters (and parentheses) that one needs, in 
many cases to zero. For example the simple liar:    (05)

(= p (that (not (p))))    (06)

now becomes    (07)

D:  (iff (R)(not (p)))    ,  T:  (= p R)    (08)

rather than    (09)

D:  (forall (p)(iff ((R p))(not (p))))  , T:  (= p (R p))    (010)

Pat    (011)

IHMC                                     (850)434 8903 home
40 South Alcaniz St.            (850)202 4416   office
Pensacola                            (850)202 4440   fax
FL 32502                              (850)291 0667   mobile (preferred)
phayes@xxxxxxx       http://www.ihmc.us/users/phayes    (012)

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

<Prev in Thread] Current Thread [Next in Thread>
  • Re: [ontolog-forum] Reducing IKL to CL, Pat Hayes <=