Warning:
This wiki has been archived and is now read-only.

DLP As Horn Rules

From OWL
Jump to: navigation, search

[Hide Review Comments]

Document title:
OWL 2 Web Ontology Language
DLP Mapping to Horn Rules (Second Edition)

This is a draft mapping from DLP fragment functional syntax to Horn rules. The functional syntax specification of DLP normatively defines the domain of the transformation.

Concept Transformation
Functional-Syntax S Tranformation Tc(S,x)
owlClassURI owlClassURI(x)
ObjectOneOf(i1 ... in) x = i1 ∨ ... ∨ x = in
ObjectIntersectionOf(c1 ... cn) Tc(c1,x) ∧ ... ∧ Tc(cn,x)
ObjectUnionOf(c1 ... cn) Tc(c1,x) ∨ ... ∨ Tc(cn,x)
ObjectSomeValuesFrom(p c) Tp(p,x,y) ∧ Tc(c,y)
ObjectHasValue(p i) Tc(p,x,i)
ObjectAllValuesFrom(p c) Tc(c,x) ← Tp(p,x,y)
ObjectMaxCardinality(0 p) False ← Tp(p,x,y)
ObjectMaxCardinality(0 p c) False ← Tp(p,x,y) ∧ Tc(c,y)
ObjectMaxCardinality(1 p) y=z ← Tp(p,x,y) ∧ Tp(p,x,z)
ObjectMaxCardinality(1 p c) y=z ← Tp(p,x,y) ∧ Tp(p,x,z) ∧ Tc(c,y) ∧ Tc(c,z)


Object Property Transformation
Functional-Syntax S Tranformation Tp(S,x,y)
objectPropertyURI objectPropertyURI(x,y)
InverseObjectProperty(p) Tp(p,y,x)


Class Axiom Transformation
Functional-Syntax S Tranformation T(S)
SubClassOf(c1 c2) Tc(c2,x) ← Tc(c1,x)
EquivalentClasses(c1 ... cn) Tc(ci,x) ← Tc(cj,x)

Tc(cj,x) ← Tc(ci,x) 1 ≤ i,j ≤ n, i ≠ j

DisjointClasses(c1 ... cn) False ← Tc(ci,x) ∧ Tc(cj,x) 1 ≤ i,j ≤ n, i ≠ j


Property Axiom Transformation
Functional-Syntax S Tranformation T(S)
SubObjectPropertyOf(p1 p2) Tp(p2,x,y) ← Tp(p1,x,y)
EquivalentObjectProperties(p1 ... pn) Tp(pi,x,y) ← Tp(pj,x,y)

Tp(pj,x,y) ← Tp(pi,x,y) 1 ≤ i,j ≤ n, i ≠ j

ObjectPropertyDomain(p c) Th(c,x) ← Tp(p,x,y)
ObjectPropertyRange(p c) Th(c,y) ← Tp(p,x,y)
TransitiveObjectProperty(p) Tp(p,x,z) ← Tp(p,x,y) ∧ Tp(p,y,z)
FunctionalObjectProperty(p) y = z ← Tp(p,x,y) ∧ Tp(p,x,z)
InverseFunctionalObjectProperty(p) y = z ← Tp(p,y,x) ∧ Tp(p,z,x)
SymmetricObjectProperty(p) Tp(p,y,x) ← Tp(p,x,y)


Fact Transformation
Functional-Syntax S Tranformation T(S)
SameIndividualAs(i1 ... jn) ii = ij 1 ≤ i,j ≤ n, i ≠ j
DifferentIndividuals(i1 ... in) ii ≠ ij 1 ≤ i,j ≤ n, i ≠ j
ClassAssertion(i c) Tc(c,i)
ObjectPropertyAssertion(p i j) Tp(i,j)
NegativeObjectPropertyAssertion(p i j) False ← Tp(i,j)


The rewriting transforms below can be used to simplify the results of transformation to the form H ← B1 ∧ ... ∧ Bn

Rule Simplification
( H ∧ H' ) ← B H ← B

H' ← B

( H ← H' ) ← B H ← H' ∧ B
H ← B ∨ B' H ← B

H ← B'

Retrieved from "https://www.w3.org/2007/OWL/wiki/index.php?title=DLP_As_Horn_Rules&oldid=3252"