Re: KIF: Re: SUO: RE: SUMO axiomatization
A very minor point, and I hesitate to disagree with Chris who may have
a better memory of the details than I, but I seem to recall that Pat's
restrictions were not that the row variable should occur only as the
last term, but that it appear as a single term for a given relation
and always in the same position, which I understand is a shade more flexible
that chris mentions, but not very much.
- David
>
>
> On Fri, Dec 21, 2001 at 11:01:39AM -0600, Chris Menzel wrote:
> >
> > > Agreement is great and all, and I liked the row variables idea, but
> > > is there a theorem prover anyway that can handle them?
> >
> > Not in general, but Pat has defined certain restrictions on the occurrence
> > of row variables (e.g., a row variable should occur only as the last term
> > in an atomic formula) that yields a subclass of KIF sentences containing
> > row variables that can still be used effectively in theorem proving.
> >
> > -chris
>
> Cyc handles row variables (called 'sequence variables' in cycl), with
> the restriction you mention.
>
> --
> - - - - * * * * * - - - - * * * * * - - - - * * * * * - - - -
> Pierluigi Miraglia Cycorp, Inc.
> Ontological Engineer 3721 Executive Center Dr.
> (512) 514-2988 Austin, TX 78731
>