From 2a3b5153955208dd4a9393fbaff57b3858efe271 Mon Sep 17 00:00:00 2001
From: Federico Igne <git@federicoigne.com>
Date: Mon, 4 Oct 2021 18:51:19 +0100
Subject: Add substitution rules in equality axiomatisation

---
 .../scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala    | 31 ++++++++++++++++++++--
 1 file changed, 29 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
index 1ff466b..5ae0227 100644
--- a/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
+++ b/src/main/scala/uk/ac/ox/cs/rsacomb/RSAOntology.scala
@@ -407,13 +407,14 @@ class RSAOntology(
     * behaviour is incompatible with other needed features like
     * negation-as-failure and aggregates.
     *
-    * @todo to complete the equality axiomatization we need to introduce
-    * substitution rules to explicate a complete "equality" semantics.
+    * @todo naïve substitution rules might not be very efficient. We
+    * should look into other ways of implementing this.
     */
   private val equalityAxioms: List[Rule] = {
     val varX = Variable.create("X")
     val varY = Variable.create("Y")
     val varZ = Variable.create("Z")
+    val varW = Variable.create("W")
     val graph = TupleTableName.create(RSAOntology.CanonGraph.getIRI)
     // Equality properties
     val properties = List(
@@ -434,6 +435,32 @@ class RSAOntology(
         TupleTableAtom.create(graph, varY, RSA.CONGRUENT, varZ)
       )
     )
+    /* Equality substitution rules */
+    val substitutions =
+      Rule.create(
+        TupleTableAtom.create(graph, varY, IRI.RDF_TYPE, varZ),
+        TupleTableAtom.create(graph, varX, RSA.CONGRUENT, varY),
+        TupleTableAtom.create(graph, varX, IRI.RDF_TYPE, varZ)
+      ) :: objroles.flatMap(r => {
+        val name = r match {
+          case x: OWLObjectProperty => x.getIRI.getIRIString
+          case x: OWLObjectInverseOf =>
+            x.getInverse.getNamedProperty.getIRI.getIRIString :: Inverse
+        }
+        List(
+          Rule.create(
+            TupleTableAtom.create(graph, varZ, name, varY),
+            TupleTableAtom.create(graph, varX, RSA.CONGRUENT, varZ),
+            TupleTableAtom.create(graph, varX, name, varY)
+          ),
+          Rule.create(
+            TupleTableAtom.create(graph, varY, name, varZ),
+            TupleTableAtom.create(graph, varX, RSA.CONGRUENT, varZ),
+            TupleTableAtom.create(graph, varY, name, varX)
+          )
+        )
+      })
+    properties ++ substitutions
   }
 
   /** Canonical model of the ontology */
-- 
cgit v1.2.3