- From: Gregg Reynolds <dev@mobileink.com>
- Date: Mon, 17 Jun 2013 07:23:30 -0500
- 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