Warning:
This wiki has been archived and is now read-only.
DLP As Horn Rules
From OWL
- 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.
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) |
Functional-Syntax S | Tranformation Tp(S,x,y) |
---|---|
objectPropertyURI | objectPropertyURI(x,y) |
InverseObjectProperty(p) | Tp(p,y,x) |
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 |
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) |
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
( H ∧ H' ) ← B | H ← B
H' ← B |
( H ← H' ) ← B | H ← H' ∧ B |
H ← B ∨ B' | H ← B
H ← B' |