Re: KIF: Re: SUO: RE: SUMO axiomatization
Bill and Chris,
Ok, we give! You guys have made a convincing and concrete case. We
almost had an out until we found one case where we used &%partition with
six arguments (we only had allowed up to five arguments in our axioms
defining &%subrelation), and since it's a subclass of
&%exhaustiveDecomposition, your axiom applies. Thanks for being so
patient, precise and concrete in explaining this.
Now, the question is what to do, and how soon. There's a cascade of
changes that flow from this. Updating the browser is a "simple matter of
programming" but we have to find resources to do it. We'd appreciate any
help you can provide in reformulating the SUMO axioms (I know Chris did
this once so maybe it just needs updating). Let's say that by the second
week in January we'll have a concrete plan for how we'll adopt row variables.
Adam & Ian
At 02:27 PM 12/20/2001 -0600, Bill Andersen wrote:
>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
Adam Pease
Teknowledge
(650) 424-0500 x571