[SCL] translating RDF, RDFS and OWL into SCL

[Bill Andersen]

On Nov 8, 2004, at 4:57 PM, Pat Hayes wrote:

>> On Nov 8, 2004, at 4:07 PM, Pat Hayes wrote:
>>
>>>> Hi, Pat...
>>>>
>>>> Didn't know you were working on this.  And, since we just built a 
>>>> translator to take OWL into our KFL (an SCL concrete syntax) I'm 
>>>> anxious to give it a read.  By when do you want comments?
>>>
>>> Im debugging the axioms right now, will update and signal you later 
>>> today. Can your engine handle the SCL tail recursions (=~= KIF 
>>> sequence variables, or RDF lists) ?
>>
>> Yup, at least I think so.  We do use sequence variables in the 
>> current engine but it's not up to the SCL spec you wrote.  We did it 
>> 4 years ago.
>
> Then its probably up to it. SCL is a step backwards from KIF, since we 
> don't allow explicit quantifier binding to the seqvars: in effect, 
> they are always universal at the top syntactic level.

That's what we have.  No existential quant over seqvars.  I have to 
check what the syntax rules are we have.  All of the axioms that use 
seqvars are part of our top-level ontology and don't get revisited very 
often so I've forgotten how that works.

> BTW, I now think that this entire detour into seqvars was kind of 
> beside the point, in spite of their elegance. Lists are just more 
> convenient, truth be told. In particular, since they are real 
> entities, not just syntactic tricks, you can quantify over them 
> directly; and the obvious list axioms mean that a list of n items 
> exists just when the items do; so in effect you get sequence-variable 
> quantification for free whether you want it or not. Ah well, one is 
> always learning,

 From a purely mathematical standpoint you're right.  But when I write 
something like:

     (forall (F G) (=> (subsumes G F) (forall (...x) (=> (F ...x) (G 
...x)))))

I really do mean to say something only about the substitutions for F 
and G and ...x.  The fact that the length of the substitutions for ...x 
can vary depending on the choice of F and G doesn't alter the fact that 
I want to say something *ontologically* about relations and their 
relata, not about lists.

If anything, I wouldn't mind if the ...x were just a shorthand for 
lists underneath the surface syntax or in the semantics, but for 
clarity's sake, I like ...x better.