Re: KIF: Re: SUO: RE: SUMO axiomatization
On Fri, Dec 21, 2001 at 01:35:00PM -0600, David Whitten wrote:
> 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
In what sense is this more flexible? I'm probably misreading your message
or Chris's or both, but I understood Chris's statement as including the
possibility that a row var be a single term for a relation expression.
> >
> >
> > 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
> >
>
--
- - - - * * * * * - - - - * * * * * - - - - * * * * * - - - -
Pierluigi Miraglia Cycorp, Inc.
Ontological Engineer 3721 Executive Center Dr.
(512) 514-2988 Austin, TX 78731