W3C home > Mailing lists > Public > public-rdf-comments@w3.org > June 2013

Are Skolem IRIs uninterpreted?

From: Gregg Reynolds <dev@mobileink.com>
Date: Mon, 17 Jun 2013 07:23:30 -0500
Message-ID: <CAO40Mi=Wmc=XaZxa0v66X98wxbRK44g2XcKOwX3yZ3oOqK=yuA@mail.gmail.com>
To: public-rdf-comments <public-rdf-comments@w3.org>
Hi,

Is it correct to say that there is an implicit requirement that Skolem
IRIs be treated as uninterpreted?  RDF11-MT
(https://dvcs.w3.org/hg/rdf/raw-file/default/rdf-mt/index.html#skolemization-1)
just says that skolemization coins fresh IRIs.

The reason I ask is that the technical definitions of e.g. Skolem
Normal Form ([1]) and Skolem function ([2]) suggest that they should
be interpreted.  But then RDF11-MT states:

"G does not entail sk(G) (since sk(G) contains IRIs not in G.)" (where
sk(G) is the skolemization of graph G).

If I've understood skolemization (the logical concept, not just
generation of unique IRIs) then G should entail sk(G) since each
Skolem IRI in sk(G) picks out a witness that makes its triples true,
which would only be the case where G is satisfied.  But since G does
not entail sk(G), I conclude that Skolem IRIs in RDF are to be treated
as uninterpreted.  In other words "skolemization" in RDF does not
refer to the logic concepts associated with skolem function, skolem
normal form, etc.

Is that correct?

Thanks,

Gregg Reynolds
[1] "Mathematical Logic", Ebbinghaus, Flum, Thomas; page 132
[2] "The Language of First Order Logic", Barwise & Etchemendy, page 269
Received on Monday, 17 June 2013 12:23:57 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 20:29:57 UTC