[SCL] Some questions for SCL and RDF

[Tanel Tammet]

Hi,

Thanks for the first comments on notes/questions about SCL syntax for RDF.

I'd ask about a point of  view from Pat and the whole SCL group concerning
the preferred way to translate SCL combined with RDF (in
whatever way the concrete syntax will look like).

Pat wrote as a part of answer to my previous question about the encoding of
predicates as used in the semantics of RDF/RDFS/OWL:

> Well, it is not clear that the use of these involves 'indirection'. 
> They are after all first-class RDF and RDFS and OWL relations in their 
> own right, and under the very same 'direct' translation they also map 
> into CL relations. Whether or not to view this 'auxiliary' vocabulary 
> as first-class seems to be a matter of taste. My own view is that it 
> is semantically more transparent to do so, in particular to express 
> rdf:type (the relationship between an entity and a predicate (/class) 
> which is true of it) as itself a binary relation:
>
> rdf:type(?x,?) iff ?y(?x)
>
> which is perfectly fine SCL. One of the great merits of SCL over 
> traditional FOL syntax is that it allows one to write things like this 
> without subterfuge.

Pat also brought an example for the subclass axiom in RDF:

subClass(?x ?y) iff  forall ?z (?x(?z) implies ?y(?z) )

Just to make myself clear I tract the first (rdf:type) formula in FOL as:

app_3(rdf:type,?x,?y) iff app_2(?y,?x)
and the second as
app_3(subClass,?x,?y) iff  forall ?z (app_2(?x,?z) implies app_2(?y,?z) )

where "app" is a predicate used as almost (or really) a single predicate 
(for example, we would then
say not "father(John,Mike)" but "app_3(father,John,Mike)" and perhaps
also "app_3(equal,2,plus(1,1))".

We could of course use a different name for "app", but the idea remains 
the same.

Sure we could translate the concrete syntax for SCL-for-RDF using the 
"app" predicate,
(or an alternative name for "app"), which would match the RDF way of
defining semantics and would thus  fit nicely into the mainstream 
RDF/RDFS/OWL way
of doing things.

Or we could take an alternative approach (which I used in the examples
sent to the list recently) where we assume that RDF/RDFS/OWL are translated
without "app" (or an alternative name).

IMHO both work but as I understand the matters, we must choose one
or another. Please tell me which of the two you would like to be used?
I'll attempt to continue with SCL-for-RDF on the lines chosen by the
SCL group instead of pushing my own view (especially since I do not have
very strong arguments for either choices).

Why I chose the non-"app" way of  writing the examples in the
mail sent previously: because if we use "app" it seems that we would
need to use "app" also for the FOL semantics of ALL CONCRETE
SYNTAXES of SCL: otherwise different SCL concrete syntaxes
would have a different semantics, which is not very nice, although
we could probably live with that too.

Another, smaller issue:

Pat asked:

 > What worries me more is  how to give an adequate FOL or CL 
translation for the cardinality restrictions in OWL.
 > These map naturally into numerical quantifiers.
 >
 > Does anyone want us to allow numerical quantifiers in SCL syntax ???

Geoff, the author/maintainer of the TPTP collection of FOL problems (the 
main
corpus for testing and comparing  FOL provers) told me that he would really
like to have the cardinality restrictions in qantifiers.  He has not 
used these
in TPTP so far, but plans to do it for some of the new examples submitted,
which do have the cardinality restrictions. He also suggested a specific 
"mainstream"
conversion algorithm of these to ordinary FOL.

Regards,
            Tanel Tammet