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