KIF: Re: SUO: RE: SUMO axiomatization

[Bill Andersen]

On 12/27/01 15:43, "Pat Hayes" <phayes at ai.uwf.edu> wrote:

>> On 12/20/01 20:04, "Christopher A. Welty" <weltyc at cs.vassar.edu> wrote:
>> 
>>> 
>>>  Agreement is great and all, and I liked the row variables idea, but
>>>  is there a theorem prover anyway that can handle them?
>> 
>> Well, I'm writing one.
> 
> Please keep me (and Chris Menzel) posted.

Pat, et al..

The system I'm working on makes the assumption that the row variables occur
in the tail position in literals.  I take it you were working on a formal
characterization of this restricted SKIF language, right?

Anyway, it will be a while til it's ready for prime time.  It is nowhere
near as sophisticated as, say, SNARK, but it's designed to handle large
axiom collections like the SUMO.  I can give you a quick rundown on what
features are present if you're interested.

 .bill

PS - Happy New Year!