Re: KIF: Re: SUO: RE: SUMO axiomatization

[Pierluigi Miraglia <miraglia@cyc.com>]

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