aboutsummaryrefslogtreecommitdiff
path: root/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala')
-rw-r--r--src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala82
1 files changed, 5 insertions, 77 deletions
diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
index 96a953f..3777c6b 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/CanonicalModel.scala
@@ -12,17 +12,12 @@ import org.semanticweb.owlapi.model.{
12} 12}
13 13
14import tech.oxfordsemantic.jrdfox.logic.datalog.{ 14import tech.oxfordsemantic.jrdfox.logic.datalog.{
15 Rule,
16 BodyFormula, 15 BodyFormula,
17 TupleTableAtom, 16 Negation,
18 Negation 17 Rule,
19} 18 TupleTableAtom
20import tech.oxfordsemantic.jrdfox.logic.expression.{
21 Term,
22 Variable,
23 // Resource,
24 IRI
25} 19}
20import tech.oxfordsemantic.jrdfox.logic.expression.{IRI, Term, Variable}
26 21
27import implicits.JavaCollections._ 22import implicits.JavaCollections._
28 23
@@ -78,73 +73,6 @@ class CanonicalModel(val ontology: RSAOntology) {
78 }) 73 })
79 } 74 }
80 75
81 /** Top axiomatization
82 *
83 * Corresponding to the following rules:
84 *
85 * ```
86 * [?a, rdf:type, owl:Thing] :- [?a, rdf:type, ?b] .
87 * [?a, rdf:type, owl:Thing], [?b, rdf:type, owl:Thing] :- [?a, ?r, ?b], FILTER(?r != rdf:type).
88 * ```
89 *
90 * @note this is a naïve implementation of top axiomatization and
91 * might change in the future. The ideal solution would be for RDFox
92 * to take care of this, but at the time of writing this is not
93 * compatible with the way we are using the tool.
94 */
95 private val topAxioms: List[Rule] = {
96 val varA = Variable.create("A")
97 val varR = Variable.create("R")
98 val varB = Variable.create("B")
99 List(
100 Rule.create(
101 RSA.Thing(varA),
102 TupleTableAtom.rdf(varA, IRI.RDF_TYPE, varB)
103 ),
104 Rule.create(
105 List(RSA.Thing(varA), RSA.Thing(varB)),
106 List(
107 TupleTableAtom.rdf(varA, varR, varB),
108 FilterAtom.create(FunctionCall.notEqual(varR, IRI.RDF_TYPE))
109 )
110 )
111 )
112 }
113
114 /** Equality axiomatization
115 *
116 * Introduce reflexivity, simmetry and transitivity rules for a naïve
117 * equality axiomatization.
118 *
119 * @note that we are using a custom `congruent` predicate to indicate
120 * equality. This is to avoid interfering with the standard
121 * `owl:sameAs`.
122 *
123 * @note RDFox is able to handle equality in a "smart" way, but this
124 * behaviour is incompatible with other needed features like
125 * negation-as-failure and aggregates.
126 *
127 * @todo to complete the equality axiomatization we need to introduce
128 * substitution rules to explicate a complete "equality" semantics.
129 */
130 private val equalityAxioms: List[Rule] = {
131 val varX = Variable.create("X")
132 val varY = Variable.create("Y")
133 val varZ = Variable.create("Z")
134 List(
135 // Reflexivity
136 Rule.create(RSA.Congruent(varX, varX), RSA.Thing(varX)),
137 // Simmetry
138 Rule.create(RSA.Congruent(varY, varX), RSA.Congruent(varX, varY)),
139 // Transitivity
140 Rule.create(
141 RSA.Congruent(varX, varZ),
142 RSA.Congruent(varX, varY),
143 RSA.Congruent(varY, varZ)
144 )
145 )
146 }
147
148 val (facts, rules): (List[TupleTableAtom], List[Rule]) = { 76 val (facts, rules): (List[TupleTableAtom], List[Rule]) = {
149 // Compute rules from ontology axioms 77 // Compute rules from ontology axioms
150 val (facts, rules) = { 78 val (facts, rules) = {
@@ -156,7 +84,7 @@ class CanonicalModel(val ontology: RSAOntology) {
156 } 84 }
157 ( 85 (
158 facts.flatten, 86 facts.flatten,
159 rolesAdditionalRules ::: topAxioms ::: equalityAxioms ::: rules.flatten 87 rolesAdditionalRules ::: rules.flatten
160 ) 88 )
161 } 89 }
162 90