From: Adam Pease ([email protected])
Date: 04/21/03
Dan,
The SUO-KIF spec is now a bit out of date with respect to SUMO
unfortunately. It lacks higher-order statements and row variables, for
example. For higher-order statements, it needs the modification that
term ::= variable | word | string | funterm | number
becomes
term ::= variable | word | string | funterm | number | sentence
In practice, for inference, we quote many higher-order expressions, as
you've indicated in your last formula below. Since this is simply a
syntactic sugaring though, and just an issue for implementation, we leave
the expressions unquoted in SUMO and run a preprocessor to add quoting in
our implementation.
Adam
At 10:33 PM 4/21/2003 -0500, Dan Connolly wrote:
>On Mon, 2003-04-21 at 17:12, Adam Pease wrote:
> > Dan,
> > The modules are in KIF in our public CVS repository at
> > <http://ontology.teknowledge.com/cgi-bin/cvsweb.cgi/SUO/Merge.txt>. Each
> > module is separated from others in the file by the tags ";; BEGIN FILE" and
> > ";; END FILE". The DAML version of the latest SUMO is at
> > <http://reliant.teknowledge.com/DAML/SUMO.daml>, although it lacks the
> > module delimiters.
>
>Ah... ok, good.
>
>Hmm... I hope this isn't too far off topic, but
>in modelling places and times it seems to come up
>quite a bit... I see this in the ontology:
>
>----------
>(instance holdsDuring BinaryPredicate)
>(instance holdsDuring AsymmetricRelation)
>(domain holdsDuring 1 TimePosition)
>(domain holdsDuring 2 Formula)
>(documentation holdsDuring "(&%holdsDuring ?TIME ?FORMULA) means that the
>proposition denoted by ?FORMULA is true in the time frame ?TIME. Note
>that this implies that ?FORMULA is true at every &%TimePoint which is a
>&%temporalPart of ?TIME.")
>
>(=>
> (and
> (holdsDuring ?TIME ?SITUATION1)
> (entails ?SITUATION1 ?SITUATION2))
> (holdsDuring ?TIME ?SITUATION2))
>
>(=>
> (holdsDuring ?TIME (not ?SITUATION))
> (not (holdsDuring ?TIME ?SITUATION)))
>----------
>
>But I can't make sense of "proposition denoted by ?FORMULA".
>
>And I can't parse formulas like this...
>
>--------
>(=>
> (believes ?AGENT ?FORMULA)
> (exists (?TIME)
> (holdsDuring ?TIME (considers ?AGENT ?FORMULA))))
>--------
>
>That Merge.txt claims to be written in a language,
>SUO-KIF, specified in http://suo.ieee.org/suo-kif.html
>but from that spec it looks like (considers ?AGENT ?FORMULA)
>parses as a functional term, not a term denoting
>a proposition.
>
>I ask partly to understand SUMO but also because
>the N3 notation I'm working on with TimBL et. al.
>(cf http://www.w3.org/2000/10/swap/Primer) has a very
>similar syntactic gizmo and I'm hard pressed to
>figure out how to specify it, formally.
>
>The only way I've been able to make sense of
>it is via quasiquoting, ala...
>
>--------
>(=>
> (believes ?AGENT ?FORMULA)
> (exists (?TIME)
> (holdsDuring ?TIME ^(considers ,?AGENT ,?FORMULA))))
>--------
>
>--
>Dan Connolly, W3C http://www.w3.org/People/Connolly/
This archive was generated by hypermail 2.1.4 : 04/22/03 EST