Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

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


On 12/20/01 14:06, "Adam Pease" <apease@ks.teknowledge.com> wrote:

> Chris,
>  Ok, maybe I've got it wrong - can you provide an example of a definition
> that is useful in the context of SUMO, and which is possible with row
> variables, but not without?

I can, but it won't surprise you:

  (*) (=> (subrelation ?P ?Q)
          (=> (?P @x)
              (?Q @x)))

According to the semantics of row variables, this axiom "does the right
thing" for relations of any finite arity.  No finite listing of rules of the
form:

 (=> (subrelation ?P ?Q)
     (=> (?P ?v0 ... ?vn)
         (?Q ?v0 ... ?vn)))

Is equivalent to (*), since the semantics of row variables rely are those of
infinitary FOL.

 .bill