Tara and Pat, (01)
I agree with Pat that you don't need a 'that' operator for reasoning
about time. But I agree with Tara that you need 'that' for many
other purposes. (02)
For the first point, I recommend the following book, which shows how
a sorted FOL (with time as a sort) can be used to represent anything
in temporal logic or dynamic logic: (03)
Gergely, Tamás, & László Úry (1991) First-Order Programming
Theories, Berlin: Springer. (04)
They show that you can't reduce temporal logic to dynamic logic or
vice-versa. But you can translate either one to a version of FOL
that quantifies over time. A sorted logic is desirable, but not
required. (05)
TA
> (forall C P
> (if
> (cl:comment 'C employs P'
> (employs C P) )
> (exists T
> (cl:comment 'It holds during some time interval T that C employs P'
> (during (that (employs C P)) T )
> ) ) ) (06)
To express this sentence without IKL, you could use a 2-argument
and a 3-argument version of 'employs': (07)
(forall (C P)
(if (employs C P)
(exists ((T Interval)) (forall ((t Instant))
(if (isin t T) (employs C P t)) )))) (08)
Comment: If C employs P, there is an implicit interval T,
and for all instants t in T, C employs P at t. (09)
But a more general option would be an entity of type Employ,
which may have any number of qualifiers attached to it.
For required qualifiers, you could state appropriate axioms: (010)
(forall ((x Employ)) (exists ((T Interval)) (forall ((t Instant))
(if (isin t T) (at_Time x t)) ))) (011)
Comment: For any instance x of Employ, there is an implicit
interval T, and for all instants t in T, x occurs at time t. (012)
With this representation, an assertion that C employs P
could be represented with "case relations" as (013)
(exists ((x Employ)) (and (Agent x C) (Theme x P)) (014)
With the above axiom, this would imply that there exists such
an interval T. The English verb 'occurs' in the comment suggests
a more general representation: Define Employ as a subtype of
Occurrent that persists for some interval. (015)
You could say that the entity of type Employ is a reification.
But I would rather say that it's just an entity of type Employ. (016)
Re Tara's examples about using 'that' to represent possibility,
prohibition, knowledge, etc.: (017)
PH
> all they do is put the entire burden of representing their meanings
> on the relation names... and implicitly make a claim that the relevant
> concepts ... are indeed properly representable as relations between
> propositions and something else. (018)
Something like the IKL 'that', McCarthy's 'ist', or the methods
of situation semantics for relating 'infons' to situations is
an important first step. But you need a full-blown theory, not
just a few axioms. That's still a major research area. (019)
PH
> BTW, did I ever send you my ideas on how to reduce IKL to CL by
> eliminating "that" constructions recursively? I would be interested
> in your reactions. (020)
That report is important. Could you put it on your web site? (021)
John (022)
_________________________________________________________________
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 (023)
|