Ontologies and Rules 253
the given RIF document, within any imported (RDF) document, or within
any document for which entailment is to be checked.
The first-order logic axiomatization of RDF sem antics now simply needs to
translate all required axiomatic triples, which is always a finite set. Moreover,
we require one additional axiom:
∀x.∀y.∀z.
triple(x, y, z) → triple(y, rdf:type, rdf:Property)
.
This correspond s to the derivation rule rdf1 in Section 3.3.2. This axiom
completes our first-order translation of RDF semantics, so that we can now
translate RDF documents triple-by-triple as in the case of simple semantics.
This also allows us again to interpret RDF data that is imported into RIF un-
der this semantics. The URI used in the import declaration ...