feat: metamodel translator

46 files changed, 1933 insertions, 120 deletions

diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java
index c560162e..40993235 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/PartialClauseRewriter.java
@@ -7,8 +7,10 @@ package tools.refinery.store.reasoning.internal;
 
 import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.dnf.DnfBuilder;
 import tools.refinery.store.query.dnf.DnfClause;
 import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.AbstractCountLiteral;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.Literal;
 import tools.refinery.store.query.term.Aggregator;
@@ -17,6 +19,7 @@ import tools.refinery.store.query.term.Term;
 import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.query.term.int_.IntTerms;
 import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms;
+import tools.refinery.store.reasoning.ReasoningAdapter;
 import tools.refinery.store.reasoning.literal.*;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.reasoning.translator.multiobject.MultiObjectTranslator;
@@ -58,6 +61,14 @@ class PartialClauseRewriter {
                         rewriteCountUpperBound(countUpperBoundLiteral);
                         return;
                 }
+                if (callLiteral instanceof CountCandidateLowerBoundLiteral countCandidateLowerBoundLiteral) {
+                        rewriteCountCandidateLowerBound(countCandidateLowerBoundLiteral);
+                        return;
+                }
+                if (callLiteral instanceof CountCandidateUpperBoundLiteral countCandidateUpperBoundLiteral) {
+                        rewriteCountCandidateUpperBound(countCandidateUpperBoundLiteral);
+                        return;
+                }
                 var target = callLiteral.getTarget();
                 if (target instanceof Dnf dnf) {
                         rewriteRecursively(callLiteral, dnf);
@@ -78,48 +89,26 @@ class PartialClauseRewriter {
         }
 
         private void rewriteCountLowerBound(CountLowerBoundLiteral literal) {
-                rewriteCount(literal, "lower", Modality.MUST, MultiObjectTranslator.LOWER_CARDINALITY_VIEW, 1, IntTerms::mul,
-                                IntTerms.INT_SUM);
+                rewritePartialCount(literal, "lower", Modality.MUST, MultiObjectTranslator.LOWER_CARDINALITY_VIEW, 1,
+                                IntTerms::mul, IntTerms.INT_SUM);
         }
 
         private void rewriteCountUpperBound(CountUpperBoundLiteral literal) {
-                rewriteCount(literal, "upper", Modality.MAY, MultiObjectTranslator.UPPER_CARDINALITY_VIEW,
+                rewritePartialCount(literal, "upper", Modality.MAY, MultiObjectTranslator.UPPER_CARDINALITY_VIEW,
                                 UpperCardinalities.ONE, UpperCardinalityTerms::mul, UpperCardinalityTerms.UPPER_CARDINALITY_SUM);
         }
 
-        private <T> void rewriteCount(ConcreteCountLiteral<T> literal, String name, Modality modality, Constraint view,
-                                                                  T one, BinaryOperator<Term<T>> mul, Aggregator<T, T> sum) {
+        private <T> void rewritePartialCount(AbstractCountLiteral<T> literal, String name, Modality modality,
+                                                                                 Constraint view, T one, BinaryOperator<Term<T>> mul, Aggregator<T, T> sum) {
                 var type = literal.getResultType();
-                var target = literal.getTarget();
-                var concreteness = literal.getConcreteness();
-                int arity = target.arity();
-                var parameters = target.getParameters();
-                var literalArguments = literal.getArguments();
-                var privateVariables = literal.getPrivateVariables(positiveVariables);
-
-                var builder = Dnf.builder("%s#%s#%s".formatted(target.name(), concreteness, name));
-                var rewrittenArguments = new ArrayList<Variable>(parameters.size());
-                var variablesToCount = new ArrayList<Variable>();
-                var helperArguments = new ArrayList<Variable>();
-                var literalToRewrittenArgumentMap = new HashMap<Variable, Variable>();
-                for (int i = 0; i < arity; i++) {
-                        var literalArgument = literalArguments.get(i);
-                        var parameter = parameters.get(i);
-                        var rewrittenArgument = literalToRewrittenArgumentMap.computeIfAbsent(literalArgument, key -> {
-                                helperArguments.add(key);
-                                var newArgument = builder.parameter(parameter);
-                                if (privateVariables.contains(key)) {
-                                        variablesToCount.add(newArgument);
-                                }
-                                return newArgument;
-                        });
-                        rewrittenArguments.add(rewrittenArgument);
-                }
+                var countResult = computeCountVariables(literal, Concreteness.PARTIAL, name);
+                var builder = countResult.builder();
                 var outputVariable = builder.parameter(type);
+                var variablesToCount = countResult.variablesToCount();
 
                 var literals = new ArrayList<Literal>();
-                literals.add(new ModalConstraint(modality, literal.getConcreteness(), target)
-                                .call(CallPolarity.POSITIVE, rewrittenArguments));
+                literals.add(new ModalConstraint(modality, Concreteness.PARTIAL, literal.getTarget())
+                                .call(CallPolarity.POSITIVE, countResult.rewrittenArguments()));
                 switch (variablesToCount.size()) {
                 case 0 -> literals.add(outputVariable.assign(new ConstantTerm<>(type, one)));
                 case 1 -> literals.add(view.call(variablesToCount.get(0),
@@ -141,11 +130,65 @@ class PartialClauseRewriter {
 
                 var helperQuery = builder.build();
                 var aggregationVariable = Variable.of(type);
+                var helperArguments = countResult.helperArguments();
                 helperArguments.add(aggregationVariable);
                 workList.addFirst(literal.getResultVariable().assign(helperQuery.aggregateBy(aggregationVariable, sum,
                                 helperArguments)));
         }
 
+        private void rewriteCountCandidateLowerBound(CountCandidateLowerBoundLiteral literal) {
+                rewriteCandidateCount(literal, "lower", Modality.MAY);
+        }
+
+        private void rewriteCountCandidateUpperBound(CountCandidateUpperBoundLiteral literal) {
+                rewriteCandidateCount(literal, "upper", Modality.MUST);
+        }
+
+        private void rewriteCandidateCount(AbstractCountLiteral<Integer> literal, String name, Modality modality) {
+                var countResult = computeCountVariables(literal, Concreteness.CANDIDATE, name);
+                var builder = countResult.builder();
+
+                var literals = new ArrayList<Literal>();
+                literals.add(new ModalConstraint(modality, Concreteness.CANDIDATE, literal.getTarget())
+                                .call(CallPolarity.POSITIVE, countResult.rewrittenArguments()));
+                for (var variable : countResult.variablesToCount()) {
+                        literals.add(new ModalConstraint(modality, Concreteness.CANDIDATE, ReasoningAdapter.EXISTS_SYMBOL)
+                                        .call(variable));
+                }
+                builder.clause(literals);
+
+                var helperQuery = builder.build();
+                workList.addFirst(literal.getResultVariable().assign(helperQuery.count(countResult.helperArguments())));
+        }
+
+        private CountResult computeCountVariables(AbstractCountLiteral<?> literal, Concreteness concreteness,
+                                                                                          String name) {
+                var target = literal.getTarget();
+                int arity = target.arity();
+                var parameters = target.getParameters();
+                var literalArguments = literal.getArguments();
+                var privateVariables = literal.getPrivateVariables(positiveVariables);
+                var builder = Dnf.builder("%s#%s#%s".formatted(target.name(), concreteness, name));
+                var rewrittenArguments = new ArrayList<Variable>(parameters.size());
+                var variablesToCount = new ArrayList<Variable>();
+                var helperArguments = new ArrayList<Variable>();
+                var literalToRewrittenArgumentMap = new HashMap<Variable, Variable>();
+                for (int i = 0; i < arity; i++) {
+                        var literalArgument = literalArguments.get(i);
+                        var parameter = parameters.get(i);
+                        var rewrittenArgument = literalToRewrittenArgumentMap.computeIfAbsent(literalArgument, key -> {
+                                helperArguments.add(key);
+                                var newArgument = builder.parameter(parameter);
+                                if (privateVariables.contains(key)) {
+                                        variablesToCount.add(newArgument);
+                                }
+                                return newArgument;
+                        });
+                        rewrittenArguments.add(rewrittenArgument);
+                }
+                return new CountResult(builder, rewrittenArguments, helperArguments, variablesToCount);
+        }
+
         private void markAsDone(Literal literal) {
                 completedLiterals.add(literal);
                 positiveVariables.addAll(literal.getOutputVariables());
@@ -173,4 +216,8 @@ class PartialClauseRewriter {
                         workList.addFirst(literals.get(i));
                 }
         }
+
+        private record CountResult(DnfBuilder builder, List<Variable> rewrittenArguments, List<Variable> helperArguments,
+                                                           List<Variable> variablesToCount) {
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java
index f878b674..889f595f 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java
@@ -41,7 +41,7 @@ public class DnfLifter {
                 var modality = modalDnf.modality();
                 var concreteness = modalDnf.concreteness();
                 var dnf = modalDnf.dnf();
-                var builder = Dnf.builder("%s#%s#%s".formatted(dnf.name(), modality, concreteness));
+                var builder = Dnf.builder(decorateName(dnf.name(), modality, concreteness));
                 builder.symbolicParameters(dnf.getSymbolicParameters());
                 builder.functionalDependencies(dnf.getFunctionalDependencies());
                 for (var clause : dnf.getClauses()) {
@@ -65,4 +65,8 @@ public class DnfLifter {
                         return "%s %s %s".formatted(modality, concreteness, dnf.name());
                 }
         }
+
+        public static String decorateName(String name, Modality modality, Concreteness concreteness) {
+                return "%s#%s#%s".formatted(name, modality, concreteness);
+        }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java
deleted file mode 100644
index 91b30964..00000000
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ConcreteCountLiteral.java
+++ /dev/null
@@ -1,47 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.reasoning.literal;
-
-import tools.refinery.store.query.Constraint;
-import tools.refinery.store.query.equality.LiteralEqualityHelper;
-import tools.refinery.store.query.equality.LiteralHashCodeHelper;
-import tools.refinery.store.query.literal.AbstractCountLiteral;
-import tools.refinery.store.query.literal.Literal;
-import tools.refinery.store.query.term.DataVariable;
-import tools.refinery.store.query.term.Variable;
-
-import java.util.List;
-import java.util.Objects;
-
-// {@link Object#equals(Object)} is implemented by {@link AbstractLiteral}.
-@SuppressWarnings("squid:S2160")
-public abstract class ConcreteCountLiteral<T> extends AbstractCountLiteral<T> {
-        private final Concreteness concreteness;
-
-        protected ConcreteCountLiteral(Class<T> resultType, DataVariable<T> resultVariable, Concreteness concreteness,
-                                                                   Constraint target, List<Variable> arguments) {
-                super(resultType, resultVariable, target, arguments);
-                this.concreteness = concreteness;
-        }
-
-        public Concreteness getConcreteness() {
-                return concreteness;
-        }
-
-        @Override
-        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
-                if (!super.equalsWithSubstitution(helper, other)) {
-                        return false;
-                }
-                var otherCountLiteral = (ConcreteCountLiteral<?>) other;
-                return Objects.equals(concreteness, otherCountLiteral.concreteness);
-        }
-
-        @Override
-        public int hashCodeWithSubstitution(LiteralHashCodeHelper helper) {
-                return Objects.hash(super.hashCodeWithSubstitution(helper), concreteness);
-        }
-}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateLowerBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateLowerBoundLiteral.java
new file mode 100644
index 00000000..91dd2b72
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateLowerBoundLiteral.java
@@ -0,0 +1,49 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.literal;
+
+import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.AbstractCountLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.List;
+
+public class CountCandidateLowerBoundLiteral extends AbstractCountLiteral<Integer> {
+        public CountCandidateLowerBoundLiteral(DataVariable<Integer> resultVariable, Constraint target,
+                                                                                   List<Variable> arguments) {
+                super(Integer.class, resultVariable, target, arguments);
+        }
+
+        @Override
+        protected Integer zero() {
+                return 0;
+        }
+
+        @Override
+        protected Integer one() {
+                return 1;
+        }
+
+        @Override
+        protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) {
+                return new CountCandidateLowerBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(),
+                                substitutedArguments);
+        }
+
+        @Override
+        public AbstractCallLiteral withArguments(Constraint newTarget, List<Variable> newArguments) {
+                return new CountCandidateLowerBoundLiteral(getResultVariable(), newTarget, newArguments);
+        }
+
+        @Override
+        protected String operatorName() {
+                return "@LowerBound(\"candidate\") count";
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateUpperBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateUpperBoundLiteral.java
new file mode 100644
index 00000000..94c9399d
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountCandidateUpperBoundLiteral.java
@@ -0,0 +1,49 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.literal;
+
+import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.AbstractCountLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.List;
+
+public class CountCandidateUpperBoundLiteral extends AbstractCountLiteral<Integer> {
+        public CountCandidateUpperBoundLiteral(DataVariable<Integer> resultVariable, Constraint target,
+                                                                                   List<Variable> arguments) {
+                super(Integer.class, resultVariable, target, arguments);
+        }
+
+        @Override
+        protected Integer zero() {
+                return 0;
+        }
+
+        @Override
+        protected Integer one() {
+                return 1;
+        }
+
+        @Override
+        protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) {
+                return new CountCandidateUpperBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(),
+                                substitutedArguments);
+        }
+
+        @Override
+        public AbstractCallLiteral withArguments(Constraint newTarget, List<Variable> newArguments) {
+                return new CountCandidateUpperBoundLiteral(getResultVariable(), newTarget, newArguments);
+        }
+
+        @Override
+        protected String operatorName() {
+                return "@UpperBound(\"candidate\") count";
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java
index 261088fc..b75b0cab 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountLowerBoundLiteral.java
@@ -7,6 +7,7 @@ package tools.refinery.store.reasoning.literal;
 
 import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.AbstractCountLiteral;
 import tools.refinery.store.query.literal.Literal;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.DataVariable;
@@ -14,10 +15,10 @@ import tools.refinery.store.query.term.Variable;
 
 import java.util.List;
 
-public class CountLowerBoundLiteral extends ConcreteCountLiteral<Integer> {
-        public CountLowerBoundLiteral(DataVariable<Integer> resultVariable, Concreteness concreteness, Constraint target,
+public class CountLowerBoundLiteral extends AbstractCountLiteral<Integer> {
+        public CountLowerBoundLiteral(DataVariable<Integer> resultVariable, Constraint target,
                                                                   List<Variable> arguments) {
-                super(Integer.class, resultVariable, concreteness, target, arguments);
+                super(Integer.class, resultVariable, target, arguments);
         }
 
         @Override
@@ -32,17 +33,17 @@ public class CountLowerBoundLiteral extends ConcreteCountLiteral<Integer> {
 
         @Override
         protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) {
-                return new CountLowerBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getConcreteness(),
-                                getTarget(), substitutedArguments);
+                return new CountLowerBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(),
+                                substitutedArguments);
         }
 
         @Override
-        protected AbstractCallLiteral internalWithTarget(Constraint newTarget) {
-                return new CountLowerBoundLiteral(getResultVariable(), getConcreteness(), newTarget, getArguments());
+        public AbstractCallLiteral withArguments(Constraint newTarget, List<Variable> newArguments) {
+                return new CountLowerBoundLiteral(getResultVariable(), newTarget, newArguments);
         }
 
         @Override
         protected String operatorName() {
-                return "@LowerBound(\"%s\") count".formatted(getConcreteness());
+                return "@LowerBound(\"partial\") count";
         }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java
index 960ded69..03842143 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/CountUpperBoundLiteral.java
@@ -7,6 +7,7 @@ package tools.refinery.store.reasoning.literal;
 
 import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.AbstractCountLiteral;
 import tools.refinery.store.query.literal.Literal;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.DataVariable;
@@ -16,10 +17,10 @@ import tools.refinery.store.representation.cardinality.UpperCardinality;
 
 import java.util.List;
 
-public class CountUpperBoundLiteral extends ConcreteCountLiteral<UpperCardinality> {
-        public CountUpperBoundLiteral(DataVariable<UpperCardinality> resultVariable, Concreteness concreteness,
-                                                                  Constraint target, List<Variable> arguments) {
-                super(UpperCardinality.class, resultVariable, concreteness, target, arguments);
+public class CountUpperBoundLiteral extends AbstractCountLiteral<UpperCardinality> {
+        public CountUpperBoundLiteral(DataVariable<UpperCardinality> resultVariable, Constraint target,
+                                                                  List<Variable> arguments) {
+                super(UpperCardinality.class, resultVariable, target, arguments);
         }
 
         @Override
@@ -34,17 +35,17 @@ public class CountUpperBoundLiteral extends ConcreteCountLiteral<UpperCardinalit
 
         @Override
         protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) {
-                return new CountUpperBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getConcreteness(),
-                                getTarget(), substitutedArguments);
+                return new CountUpperBoundLiteral(substitution.getTypeSafeSubstitute(getResultVariable()), getTarget(),
+                                substitutedArguments);
         }
 
         @Override
-        protected AbstractCallLiteral internalWithTarget(Constraint newTarget) {
-                return new CountUpperBoundLiteral(getResultVariable(), getConcreteness(), newTarget, getArguments());
+        public AbstractCallLiteral withArguments(Constraint newTarget, List<Variable> newArguments) {
+                return new CountUpperBoundLiteral(getResultVariable(), newTarget, newArguments);
         }
 
         @Override
         protected String operatorName() {
-                return "@UpperBound(\"%s\") count".formatted(getConcreteness());
+                return "@UpperBound(\"partial\") count";
         }
 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java
new file mode 100644
index 00000000..b6bccb01
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/refinement/RefinementBasedInitializer.java
@@ -0,0 +1,34 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.refinement;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.reasoning.seed.ModelSeed;
+
+public class RefinementBasedInitializer<A, C> implements PartialModelInitializer {
+        private final PartialSymbol<A, C> partialSymbol;
+
+        public RefinementBasedInitializer(PartialSymbol<A, C> partialSymbol) {
+                this.partialSymbol = partialSymbol;
+        }
+
+        @Override
+        public void initialize(Model model, ModelSeed modelSeed) {
+                var refiner = model.getAdapter(ReasoningAdapter.class).getRefiner(partialSymbol);
+                var defaultValue = partialSymbol.abstractDomain().unknown();
+                var cursor = modelSeed.getCursor(partialSymbol, defaultValue);
+                while (cursor.move()) {
+                        var key = cursor.getKey();
+                        var value = cursor.getValue();
+                        if (!refiner.merge(key, value)) {
+                                throw new IllegalArgumentException("Failed to merge value %s for key %s into %s"
+                                                .formatted(value, key, partialSymbol));
+                        }
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java
index aee74eb3..6f9492a3 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/PartialRelationTranslator.java
@@ -9,6 +9,7 @@ import tools.refinery.store.model.ModelStoreBuilder;
 import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.ModelQueryBuilder;
 import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.dnf.QueryBuilder;
 import tools.refinery.store.query.dnf.RelationalQuery;
 import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.query.view.MayView;
@@ -18,16 +19,20 @@ import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
 import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter;
 import tools.refinery.store.reasoning.interpretation.QueryBasedRelationInterpretationFactory;
 import tools.refinery.store.reasoning.interpretation.QueryBasedRelationRewriter;
+import tools.refinery.store.reasoning.lifting.DnfLifter;
 import tools.refinery.store.reasoning.literal.Concreteness;
 import tools.refinery.store.reasoning.literal.Modality;
 import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner;
 import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
+import tools.refinery.store.reasoning.refinement.PartialModelInitializer;
 import tools.refinery.store.reasoning.refinement.StorageRefiner;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.representation.AnySymbol;
 import tools.refinery.store.representation.Symbol;
 import tools.refinery.store.representation.TruthValue;
 
+import java.util.function.BiConsumer;
+
 @SuppressWarnings("UnusedReturnValue")
 public final class PartialRelationTranslator extends PartialSymbolTranslator<TruthValue, Boolean> {
         private final PartialRelation partialRelation;
@@ -84,6 +89,12 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru
                 return this;
         }
 
+        @Override
+        public PartialRelationTranslator initializer(PartialModelInitializer initializer) {
+                super.initializer(initializer);
+                return this;
+        }
+
         public PartialRelationTranslator query(RelationalQuery query) {
                 checkNotConfigured();
                 if (this.query != null) {
@@ -102,6 +113,12 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru
                 return this;
         }
 
+        public PartialRelationTranslator mayNever() {
+                var never = createQuery(partialRelation.name() + "#never", (builder, parameters) -> {});
+                may(never);
+                return this;
+        }
+
         public PartialRelationTranslator must(RelationalQuery must) {
                 checkNotConfigured();
                 if (this.must != null) {
@@ -163,20 +180,24 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru
                 }
         }
 
-        private RelationalQuery createQuery(Constraint constraint) {
+        private RelationalQuery createQuery(String name, BiConsumer<QueryBuilder, Variable[]> callback) {
                 int arity = partialRelation.arity();
-                var queryBuilder = Query.builder(partialRelation.name());
+                var queryBuilder = Query.builder(name);
                 var parameters = new Variable[arity];
                 for (int i = 0; i < arity; i++) {
                         parameters[i] = queryBuilder.parameter("p" + 1);
                 }
-                queryBuilder.clause(constraint.call(parameters));
+                callback.accept(queryBuilder, parameters);
                 return queryBuilder.build();
         }
 
+        private RelationalQuery createQuery(String name, Constraint constraint) {
+                return createQuery(name, (builder, parameters) -> builder.clause(constraint.call(parameters)));
+        }
+
         private void createFallbackQueryFromRewriter() {
                 if (rewriter != null && query == null) {
-                        query = createQuery(partialRelation);
+                        query = createQuery(partialRelation.name(), partialRelation);
                 }
         }
 
@@ -189,10 +210,12 @@ public final class PartialRelationTranslator extends PartialSymbolTranslator<Tru
                 var typedStorageSymbol = (Symbol<TruthValue>) storageSymbol;
                 var defaultValue = typedStorageSymbol.defaultValue();
                 if (may == null && !defaultValue.may()) {
-                        may = createQuery(new MayView(typedStorageSymbol));
+                        may = createQuery(DnfLifter.decorateName(partialRelation.name(), Modality.MAY, Concreteness.PARTIAL),
+                                        new MayView(typedStorageSymbol));
                 }
                 if (must == null && !defaultValue.must()) {
-                        must = createQuery(new MustView(typedStorageSymbol));
+                        must = createQuery(DnfLifter.decorateName(partialRelation.name(), Modality.MUST, Concreteness.PARTIAL),
+                                        new MustView(typedStorageSymbol));
                 }
         }
 
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java
new file mode 100644
index 00000000..9d1b8cf4
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentHierarchyTranslator.java
@@ -0,0 +1,221 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.containment;
+
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.dnf.RelationalQuery;
+import tools.refinery.store.query.literal.Connectivity;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.literal.RepresentativeElectionLiteral;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.view.AnySymbolView;
+import tools.refinery.store.reasoning.lifting.DnfLifter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+import tools.refinery.store.reasoning.translator.RoundingMode;
+import tools.refinery.store.reasoning.translator.multiplicity.ConstrainedMultiplicity;
+import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.cardinality.CardinalityIntervals;
+import tools.refinery.store.representation.cardinality.FiniteUpperCardinality;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Map;
+
+import static tools.refinery.store.query.literal.Literals.check;
+import static tools.refinery.store.query.literal.Literals.not;
+import static tools.refinery.store.query.term.int_.IntTerms.constant;
+import static tools.refinery.store.query.term.int_.IntTerms.less;
+import static tools.refinery.store.reasoning.ReasoningAdapter.EXISTS_SYMBOL;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.may;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.must;
+
+public class ContainmentHierarchyTranslator implements ModelStoreConfiguration {
+        public static final PartialRelation CONTAINED_SYMBOL = new PartialRelation("contained", 1);
+        public static final PartialRelation INVALID_NUMBER_OF_CONTAINERS = new PartialRelation("invalidNumberOfContainers",
+                        1);
+        public static final PartialRelation CONTAINS_SYMBOL = new PartialRelation("contains", 2);
+
+        private final Symbol<InferredContainment> containsStorage = Symbol.of("CONTAINS", 2, InferredContainment.class,
+                        InferredContainment.UNKNOWN);
+        private final AnySymbolView forbiddenContainsView = new ForbiddenContainsView(containsStorage);
+        private final RelationalQuery containsMayNewTargetHelper;
+        private final RelationalQuery containsMayExistingHelper;
+        private final RelationalQuery weakComponents;
+        private final RelationalQuery strongComponents;
+        private final Map<PartialRelation, ContainmentInfo> containmentInfoMap;
+
+        public ContainmentHierarchyTranslator(Map<PartialRelation, ContainmentInfo> containmentInfoMap) {
+                this.containmentInfoMap = containmentInfoMap;
+
+                var name = CONTAINS_SYMBOL.name();
+
+                containsMayNewTargetHelper = Query.of(name + "#mayNewTargetHelper", (builder, child) -> builder
+                                .clause(Integer.class, existingContainers -> List.of(
+                                                may(CONTAINED_SYMBOL.call(child)),
+                                                new CountLowerBoundLiteral(existingContainers, CONTAINS_SYMBOL, List.of(Variable.of(), child)),
+                                                check(less(existingContainers, constant(1)))
+                                )));
+
+                containsMayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder
+                                .clause(Integer.class, existingContainers -> List.of(
+                                                must(CONTAINS_SYMBOL.call(parent, child)),
+                                                not(forbiddenContainsView.call(parent, child))
+                                                // Violation of monotonicity:
+                                                // Containment edges violating upper multiplicity will not be marked as {@code ERROR}, but the
+                                                // {@code invalidNumberOfContainers} error pattern will already mark the node as invalid.
+                                )));
+
+                var mustExistBothContains = Query.of(name + "#mustExistBoth", (builder, parent, child) -> builder.clause(
+                                must(CONTAINS_SYMBOL.call(parent, child)),
+                                must(EXISTS_SYMBOL.call(parent)),
+                                must(EXISTS_SYMBOL.call(child))
+                ));
+
+                weakComponents = Query.of(name + "#weakComponents", (builder, node, representative) -> builder.clause(
+                                new RepresentativeElectionLiteral(Connectivity.WEAK, mustExistBothContains.getDnf(), node,
+                                                representative)
+                ));
+
+                strongComponents = Query.of(name + "#strongComponents", (builder, node, representative) -> builder.clause(
+                                new RepresentativeElectionLiteral(Connectivity.STRONG, mustExistBothContains.getDnf(), node,
+                                                representative)
+                ));
+        }
+
+        @Override
+        public void apply(ModelStoreBuilder storeBuilder) {
+                storeBuilder.symbol(containsStorage);
+                translateContains(storeBuilder);
+                translateInvalidNumberOfContainers(storeBuilder);
+                for (var entry : containmentInfoMap.entrySet()) {
+                        var linkType = entry.getKey();
+                        var info = entry.getValue();
+                        translateContainmentLinkType(storeBuilder, linkType, info);
+                        translateInvalidMultiplicity(storeBuilder, linkType, info);
+                }
+        }
+
+        private void translateContainmentLinkType(ModelStoreBuilder storeBuilder, PartialRelation linkType,
+                                                                                          ContainmentInfo info) {
+                var name = linkType.name();
+                var sourceType = info.sourceType();
+                var targetType = info.targetType();
+                var upperCardinality = info.multiplicity().multiplicity().upperBound();
+
+                var mayNewSourceHelper = Query.of(name + "#mayNewSourceHelper", (builder, parent) -> {
+                        var literals = new ArrayList<Literal>();
+                        literals.add(may(sourceType.call(parent)));
+                        if (upperCardinality instanceof FiniteUpperCardinality finiteUpperCardinality) {
+                                var existingCount = Variable.of("existingCount", Integer.class);
+                                literals.add(new CountLowerBoundLiteral(existingCount, linkType, List.of(parent, Variable.of())));
+                                literals.add(check(less(existingCount, constant(finiteUpperCardinality.finiteUpperBound()))));
+                        }
+                        builder.clause(literals);
+                });
+
+                var mayNewTargetHelper = Query.of(name + "#mayNewTargetHelper", (builder, child) -> builder.clause(
+                                containsMayNewTargetHelper.call(child),
+                                may(targetType.call(child))
+                ));
+
+                var forbiddenLinkView = new ForbiddenContainmentLinkView(containsStorage, linkType);
+
+                var mayNewHelper = Query.of(name + "#mayNewHelper", (builder, parent, child) -> builder.clause(
+                                mayNewSourceHelper.call(parent),
+                                mayNewTargetHelper.call(child),
+                                not(must(CONTAINS_SYMBOL.call(parent, child))),
+                                not(forbiddenLinkView.call(parent, child))
+                ));
+
+                var mayExistingHelper = Query.of(name + "#mayExistingHelper", (builder, parent, child) -> builder.clause(
+                                must(linkType.call(parent, child)),
+                                containsMayExistingHelper.call(parent, child),
+                                may(sourceType.call(parent)),
+                                may(targetType.call(child)),
+                                not(forbiddenLinkView.call(parent, child))
+                                // Violation of monotonicity:
+                                // Containment edges violating upper multiplicity will not be marked as {@code ERROR}, but the
+                                // {@code invalidNumberOfContainers} error pattern will already mark the node as invalid.
+                ));
+
+                var may = Query.of(name + "#may", (builder, parent, child) -> builder
+                                .clause(
+                                                mayNewHelper.call(parent, child),
+                                                not(weakComponents.call(parent, Variable.of()))
+                                )
+                                .clause(representative -> List.of(
+                                                mayNewHelper.call(parent, child),
+                                                weakComponents.call(child, representative),
+                                                // Violation of para-consistency:
+                                                // If there is a surely existing node with at least two containers, its (transitive) containers
+                                                // will end up in the same weakly connected component, and we will spuriously mark the
+                                                // containment edge between the (transitive) containers as {@code FALSE}. However, such
+                                                // models can never be finished.
+                                                //
+                                                // Violation of monotonicity:
+                                                // if the a {@code TRUE} value is added to the representation in the previous situation,
+                                                // we'll check strongly connected components instead of weakly connected ones. Therefore, the
+                                                // view for the partial symbol will change from {@code FALSE} to {@code TRUE}. This doesn't
+                                                // affect the overall inconsistency of the partial model (due to the surely existing node
+                                                // with multiple containers).
+                                                not(weakComponents.call(child, representative))
+                                ))
+                                .clause(
+                                                mayExistingHelper.call(parent, child),
+                                                not(strongComponents.call(parent, Variable.of()))
+                                )
+                                .clause(representative -> List.of(
+                                                mayExistingHelper.call(parent, child),
+                                                strongComponents.call(parent, representative),
+                                                not(strongComponents.call(parent, representative))
+                                )));
+
+                storeBuilder.with(PartialRelationTranslator.of(linkType)
+                                .may(may)
+                                .must(Query.of(name + "#must", (builder, parent, child) -> builder.clause(
+                                                new MustContainmentLinkView(containsStorage, linkType).call(parent, child)
+                                )))
+                                .roundingMode(RoundingMode.PREFER_FALSE)
+                                .refiner(ContainmentLinkRefiner.of(linkType, containsStorage, info.sourceType(), info.targetType()))
+                                .initializer(new RefinementBasedInitializer<>(linkType)));
+        }
+
+        private void translateInvalidMultiplicity(ModelStoreBuilder storeBuilder, PartialRelation linkType,
+                                                                                          ContainmentInfo info) {
+                storeBuilder.with(new InvalidMultiplicityErrorTranslator(info.sourceType(), linkType, false,
+                                info.multiplicity()));
+        }
+
+        private void translateContains(ModelStoreBuilder storeBuilder) {
+                var name = CONTAINS_SYMBOL.name();
+                var mustName = DnfLifter.decorateName(name, Modality.MUST, Concreteness.PARTIAL);
+
+                storeBuilder.with(PartialRelationTranslator.of(CONTAINS_SYMBOL)
+                                .query(Query.of(name, (builder, parent, child) -> {
+                                        for (var linkType : containmentInfoMap.keySet()) {
+                                                builder.clause(linkType.call(parent, child));
+                                        }
+                                }))
+                                .must(Query.of(mustName, (builder, parent, child) -> builder.clause(
+                                                new MustContainsView(containsStorage).call(parent, child)
+                                )))
+                                .refiner(ContainsRefiner.of(containsStorage))
+                                .initializer(new RefinementBasedInitializer<>(CONTAINS_SYMBOL)));
+        }
+
+        private void translateInvalidNumberOfContainers(ModelStoreBuilder storeBuilder) {
+                storeBuilder.with(new InvalidMultiplicityErrorTranslator(CONTAINED_SYMBOL, CONTAINS_SYMBOL, true,
+                                ConstrainedMultiplicity.of(CardinalityIntervals.ONE, INVALID_NUMBER_OF_CONTAINERS)));
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentInfo.java
new file mode 100644
index 00000000..1087e54d
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentInfo.java
@@ -0,0 +1,23 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.containment;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
+
+public record ContainmentInfo(PartialRelation sourceType, Multiplicity multiplicity,
+                                                          PartialRelation targetType) {
+        public ContainmentInfo {
+                if (sourceType.arity() != 1) {
+                        throw new IllegalArgumentException("Expected source type %s to be of arity 1, got %d instead"
+                                        .formatted(sourceType, sourceType.arity()));
+                }
+                if (targetType.arity() != 1) {
+                        throw new IllegalArgumentException("Expected target type %s to be of arity 1, got %d instead"
+                                        .formatted(targetType, targetType.arity()));
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java
new file mode 100644
index 00000000..497ed98f
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainmentLinkRefiner.java
@@ -0,0 +1,128 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.containment;
+
+import tools.refinery.store.model.Interpretation;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner;
+import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.ArrayList;
+import java.util.Set;
+
+class ContainmentLinkRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> {
+        private final Factory factory;
+        private final Interpretation<InferredContainment> interpretation;
+        private final PartialInterpretationRefiner<TruthValue, Boolean> sourceRefiner;
+        private final PartialInterpretationRefiner<TruthValue, Boolean> targetRefiner;
+
+        public ContainmentLinkRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
+                                                                  Factory factory) {
+                super(adapter, partialSymbol);
+                this.factory = factory;
+                interpretation = adapter.getModel().getInterpretation(factory.symbol);
+                sourceRefiner = adapter.getRefiner(factory.sourceType);
+                targetRefiner = adapter.getRefiner(factory.targetType);
+        }
+
+        @Override
+        public boolean merge(Tuple key, TruthValue value) {
+                var oldValue = interpretation.get(key);
+                var newValue = mergeLink(oldValue, value);
+                if (oldValue != newValue) {
+                        interpretation.put(key, newValue);
+                }
+                if (value.must()) {
+                        return sourceRefiner.merge(Tuple.of(key.get(0)), TruthValue.TRUE) &&
+                                        targetRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE);
+                }
+                return true;
+        }
+
+        public InferredContainment mergeLink(InferredContainment oldValue, TruthValue toMerge) {
+                return switch (toMerge) {
+                        case UNKNOWN -> oldValue;
+                        case TRUE -> mustLink(oldValue);
+                        case FALSE -> forbidLink(oldValue);
+                        case ERROR -> errorLink(oldValue);
+                };
+        }
+
+        public InferredContainment mustLink(InferredContainment oldValue) {
+                var mustLinks = oldValue.mustLinks();
+                if (oldValue.contains().may() && mustLinks.isEmpty() && oldValue.forbiddenLinks().isEmpty()) {
+                        return factory.trueLink;
+                }
+                if (mustLinks.contains(factory.linkType)) {
+                        return oldValue;
+                }
+                return new InferredContainment(oldValue.contains().merge(TruthValue.TRUE),
+                                addToSet(mustLinks, factory.linkType), oldValue.forbiddenLinks());
+        }
+
+        public InferredContainment forbidLink(InferredContainment oldValue) {
+                var forbiddenLinks = oldValue.forbiddenLinks();
+                if (oldValue.contains() == TruthValue.UNKNOWN && oldValue.mustLinks().isEmpty() && forbiddenLinks.isEmpty()) {
+                        return factory.falseLinkUnknownContains;
+                }
+                if (forbiddenLinks.contains(factory.linkType)) {
+                        return oldValue;
+                }
+                return new InferredContainment(oldValue.contains(), oldValue.mustLinks(),
+                                addToSet(forbiddenLinks, factory.linkType));
+        }
+
+        public InferredContainment errorLink(InferredContainment oldValue) {
+                return new InferredContainment(TruthValue.ERROR, addToSet(oldValue.mustLinks(), factory.linkType),
+                                addToSet(oldValue.forbiddenLinks(), factory.linkType));
+        }
+
+        private static Set<PartialRelation> addToSet(Set<PartialRelation> oldSet, PartialRelation linkType) {
+                if (oldSet.isEmpty()) {
+                        return Set.of(linkType);
+                }
+                var newElements = new ArrayList<PartialRelation>(oldSet.size() + 1);
+                newElements.addAll(oldSet);
+                newElements.add(linkType);
+                return Set.copyOf(newElements);
+        }
+
+        public static PartialInterpretationRefiner.Factory<TruthValue, Boolean> of(
+                        PartialRelation linkType, Symbol<InferredContainment> symbol, PartialRelation sourceType,
+                        PartialRelation targetType) {
+                return new Factory(linkType, symbol, sourceType, targetType);
+        }
+
+        private static class Factory implements PartialInterpretationRefiner.Factory<TruthValue, Boolean> {
+                public final PartialRelation linkType;
+                public final Symbol<InferredContainment> symbol;
+                public final PartialRelation targetType;
+                public final PartialRelation sourceType;
+                public final InferredContainment trueLink;
+                public final InferredContainment falseLinkUnknownContains;
+
+                public Factory(PartialRelation linkType, Symbol<InferredContainment> symbol, PartialRelation sourceType,
+                                           PartialRelation targetType) {
+                        this.linkType = linkType;
+                        this.symbol = symbol;
+                        this.sourceType = sourceType;
+                        this.targetType = targetType;
+                        trueLink = new InferredContainment(TruthValue.TRUE, Set.of(linkType), Set.of());
+                        falseLinkUnknownContains = new InferredContainment(TruthValue.FALSE, Set.of(), Set.of(linkType));
+                }
+
+                @Override
+                public PartialInterpretationRefiner<TruthValue, Boolean> create(
+                                ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol) {
+                        return new ContainmentLinkRefiner(adapter, partialSymbol, this);
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java
new file mode 100644
index 00000000..b57ca095
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ContainsRefiner.java
@@ -0,0 +1,70 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.containment;
+
+import tools.refinery.store.model.Interpretation;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner;
+import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.Set;
+
+class ContainsRefiner extends AbstractPartialInterpretationRefiner<TruthValue, Boolean> {
+        private static final InferredContainment CONTAINS_TRUE = new InferredContainment(TruthValue.TRUE, Set.of(),
+                        Set.of());
+        private static final InferredContainment CONTAINS_FALSE = new InferredContainment(TruthValue.FALSE, Set.of(),
+                        Set.of());
+        private static final InferredContainment CONTAINS_ERROR = new InferredContainment(TruthValue.ERROR, Set.of(),
+                        Set.of());
+
+        private final PartialInterpretationRefiner<TruthValue, Boolean> containedRefiner;
+        private final Interpretation<InferredContainment> interpretation;
+
+        public ContainsRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
+                                                   Symbol<InferredContainment> symbol) {
+                super(adapter, partialSymbol);
+                containedRefiner = adapter.getRefiner(ContainmentHierarchyTranslator.CONTAINED_SYMBOL);
+                interpretation = adapter.getModel().getInterpretation(symbol);
+        }
+
+        @Override
+        public boolean merge(Tuple key, TruthValue value) {
+                var oldValue = interpretation.get(key);
+                var newValue = mergeContains(oldValue, value);
+                if (oldValue != newValue) {
+                        interpretation.put(key, newValue);
+                }
+                if (value.must()) {
+                        return containedRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE);
+                }
+                return true;
+        }
+
+        public InferredContainment mergeContains(InferredContainment oldValue, TruthValue toMerge) {
+                var oldContains = oldValue.contains();
+                var newContains = oldContains.merge(toMerge);
+                if (newContains == oldContains) {
+                        return oldValue;
+                }
+                if (oldValue.mustLinks().isEmpty() && oldValue.forbiddenLinks().isEmpty()) {
+                        return switch (toMerge) {
+                                case UNKNOWN -> oldValue;
+                                case TRUE -> oldContains.may() ? CONTAINS_TRUE : CONTAINS_ERROR;
+                                case FALSE -> oldContains.must() ? CONTAINS_ERROR : CONTAINS_FALSE;
+                                case ERROR -> CONTAINS_ERROR;
+                        };
+                }
+                return new InferredContainment(newContains, oldValue.mustLinks(), oldValue.forbiddenLinks());
+        }
+
+        public static Factory<TruthValue, Boolean> of(Symbol<InferredContainment> symbol) {
+                return (adapter, partialSymbol) -> new ContainsRefiner(adapter, partialSymbol, symbol);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainmentLinkView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainmentLinkView.java
new file mode 100644
index 00000000..cf0e2971
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainmentLinkView.java
@@ -0,0 +1,21 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.containment;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+
+class ForbiddenContainmentLinkView extends InferredContainmentLinkView {
+        public ForbiddenContainmentLinkView(Symbol<InferredContainment> symbol, PartialRelation link) {
+                super(symbol, "must", link);
+        }
+
+        @Override
+        protected boolean doFilter(Tuple key, InferredContainment value) {
+                return value.forbiddenLinks().contains(link);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainsView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainsView.java
new file mode 100644
index 00000000..efe674f1
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/ForbiddenContainsView.java
@@ -0,0 +1,21 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.containment;
+
+import tools.refinery.store.query.view.TuplePreservingView;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+
+class ForbiddenContainsView extends TuplePreservingView<InferredContainment> {
+        public ForbiddenContainsView(Symbol<InferredContainment> symbol) {
+                super(symbol, "contains#forbidden");
+        }
+
+        @Override
+        protected boolean doFilter(Tuple key, InferredContainment value) {
+                return !value.contains().may();
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java
new file mode 100644
index 00000000..90802864
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainment.java
@@ -0,0 +1,37 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.containment;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.TruthValue;
+
+import java.util.Set;
+
+record InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks,
+                                                   Set<PartialRelation> forbiddenLinks) {
+        public static final InferredContainment UNKNOWN = new InferredContainment(
+                        TruthValue.UNKNOWN, Set.of(), Set.of());
+
+        public InferredContainment(TruthValue contains, Set<PartialRelation> mustLinks,
+                                                           Set<PartialRelation> forbiddenLinks) {
+                this.contains = adjustContains(contains, mustLinks, forbiddenLinks);
+                this.mustLinks = mustLinks;
+                this.forbiddenLinks = forbiddenLinks;
+        }
+
+        private static TruthValue adjustContains(TruthValue contains, Set<PartialRelation> mustLinks,
+                                                                                         Set<PartialRelation> forbiddenLinks) {
+                var result = contains;
+                if (!mustLinks.isEmpty()) {
+                        result = result.merge(TruthValue.TRUE);
+                }
+                boolean hasErrorLink = mustLinks.stream().anyMatch(forbiddenLinks::contains);
+                if (mustLinks.size() >= 2 || hasErrorLink) {
+                        result = result.merge(TruthValue.ERROR);
+                }
+                return result;
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainmentLinkView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainmentLinkView.java
new file mode 100644
index 00000000..d187ad91
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/InferredContainmentLinkView.java
@@ -0,0 +1,35 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.containment;
+
+import tools.refinery.store.query.view.TuplePreservingView;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.Symbol;
+
+import java.util.Objects;
+
+abstract class InferredContainmentLinkView extends TuplePreservingView<InferredContainment> {
+        protected final PartialRelation link;
+
+        protected InferredContainmentLinkView(Symbol<InferredContainment> symbol, String name, PartialRelation link) {
+                super(symbol, link.name() + "#" + name);
+                this.link = link;
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                if (!super.equals(o)) return false;
+                InferredContainmentLinkView that = (InferredContainmentLinkView) o;
+                return Objects.equals(link, that.link);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), link);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainmentLinkView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainmentLinkView.java
new file mode 100644
index 00000000..474942d6
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainmentLinkView.java
@@ -0,0 +1,21 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.containment;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+
+class MustContainmentLinkView extends InferredContainmentLinkView {
+        public MustContainmentLinkView(Symbol<InferredContainment> symbol, PartialRelation link) {
+                super(symbol, "must", link);
+        }
+
+        @Override
+        protected boolean doFilter(Tuple key, InferredContainment value) {
+                return value.mustLinks().contains(link);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainsView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainsView.java
new file mode 100644
index 00000000..6bc62a59
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/containment/MustContainsView.java
@@ -0,0 +1,21 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.containment;
+
+import tools.refinery.store.query.view.TuplePreservingView;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+
+class MustContainsView extends TuplePreservingView<InferredContainment> {
+        public MustContainsView(Symbol<InferredContainment> symbol) {
+                super(symbol, "contains#must");
+        }
+
+        @Override
+        protected boolean doFilter(Tuple key, InferredContainment value) {
+                return value.contains().must();
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java
new file mode 100644
index 00000000..c4a2f2b3
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/CrossReferenceUtils.java
@@ -0,0 +1,57 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.crossreference;
+
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.dnf.RelationalQuery;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.term.NodeVariable;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.reasoning.literal.CountLowerBoundLiteral;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
+import tools.refinery.store.representation.cardinality.FiniteUpperCardinality;
+
+import java.util.ArrayList;
+import java.util.List;
+
+import static tools.refinery.store.query.literal.Literals.check;
+import static tools.refinery.store.query.term.int_.IntTerms.constant;
+import static tools.refinery.store.query.term.int_.IntTerms.less;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.may;
+
+class CrossReferenceUtils {
+        private CrossReferenceUtils() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static RelationalQuery createMayHelper(PartialRelation linkType, PartialRelation type,
+                                                                                                  Multiplicity multiplicity, boolean inverse) {
+                String name;
+                NodeVariable variable;
+                List<Variable> arguments;
+                if (inverse) {
+                        name = "Target";
+                        variable = Variable.of("target");
+                        arguments = List.of(Variable.of("source"), variable);
+                } else {
+                        name = "Source";
+                        variable = Variable.of("source");
+                        arguments = List.of(variable, Variable.of("target"));
+                }
+                var builder = Query.builder(linkType.name() + "#mayNew" + name);
+                builder.parameter(variable);
+                var literals = new ArrayList<Literal>();
+                literals.add(may(type.call(variable)));
+                if (multiplicity.multiplicity().upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) {
+                        var existingLinks = Variable.of("existingLinks", Integer.class);
+                        literals.add(new CountLowerBoundLiteral(existingLinks, linkType, arguments));
+                        literals.add(check(less(existingLinks, constant(finiteUpperCardinality.finiteUpperBound()))));
+                }
+                builder.clause(literals);
+                return builder.build();
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java
new file mode 100644
index 00000000..d8c6a5ea
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceInfo.java
@@ -0,0 +1,16 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.crossreference;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
+
+public record DirectedCrossReferenceInfo(PartialRelation sourceType, Multiplicity sourceMultiplicity,
+                                                                                 PartialRelation targetType, Multiplicity targetMultiplicity) {
+        public boolean isConstrained() {
+                return sourceMultiplicity.isConstrained() || targetMultiplicity.isConstrained();
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java
new file mode 100644
index 00000000..0700f9f7
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceRefiner.java
@@ -0,0 +1,46 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.crossreference;
+
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner;
+import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+class DirectedCrossReferenceRefiner extends ConcreteSymbolRefiner<TruthValue, Boolean> {
+        private final PartialInterpretationRefiner<TruthValue, Boolean> sourceRefiner;
+        private final PartialInterpretationRefiner<TruthValue, Boolean> targetRefiner;
+
+        public DirectedCrossReferenceRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
+                                                                                 Symbol<TruthValue> concreteSymbol, PartialRelation sourceType,
+                                                                                 PartialRelation targetType) {
+                super(adapter, partialSymbol, concreteSymbol);
+                sourceRefiner = adapter.getRefiner(sourceType);
+                targetRefiner = adapter.getRefiner(targetType);
+        }
+
+        @Override
+        public boolean merge(Tuple key, TruthValue value) {
+                if (!super.merge(key, value)) {
+                        return false;
+                }
+                if (value.must()) {
+                        return sourceRefiner.merge(Tuple.of(key.get(0)), TruthValue.TRUE) &&
+                                        targetRefiner.merge(Tuple.of(key.get(1)), TruthValue.TRUE);
+                }
+                return true;
+        }
+
+        public static Factory<TruthValue, Boolean> of(Symbol<TruthValue> concreteSymbol, PartialRelation sourceType,
+                                                                                                  PartialRelation targetType) {
+                return (adapter, partialSymbol) -> new DirectedCrossReferenceRefiner(adapter, partialSymbol, concreteSymbol,
+                                sourceType, targetType);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java
new file mode 100644
index 00000000..f978aad4
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/DirectedCrossReferenceTranslator.java
@@ -0,0 +1,82 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.crossreference;
+
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.dnf.RelationalQuery;
+import tools.refinery.store.query.view.ForbiddenView;
+import tools.refinery.store.reasoning.lifting.DnfLifter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator;
+import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+
+import static tools.refinery.store.query.literal.Literals.not;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.may;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.must;
+
+public class DirectedCrossReferenceTranslator implements ModelStoreConfiguration {
+        private final PartialRelation linkType;
+        private final DirectedCrossReferenceInfo info;
+        private final Symbol<TruthValue> symbol;
+
+        public DirectedCrossReferenceTranslator(PartialRelation linkType, DirectedCrossReferenceInfo info) {
+                this.linkType = linkType;
+                this.info = info;
+                symbol = Symbol.of(linkType.name(), 2, TruthValue.class, TruthValue.UNKNOWN);
+        }
+
+        @Override
+        public void apply(ModelStoreBuilder storeBuilder) {
+                var name = linkType.name();
+                var sourceType = info.sourceType();
+                var targetType = info.targetType();
+                var mayNewSource = createMayHelper(sourceType, info.sourceMultiplicity(), false);
+                var mayNewTarget = createMayHelper(targetType, info.targetMultiplicity(), true);
+                var forbiddenView = new ForbiddenView(symbol);
+                var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL);
+
+                storeBuilder.with(PartialRelationTranslator.of(linkType)
+                                .symbol(symbol)
+                                .may(Query.of(mayName, (builder, source, target) -> {
+                                        builder.clause(
+                                                        mayNewSource.call(source),
+                                                        mayNewTarget.call(target),
+                                                        not(forbiddenView.call(source, target))
+                                        );
+                                        if (info.isConstrained()) {
+                                                // Violation of monotonicity:
+                                                // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the
+                                                // corresponding error pattern will already mark the node as invalid.
+                                                builder.clause(
+                                                                must(linkType.call(source, target)),
+                                                                not(forbiddenView.call(source, target)),
+                                                                may(sourceType.call(source)),
+                                                                may(targetType.call(target))
+                                                );
+                                        }
+                                }))
+                                .refiner(DirectedCrossReferenceRefiner.of(symbol, sourceType, targetType))
+                                .initializer(new RefinementBasedInitializer<>(linkType)));
+
+                storeBuilder.with(new InvalidMultiplicityErrorTranslator(sourceType, linkType, false,
+                                info.sourceMultiplicity()));
+
+                storeBuilder.with(new InvalidMultiplicityErrorTranslator(targetType, linkType, true,
+                                info.targetMultiplicity()));
+        }
+
+        private RelationalQuery createMayHelper(PartialRelation type, Multiplicity multiplicity, boolean inverse) {
+                return CrossReferenceUtils.createMayHelper(linkType, type, multiplicity, inverse);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java
new file mode 100644
index 00000000..fe99bc54
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceInfo.java
@@ -0,0 +1,15 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.crossreference;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
+
+public record UndirectedCrossReferenceInfo(PartialRelation type, Multiplicity multiplicity) {
+        public boolean isConstrained() {
+                return multiplicity.isConstrained();
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java
new file mode 100644
index 00000000..43c1462b
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceRefiner.java
@@ -0,0 +1,44 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.crossreference;
+
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.refinement.ConcreteSymbolRefiner;
+import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+class UndirectedCrossReferenceRefiner extends ConcreteSymbolRefiner<TruthValue, Boolean> {
+        private final PartialInterpretationRefiner<TruthValue, Boolean> sourceRefiner;
+
+        public UndirectedCrossReferenceRefiner(ReasoningAdapter adapter, PartialSymbol<TruthValue, Boolean> partialSymbol,
+                                                                                   Symbol<TruthValue> concreteSymbol, PartialRelation sourceType) {
+                super(adapter, partialSymbol, concreteSymbol);
+                sourceRefiner = adapter.getRefiner(sourceType);
+        }
+
+        @Override
+        public boolean merge(Tuple key, TruthValue value) {
+                int source = key.get(0);
+                int target = key.get(1);
+                if (!super.merge(key, value) || !super.merge(Tuple.of(target, source), value)) {
+                        return false;
+                }
+                if (value.must()) {
+                        return sourceRefiner.merge(Tuple.of(source), TruthValue.TRUE) &&
+                                        sourceRefiner.merge(Tuple.of(target), TruthValue.TRUE);
+                }
+                return true;
+        }
+
+        public static Factory<TruthValue, Boolean> of(Symbol<TruthValue> concreteSymbol, PartialRelation sourceType) {
+                return (adapter, partialSymbol) -> new UndirectedCrossReferenceRefiner(adapter, partialSymbol, concreteSymbol,
+                                sourceType);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java
new file mode 100644
index 00000000..e599992d
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/crossreference/UndirectedCrossReferenceTranslator.java
@@ -0,0 +1,71 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.crossreference;
+
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.view.ForbiddenView;
+import tools.refinery.store.reasoning.lifting.DnfLifter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+import tools.refinery.store.reasoning.translator.multiplicity.InvalidMultiplicityErrorTranslator;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+
+import static tools.refinery.store.query.literal.Literals.not;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.may;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.must;
+
+public class UndirectedCrossReferenceTranslator implements ModelStoreConfiguration {
+        private final PartialRelation linkType;
+        private final UndirectedCrossReferenceInfo info;
+        private final Symbol<TruthValue> symbol;
+
+        public UndirectedCrossReferenceTranslator(PartialRelation linkType, UndirectedCrossReferenceInfo info) {
+                this.linkType = linkType;
+                this.info = info;
+                symbol = Symbol.of(linkType.name(), 2, TruthValue.class, TruthValue.UNKNOWN);
+        }
+
+        @Override
+        public void apply(ModelStoreBuilder storeBuilder) {
+                var name = linkType.name();
+                var type = info.type();
+                var forbiddenView = new ForbiddenView(symbol);
+                var mayName = DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL);
+
+                var mayNewSource = CrossReferenceUtils.createMayHelper(linkType, type, info.multiplicity(), false);
+
+                storeBuilder.with(PartialRelationTranslator.of(linkType)
+                                .symbol(symbol)
+                                .may(Query.of(mayName, (builder, source, target) -> {
+                                        builder.clause(
+                                                        mayNewSource.call(source),
+                                                        mayNewSource.call(target),
+                                                        not(forbiddenView.call(source, target))
+                                        );
+                                        if (info.isConstrained()) {
+                                                // Violation of monotonicity:
+                                                // Edges violating upper multiplicity will not be marked as {@code ERROR}, but the
+                                                // corresponding error pattern will already mark the node as invalid.
+                                                builder.clause(
+                                                                must(linkType.call(source, target)),
+                                                                not(forbiddenView.call(source, target)),
+                                                                may(type.call(source)),
+                                                                may(type.call(target))
+                                                );
+                                        }
+                                }))
+                                .refiner(UndirectedCrossReferenceRefiner.of(symbol, type))
+                                .initializer(new RefinementBasedInitializer<>(linkType)));
+
+                storeBuilder.with(new InvalidMultiplicityErrorTranslator(type, linkType, false, info.multiplicity()));
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ContainedTypeHierarchyBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ContainedTypeHierarchyBuilder.java
new file mode 100644
index 00000000..cc43bce6
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ContainedTypeHierarchyBuilder.java
@@ -0,0 +1,32 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.metamodel;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
+import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyBuilder;
+
+import java.util.Collection;
+
+public class ContainedTypeHierarchyBuilder extends TypeHierarchyBuilder {
+        ContainedTypeHierarchyBuilder() {
+        }
+
+        boolean isInvalidType(PartialRelation type) {
+                return !typeInfoMap.containsKey(type);
+        }
+
+        void setContainedTypes(Collection<PartialRelation> containedTypes) {
+                for (var containedType : containedTypes) {
+                        var currentInfo = typeInfoMap.get(containedType);
+                        if (currentInfo == null) {
+                                throw new IllegalArgumentException("Invalid contained type: " + containedType);
+                        }
+                        var newInfo = currentInfo.addSupertype(ContainmentHierarchyTranslator.CONTAINED_SYMBOL);
+                        typeInfoMap.put(containedType, newInfo);
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/Metamodel.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/Metamodel.java
new file mode 100644
index 00000000..72b836ff
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/Metamodel.java
@@ -0,0 +1,23 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.metamodel;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.containment.ContainmentInfo;
+import tools.refinery.store.reasoning.translator.crossreference.DirectedCrossReferenceInfo;
+import tools.refinery.store.reasoning.translator.crossreference.UndirectedCrossReferenceInfo;
+import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchy;
+
+import java.util.Map;
+
+public record Metamodel(TypeHierarchy typeHierarchy, Map<PartialRelation, ContainmentInfo> containmentHierarchy,
+                                                Map<PartialRelation, DirectedCrossReferenceInfo> directedCrossReferences,
+                                                Map<PartialRelation, UndirectedCrossReferenceInfo> undirectedCrossReferences,
+                                                Map<PartialRelation, PartialRelation> oppositeReferences) {
+        public static MetamodelBuilder builder() {
+                return new MetamodelBuilder();
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java
new file mode 100644
index 00000000..92370e25
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelBuilder.java
@@ -0,0 +1,223 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.metamodel;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
+import tools.refinery.store.reasoning.translator.containment.ContainmentInfo;
+import tools.refinery.store.reasoning.translator.crossreference.DirectedCrossReferenceInfo;
+import tools.refinery.store.reasoning.translator.crossreference.UndirectedCrossReferenceInfo;
+import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
+import tools.refinery.store.reasoning.translator.multiplicity.UnconstrainedMultiplicity;
+import tools.refinery.store.reasoning.translator.typehierarchy.TypeInfo;
+import tools.refinery.store.representation.cardinality.CardinalityIntervals;
+
+import java.util.*;
+
+public class MetamodelBuilder {
+        private final ContainedTypeHierarchyBuilder typeHierarchyBuilder = new ContainedTypeHierarchyBuilder();
+        private final Map<PartialRelation, ReferenceInfo> referenceInfoMap = new LinkedHashMap<>();
+        private final Set<PartialRelation> containedTypes = new HashSet<>();
+        private final Map<PartialRelation, ContainmentInfo> containmentHierarchy = new LinkedHashMap<>();
+        private final Map<PartialRelation, DirectedCrossReferenceInfo> directedCrossReferences = new LinkedHashMap<>();
+        private final Map<PartialRelation, UndirectedCrossReferenceInfo> undirectedCrossReferences = new LinkedHashMap<>();
+        private final Map<PartialRelation, PartialRelation> oppositeReferences = new LinkedHashMap<>();
+
+        MetamodelBuilder() {
+                typeHierarchyBuilder.type(ContainmentHierarchyTranslator.CONTAINED_SYMBOL, true);
+        }
+
+        public MetamodelBuilder type(PartialRelation partialRelation, TypeInfo typeInfo) {
+                typeHierarchyBuilder.type(partialRelation, typeInfo);
+                return this;
+
+        }
+
+        public MetamodelBuilder type(PartialRelation partialRelation, boolean abstractType,
+                                                                 PartialRelation... supertypes) {
+                typeHierarchyBuilder.type(partialRelation, abstractType, supertypes);
+                return this;
+        }
+
+        public MetamodelBuilder type(PartialRelation partialRelation, boolean abstractType,
+                                                                 Collection<PartialRelation> supertypes) {
+                typeHierarchyBuilder.type(partialRelation, abstractType, supertypes);
+                return this;
+        }
+
+        public MetamodelBuilder type(PartialRelation partialRelation, PartialRelation... supertypes) {
+                typeHierarchyBuilder.type(partialRelation, supertypes);
+                return this;
+        }
+
+        public MetamodelBuilder type(PartialRelation partialRelation, Collection<PartialRelation> supertypes) {
+                typeHierarchyBuilder.type(partialRelation, supertypes);
+                return this;
+        }
+
+        public MetamodelBuilder types(Collection<Map.Entry<PartialRelation, TypeInfo>> entries) {
+                typeHierarchyBuilder.types(entries);
+                return this;
+        }
+
+        public MetamodelBuilder types(Map<PartialRelation, TypeInfo> map) {
+                typeHierarchyBuilder.types(map);
+                return this;
+        }
+
+        public MetamodelBuilder reference(PartialRelation linkType, ReferenceInfo info) {
+                if (linkType.arity() != 2) {
+                        throw new IllegalArgumentException("Only references of arity 2 are supported, got %s with %d instead"
+                                        .formatted(linkType, linkType.arity()));
+                }
+                var putResult = referenceInfoMap.put(linkType, info);
+                if (putResult != null && !putResult.equals(info)) {
+                        throw new IllegalArgumentException("Duplicate reference info for partial relation: " + linkType);
+                }
+                return this;
+        }
+
+        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment,
+                                                                          Multiplicity multiplicity, PartialRelation targetType,
+                                                                          PartialRelation opposite) {
+                return reference(linkType, new ReferenceInfo(containment, sourceType, multiplicity, targetType, opposite));
+        }
+
+        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, Multiplicity multiplicity,
+                                                                          PartialRelation targetType, PartialRelation opposite) {
+                return reference(linkType, sourceType, false, multiplicity, targetType, opposite);
+        }
+
+        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType,
+                                                                          boolean containment, PartialRelation targetType, PartialRelation opposite) {
+                return reference(linkType, sourceType, containment, UnconstrainedMultiplicity.INSTANCE, targetType, opposite);
+        }
+
+        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, PartialRelation targetType,
+                                                                          PartialRelation opposite) {
+                return reference(linkType, sourceType, UnconstrainedMultiplicity.INSTANCE, targetType, opposite);
+        }
+
+        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment,
+                                                                          Multiplicity multiplicity, PartialRelation targetType) {
+                return reference(linkType, sourceType, containment, multiplicity, targetType, null);
+        }
+
+        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, Multiplicity multiplicity,
+                                                                          PartialRelation targetType) {
+                return reference(linkType, sourceType, multiplicity, targetType, null);
+        }
+
+        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType, boolean containment,
+                                                                          PartialRelation targetType) {
+                return reference(linkType, sourceType, containment, targetType, null);
+        }
+
+        public MetamodelBuilder reference(PartialRelation linkType, PartialRelation sourceType,
+                                                                          PartialRelation targetType) {
+                return reference(linkType, sourceType, targetType, null);
+        }
+
+        public MetamodelBuilder references(Collection<Map.Entry<PartialRelation, ReferenceInfo>> entries) {
+                for (var entry : entries) {
+                        reference(entry.getKey(), entry.getValue());
+                }
+                return this;
+        }
+
+        public MetamodelBuilder references(Map<PartialRelation, ReferenceInfo> map) {
+                return references(map.entrySet());
+        }
+
+        public Metamodel build() {
+                for (var entry : referenceInfoMap.entrySet()) {
+                        var linkType = entry.getKey();
+                        var info = entry.getValue();
+                        processReferenceInfo(linkType, info);
+                }
+                typeHierarchyBuilder.setContainedTypes(containedTypes);
+                var typeHierarchy = typeHierarchyBuilder.build();
+                return new Metamodel(typeHierarchy, Collections.unmodifiableMap(containmentHierarchy),
+                                Collections.unmodifiableMap(directedCrossReferences),
+                                Collections.unmodifiableMap(undirectedCrossReferences),
+                                Collections.unmodifiableMap(oppositeReferences));
+        }
+
+        private void processReferenceInfo(PartialRelation linkType, ReferenceInfo info) {
+                if (oppositeReferences.containsKey(linkType) || containmentHierarchy.containsKey(linkType)) {
+                        // We already processed this reference while processing its opposite.
+                        return;
+                }
+                var sourceType = info.sourceType();
+                var targetType = info.targetType();
+                if (typeHierarchyBuilder.isInvalidType(sourceType)) {
+                        throw new IllegalArgumentException("Source type %s of %s is not in type hierarchy"
+                                        .formatted(sourceType, linkType));
+                }
+                if (typeHierarchyBuilder.isInvalidType(targetType)) {
+                        throw new IllegalArgumentException("Target type %s of %s is not in type hierarchy"
+                                        .formatted(targetType, linkType));
+                }
+                var opposite = info.opposite();
+                Multiplicity targetMultiplicity = UnconstrainedMultiplicity.INSTANCE;
+                if (opposite != null) {
+                        var oppositeInfo = referenceInfoMap.get(opposite);
+                        validateOpposite(linkType, info, opposite, oppositeInfo);
+                        targetMultiplicity = oppositeInfo.multiplicity();
+                        if (oppositeInfo.containment()) {
+                                // Skip processing this reference and process it once we encounter its containment opposite.
+                                return;
+                        }
+                        if (opposite.equals(linkType)) {
+                                if (!sourceType.equals(targetType)) {
+                                        throw new IllegalArgumentException("Target %s of undirected reference %s differs from source %s"
+                                                        .formatted(targetType, linkType, sourceType));
+                                }
+                                undirectedCrossReferences.put(linkType, new UndirectedCrossReferenceInfo(sourceType,
+                                                info.multiplicity()));
+                                return;
+                        }
+                        oppositeReferences.put(opposite, linkType);
+                }
+                if (info.containment()) {
+                        if (targetMultiplicity.multiplicity().meet(CardinalityIntervals.ONE).isEmpty()) {
+                                throw new IllegalArgumentException("Invalid opposite %s with multiplicity %s of containment %s"
+                                                .formatted(opposite, targetMultiplicity, linkType));
+                        }
+                        containedTypes.add(targetType);
+                        containmentHierarchy.put(linkType, new ContainmentInfo(sourceType, info.multiplicity(), targetType));
+                        return;
+                }
+                directedCrossReferences.put(linkType, new DirectedCrossReferenceInfo(sourceType, info.multiplicity(),
+                                targetType, targetMultiplicity));
+        }
+
+        private static void validateOpposite(PartialRelation linkType, ReferenceInfo info, PartialRelation opposite,
+                                                                                 ReferenceInfo oppositeInfo) {
+                var sourceType = info.sourceType();
+                var targetType = info.targetType();
+                if (oppositeInfo == null) {
+                        throw new IllegalArgumentException("Opposite %s of %s is not defined"
+                                        .formatted(opposite, linkType));
+                }
+                if (!oppositeInfo.opposite().equals(linkType)) {
+                        throw new IllegalArgumentException("Expected %s to have opposite %s, got %s instead"
+                                        .formatted(opposite, linkType, oppositeInfo.opposite()));
+                }
+                if (!oppositeInfo.sourceType().equals(targetType)) {
+                        throw new IllegalArgumentException("Expected %s to have source type %s, got %s instead"
+                                        .formatted(opposite, targetType, oppositeInfo.sourceType()));
+                }
+                if (!oppositeInfo.targetType().equals(sourceType)) {
+                        throw new IllegalArgumentException("Expected %s to have target type %s, got %s instead"
+                                        .formatted(opposite, sourceType, oppositeInfo.targetType()));
+                }
+                if (oppositeInfo.containment() && info.containment()) {
+                        throw new IllegalArgumentException("Opposite %s of containment %s cannot be containment"
+                                        .formatted(opposite, linkType));
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTranslator.java
new file mode 100644
index 00000000..5afa58f2
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/MetamodelTranslator.java
@@ -0,0 +1,37 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.metamodel;
+
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
+import tools.refinery.store.reasoning.translator.containment.ContainmentHierarchyTranslator;
+import tools.refinery.store.reasoning.translator.crossreference.DirectedCrossReferenceTranslator;
+import tools.refinery.store.reasoning.translator.crossreference.UndirectedCrossReferenceTranslator;
+import tools.refinery.store.reasoning.translator.opposite.OppositeRelationTranslator;
+import tools.refinery.store.reasoning.translator.typehierarchy.TypeHierarchyTranslator;
+
+public class MetamodelTranslator implements ModelStoreConfiguration {
+        private final Metamodel metamodel;
+
+        public MetamodelTranslator(Metamodel metamodel) {
+                this.metamodel = metamodel;
+        }
+
+        @Override
+        public void apply(ModelStoreBuilder storeBuilder) {
+                storeBuilder.with(new TypeHierarchyTranslator(metamodel.typeHierarchy()));
+                storeBuilder.with(new ContainmentHierarchyTranslator(metamodel.containmentHierarchy()));
+                for (var entry : metamodel.directedCrossReferences().entrySet()) {
+                        storeBuilder.with(new DirectedCrossReferenceTranslator(entry.getKey(), entry.getValue()));
+                }
+                for (var entry : metamodel.undirectedCrossReferences().entrySet()) {
+                        storeBuilder.with(new UndirectedCrossReferenceTranslator(entry.getKey(), entry.getValue()));
+                }
+                for (var entry : metamodel.oppositeReferences().entrySet()) {
+                        storeBuilder.with(new OppositeRelationTranslator(entry.getKey(), entry.getValue()));
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java
new file mode 100644
index 00000000..9a6b4012
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/metamodel/ReferenceInfo.java
@@ -0,0 +1,13 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.metamodel;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.multiplicity.Multiplicity;
+
+public record ReferenceInfo(boolean containment, PartialRelation sourceType, Multiplicity multiplicity,
+                                                        PartialRelation targetType, PartialRelation opposite) {
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java
index 393a8769..61b9488c 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/EqualsRelationRewriter.java
@@ -69,12 +69,12 @@ class EqualsRelationRewriter extends QueryBasedRelationRewriter {
         }
 
         public static EqualsRelationRewriter of(AnySymbolView upperCardinalityView) {
-                var may = Query.of("MAY_EQUALS", (builder, p1, p2) -> builder
+                var may = Query.of("equals#may", (builder, p1, p2) -> builder
                                 .clause(
                                                 p1.isEquivalent(p2),
                                                 upperCardinalityView.call(p1, Variable.of(UpperCardinality.class))
                                 ));
-                var must = Query.of("MUST_EQUALS", (builder, p1, p2) -> builder
+                var must = Query.of("equals#must", (builder, p1, p2) -> builder
                                 .clause(UpperCardinality.class, upper -> List.of(
                                                 p1.isEquivalent(p2),
                                                 upperCardinalityView.call(p1, upper),
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java
index 09993c80..c62557d7 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiobject/MultiObjectTranslator.java
@@ -41,12 +41,12 @@ public class MultiObjectTranslator implements ModelStoreConfiguration {
                 storeBuilder.symbol(COUNT_STORAGE);
 
                 storeBuilder.with(PartialRelationTranslator.of(ReasoningAdapter.EXISTS_SYMBOL)
-                                .may(Query.of("MAY_EXISTS", (builder, p1) -> builder
+                                .may(Query.of("exists#may", (builder, p1) -> builder
                                                 .clause(UpperCardinality.class, upper -> List.of(
                                                                 UPPER_CARDINALITY_VIEW.call(p1, upper),
                                                                 check(greaterEq(upper, constant(UpperCardinalities.ONE)))
                                                 ))))
-                                .must(Query.of("MUST_EXISTS", (builder, p1) -> builder
+                                .must(Query.of("exists#must", (builder, p1) -> builder
                                                 .clause(Integer.class, lower -> List.of(
                                                                 LOWER_CARDINALITY_VIEW.call(p1, lower),
                                                                 check(greaterEq(lower, constant(1)))
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/ConstrainedMultiplicity.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/ConstrainedMultiplicity.java
new file mode 100644
index 00000000..e441e41e
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/ConstrainedMultiplicity.java
@@ -0,0 +1,36 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiplicity;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+import tools.refinery.store.representation.cardinality.CardinalityIntervals;
+import tools.refinery.store.representation.cardinality.NonEmptyCardinalityInterval;
+
+public record ConstrainedMultiplicity(NonEmptyCardinalityInterval multiplicity, PartialRelation errorSymbol)
+                implements Multiplicity {
+        public ConstrainedMultiplicity {
+                if (multiplicity.equals(CardinalityIntervals.SET)) {
+                        throw new IllegalArgumentException("Expected a constrained cardinality interval");
+                }
+                if (errorSymbol.arity() != 1) {
+                        throw new IllegalArgumentException("Expected error symbol %s to have arity 1, got %d instead"
+                                        .formatted(errorSymbol, errorSymbol.arity()));
+                }
+        }
+
+        public static ConstrainedMultiplicity of(CardinalityInterval multiplicity, PartialRelation errorSymbol) {
+                if (!(multiplicity instanceof NonEmptyCardinalityInterval nonEmptyCardinalityInterval)) {
+                        throw new IllegalArgumentException("Inconsistent multiplicity");
+                }
+                return new ConstrainedMultiplicity(nonEmptyCardinalityInterval, errorSymbol);
+        }
+
+        @Override
+        public boolean isConstrained() {
+                return true;
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java
new file mode 100644
index 00000000..522d8455
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/InvalidMultiplicityErrorTranslator.java
@@ -0,0 +1,115 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiplicity;
+
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.term.int_.IntTerms;
+import tools.refinery.store.reasoning.lifting.DnfLifter;
+import tools.refinery.store.reasoning.literal.*;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+import tools.refinery.store.representation.cardinality.FiniteUpperCardinality;
+import tools.refinery.store.representation.cardinality.UpperCardinalities;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+import java.util.List;
+
+import static tools.refinery.store.query.literal.Literals.check;
+import static tools.refinery.store.query.term.int_.IntTerms.greater;
+import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.constant;
+import static tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms.less;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.candidateMust;
+import static tools.refinery.store.reasoning.literal.PartialLiterals.must;
+
+public class InvalidMultiplicityErrorTranslator implements ModelStoreConfiguration {
+        private final PartialRelation nodeType;
+        private final PartialRelation linkType;
+        private final boolean inverse;
+        private final Multiplicity multiplicity;
+
+        public InvalidMultiplicityErrorTranslator(PartialRelation nodeType, PartialRelation linkType,
+                                                                                          boolean inverse, Multiplicity multiplicity) {
+                if (nodeType.arity() != 1) {
+                        throw new IllegalArgumentException("Node type must be of arity 1, got %s with arity %d instead"
+                                        .formatted(nodeType, nodeType.arity()));
+                }
+                if (linkType.arity() != 2) {
+                        throw new IllegalArgumentException("Link type must be of arity 2, got %s with arity %d instead"
+                                        .formatted(linkType, linkType.arity()));
+                }
+                this.nodeType = nodeType;
+                this.linkType = linkType;
+                this.inverse = inverse;
+                this.multiplicity = multiplicity;
+        }
+
+        @Override
+        public void apply(ModelStoreBuilder storeBuilder) {
+                if (!(multiplicity instanceof ConstrainedMultiplicity constrainedMultiplicity)) {
+                        return;
+                }
+
+                var name = constrainedMultiplicity.errorSymbol().name();
+                var cardinalityInterval = constrainedMultiplicity.multiplicity();
+                var node = Variable.of("node");
+                var other = Variable.of("other");
+                List<Variable> arguments = inverse ? List.of(other, node) : List.of(node, other);
+                var mustBuilder = Query.builder(DnfLifter.decorateName(name, Modality.MUST, Concreteness.PARTIAL))
+                                .parameter(node);
+                var candidateMayBuilder = Query.builder(DnfLifter.decorateName(name, Modality.MAY, Concreteness.PARTIAL))
+                                .parameter(node);
+                var candidateMustBuilder = Query.builder(DnfLifter.decorateName(name, Modality.MUST, Concreteness.PARTIAL))
+                                .parameter(node);
+
+                int lowerBound = cardinalityInterval.lowerBound();
+                if (lowerBound > 0) {
+                        var lowerBoundCardinality = UpperCardinalities.atMost(lowerBound);
+                        mustBuilder.clause(UpperCardinality.class, existingContents -> List.of(
+                                        must(nodeType.call(node)),
+                                        new CountUpperBoundLiteral(existingContents, linkType, arguments),
+                                        check(less(existingContents, constant(lowerBoundCardinality)))
+                        ));
+                        candidateMayBuilder.clause(Integer.class, existingContents -> List.of(
+                                        candidateMust(nodeType.call(node)),
+                                        new CountCandidateLowerBoundLiteral(existingContents, linkType, arguments),
+                                        check(IntTerms.less(existingContents, IntTerms.constant(lowerBound)))
+                        ));
+                        candidateMustBuilder.clause(Integer.class, existingContents -> List.of(
+                                        candidateMust(nodeType.call(node)),
+                                        new CountCandidateUpperBoundLiteral(existingContents, linkType, arguments),
+                                        check(IntTerms.less(existingContents, IntTerms.constant(lowerBound)))
+                        ));
+                }
+
+                if (cardinalityInterval.upperBound() instanceof FiniteUpperCardinality finiteUpperCardinality) {
+                        int upperBound = finiteUpperCardinality.finiteUpperBound();
+                        mustBuilder.clause(Integer.class, existingContents -> List.of(
+                                        must(nodeType.call(node)),
+                                        new CountLowerBoundLiteral(existingContents, linkType, arguments),
+                                        check(greater(existingContents, IntTerms.constant(upperBound)))
+                        ));
+                        candidateMayBuilder.clause(Integer.class, existingContents -> List.of(
+                                        candidateMust(nodeType.call(node)),
+                                        new CountCandidateUpperBoundLiteral(existingContents, linkType, arguments),
+                                        check(greater(existingContents, IntTerms.constant(upperBound)))
+                        ));
+                        candidateMustBuilder.clause(Integer.class, existingContents -> List.of(
+                                        candidateMust(nodeType.call(node)),
+                                        new CountCandidateLowerBoundLiteral(existingContents, linkType, arguments),
+                                        check(greater(existingContents, IntTerms.constant(upperBound)))
+                        ));
+                }
+
+                storeBuilder.with(PartialRelationTranslator.of(constrainedMultiplicity.errorSymbol())
+                                .mayNever()
+                                .must(mustBuilder.build())
+                                .candidateMay(candidateMayBuilder.build())
+                                .candidateMust(candidateMustBuilder.build()));
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/Multiplicity.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/Multiplicity.java
new file mode 100644
index 00000000..d1d6dd1e
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/Multiplicity.java
@@ -0,0 +1,14 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiplicity;
+
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+
+public sealed interface Multiplicity permits ConstrainedMultiplicity, UnconstrainedMultiplicity {
+        CardinalityInterval multiplicity();
+
+        boolean isConstrained();
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/UnconstrainedMultiplicity.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/UnconstrainedMultiplicity.java
new file mode 100644
index 00000000..2159b88c
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/multiplicity/UnconstrainedMultiplicity.java
@@ -0,0 +1,28 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.multiplicity;
+
+import tools.refinery.store.representation.cardinality.CardinalityInterval;
+import tools.refinery.store.representation.cardinality.CardinalityIntervals;
+
+// Singleton implementation, because there is only a single complete interval.
+@SuppressWarnings("squid:S6548")
+public final class UnconstrainedMultiplicity implements Multiplicity {
+        public static final UnconstrainedMultiplicity INSTANCE = new UnconstrainedMultiplicity();
+
+        private UnconstrainedMultiplicity() {
+        }
+
+        @Override
+        public CardinalityInterval multiplicity() {
+                return CardinalityIntervals.SET;
+        }
+
+        @Override
+        public boolean isConstrained() {
+                return true;
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java
new file mode 100644
index 00000000..7290ab40
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeInterpretation.java
@@ -0,0 +1,77 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.opposite;
+
+
+import tools.refinery.store.map.AnyVersionedMap;
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.interpretation.AbstractPartialInterpretation;
+import tools.refinery.store.reasoning.interpretation.PartialInterpretation;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.Set;
+
+class OppositeInterpretation<A, C> extends AbstractPartialInterpretation<A, C> {
+        private final PartialInterpretation<A, C> opposite;
+
+        private OppositeInterpretation(ReasoningAdapter adapter, Concreteness concreteness,
+                                                                   PartialSymbol<A, C> partialSymbol, PartialInterpretation<A, C> opposite) {
+                super(adapter, concreteness, partialSymbol);
+                this.opposite = opposite;
+        }
+
+        @Override
+        public A get(Tuple key) {
+                return opposite.get(OppositeUtils.flip(key));
+        }
+
+        @Override
+        public Cursor<Tuple, A> getAll() {
+                return new OppositeCursor<>(opposite.getAll());
+        }
+
+        public static <A1, C1> Factory<A1, C1> of(PartialSymbol<A1, C1> oppositeSymbol) {
+                return (adapter, concreteness, partialSymbol) -> {
+                        var opposite = adapter.getPartialInterpretation(concreteness, oppositeSymbol);
+                        return new OppositeInterpretation<>(adapter, concreteness, partialSymbol, opposite);
+                };
+        }
+
+        private record OppositeCursor<T>(Cursor<Tuple, T> opposite) implements Cursor<Tuple, T> {
+                @Override
+                public Tuple getKey() {
+                        return OppositeUtils.flip(opposite.getKey());
+                }
+
+                @Override
+                public T getValue() {
+                        return opposite.getValue();
+                }
+
+                @Override
+                public boolean isTerminated() {
+                        return opposite.isTerminated();
+                }
+
+                @Override
+                public boolean move() {
+                        return opposite.move();
+                }
+
+                @Override
+                public Set<AnyVersionedMap> getDependingMaps() {
+                        return opposite.getDependingMaps();
+                }
+
+                @Override
+                public boolean isDirty() {
+                        return opposite.isDirty();
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java
new file mode 100644
index 00000000..d09684df
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRefiner.java
@@ -0,0 +1,32 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.opposite;
+
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.refinement.AbstractPartialInterpretationRefiner;
+import tools.refinery.store.reasoning.refinement.PartialInterpretationRefiner;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.tuple.Tuple;
+
+public class OppositeRefiner<A, C> extends AbstractPartialInterpretationRefiner<A, C> {
+        private final PartialInterpretationRefiner<A, C> opposite;
+
+        protected OppositeRefiner(ReasoningAdapter adapter, PartialSymbol<A, C> partialSymbol,
+                                                          PartialSymbol<A, C> oppositeSymbol) {
+                super(adapter, partialSymbol);
+                opposite = adapter.getRefiner(oppositeSymbol);
+        }
+
+        @Override
+        public boolean merge(Tuple key, A value) {
+                var oppositeKey = OppositeUtils.flip(key);
+                return opposite.merge(oppositeKey, value);
+        }
+
+        public static <A1, C1> Factory<A1, C1> of(PartialSymbol<A1, C1> oppositeSymbol) {
+                return (adapter, partialSymbol) -> new OppositeRefiner<>(adapter, partialSymbol, oppositeSymbol);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRelationTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRelationTranslator.java
new file mode 100644
index 00000000..b25b9d7d
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeRelationTranslator.java
@@ -0,0 +1,51 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.opposite;
+
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.model.ModelStoreConfiguration;
+import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.reasoning.interpretation.PartialRelationRewriter;
+import tools.refinery.store.reasoning.literal.Concreteness;
+import tools.refinery.store.reasoning.literal.ModalConstraint;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.refinement.RefinementBasedInitializer;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.PartialRelationTranslator;
+
+import java.util.List;
+import java.util.Set;
+
+public class OppositeRelationTranslator implements ModelStoreConfiguration, PartialRelationRewriter {
+        private final PartialRelation linkType;
+        private final PartialRelation opposite;
+
+        public OppositeRelationTranslator(PartialRelation linkType, PartialRelation opposite) {
+                this.linkType = linkType;
+                this.opposite = opposite;
+        }
+
+        @Override
+        public void apply(ModelStoreBuilder storeBuilder) {
+                storeBuilder.with(PartialRelationTranslator.of(linkType)
+                                .rewriter(this)
+                                .interpretation(OppositeInterpretation.of(opposite))
+                                .refiner(OppositeRefiner.of(opposite))
+                                .initializer(new RefinementBasedInitializer<>(linkType)));
+        }
+
+        @Override
+        public List<Literal> rewriteLiteral(Set<Variable> positiveVariables, AbstractCallLiteral literal,
+                                                                                Modality modality, Concreteness concreteness) {
+                var arguments = literal.getArguments();
+                var newArguments = List.of(arguments.get(1), arguments.get(0));
+                var modalOpposite = new ModalConstraint(modality, concreteness, opposite);
+                var oppositeLiteral = literal.withArguments(modalOpposite, newArguments);
+                return List.of(oppositeLiteral);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeUtils.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeUtils.java
new file mode 100644
index 00000000..2a9e6b5d
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/opposite/OppositeUtils.java
@@ -0,0 +1,22 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.translator.opposite;
+
+import tools.refinery.store.tuple.Tuple;
+import tools.refinery.store.tuple.Tuple2;
+
+final class OppositeUtils {
+        private OppositeUtils() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static Tuple flip(Tuple tuple) {
+                if (!(tuple instanceof Tuple2 tuple2)) {
+                        throw new IllegalArgumentException("Cannot flip tuple: " + tuple);
+                }
+                return Tuple.of(tuple2.value1(), tuple2.value0());
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java
index 39a76745..ebe0d1b9 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java
@@ -10,7 +10,7 @@ import tools.refinery.store.representation.TruthValue;
 
 import java.util.*;
 
-final class TypeAnalysisResult {
+public final class TypeAnalysisResult {
         private final ExtendedTypeInfo extendedTypeInfo;
         private final List<PartialRelation> directSubtypes;
         private final List<ExtendedTypeInfo> allExternalTypeInfoList;
@@ -44,6 +44,10 @@ final class TypeAnalysisResult {
                 return inferredType;
         }
 
+        public boolean isSubtypeOf(TypeAnalysisResult other) {
+                return extendedTypeInfo.getAllSubtypes().contains(other.type());
+        }
+
         public InferredType merge(InferredType inferredType, TruthValue value) {
                 return switch (value) {
                         case UNKNOWN -> inferredType;
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java
index 99069ab9..c32a06cb 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchy.java
@@ -79,7 +79,12 @@ public class TypeHierarchy {
                                 var found = new HashSet<PartialRelation>();
                                 var allSupertypes = extendedTypeInfo.getAllSupertypes();
                                 for (var supertype : allSupertypes) {
-                                        found.addAll(extendedTypeInfoMap.get(supertype).getAllSupertypes());
+                                        var supertypeInfo = extendedTypeInfoMap.get(supertype);
+                                        if (supertypeInfo == null) {
+                                                throw new IllegalArgumentException("Supertype %s of %s is missing from the type hierarchy"
+                                                                .formatted(supertype, extendedTypeInfo.getType()));
+                                        }
+                                        found.addAll(supertypeInfo.getAllSupertypes());
                                 }
                                 if (allSupertypes.addAll(found)) {
                                         changed = true;
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java
index 0fca4810..36efb878 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyBuilder.java
@@ -7,18 +7,19 @@ package tools.refinery.store.reasoning.translator.typehierarchy;
 
 import tools.refinery.store.reasoning.representation.PartialRelation;
 
-import java.util.Collection;
-import java.util.LinkedHashMap;
-import java.util.List;
-import java.util.Map;
+import java.util.*;
 
+@SuppressWarnings("UnusedReturnValue")
 public class TypeHierarchyBuilder {
-        private final Map<PartialRelation, TypeInfo> typeInfoMap = new LinkedHashMap<>();
+        protected final Map<PartialRelation, TypeInfo> typeInfoMap = new LinkedHashMap<>();
+
+        protected TypeHierarchyBuilder() {
+        }
 
         public TypeHierarchyBuilder type(PartialRelation partialRelation, TypeInfo typeInfo) {
                 if (partialRelation.arity() != 1) {
-                        throw new IllegalArgumentException("Only types of arity 1 are supported, hot %d instead"
-                                        .formatted(partialRelation.arity()));
+                        throw new IllegalArgumentException("Only types of arity 1 are supported, got %s with %d instead"
+                                        .formatted(partialRelation, partialRelation.arity()));
                 }
                 var putResult = typeInfoMap.put(partialRelation, typeInfo);
                 if (putResult != null && !putResult.equals(typeInfo)) {
@@ -29,7 +30,7 @@ public class TypeHierarchyBuilder {
 
         public TypeHierarchyBuilder type(PartialRelation partialRelation, boolean abstractType,
                                                                          PartialRelation... supertypes) {
-                return type(partialRelation, abstractType, List.of(supertypes));
+                return type(partialRelation, abstractType, Set.of(supertypes));
         }
 
         public TypeHierarchyBuilder type(PartialRelation partialRelation, boolean abstractType,
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java
index 6a45acd3..4bff4557 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslator.java
@@ -44,7 +44,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration {
         }
 
         private ModelStoreConfiguration createPreservedTypeTranslator(PartialRelation type, TypeAnalysisResult result) {
-                var may = Query.of(type.name() + "#may", (builder, p1) -> {
+                var may = Query.of(type.name() + "#partial#may", (builder, p1) -> {
                         if (result.isAbstractType()) {
                                 for (var subtype : result.getDirectSubtypes()) {
                                         builder.clause(PartialLiterals.may(subtype.call(p1)));
@@ -54,7 +54,7 @@ public class TypeHierarchyTranslator implements ModelStoreConfiguration {
                         }
                 });
 
-                var must = Query.of(type.name() + "#must", (builder, p1) -> builder.clause(
+                var must = Query.of(type.name() + "#partial#must", (builder, p1) -> builder.clause(
                                 new MustTypeView(typeSymbol, type).call(p1)
                 ));
 
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java
index 68ed4089..e6bdaff2 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java
@@ -9,5 +9,15 @@ import tools.refinery.store.reasoning.representation.PartialRelation;
 
 import java.util.*;
 
-public record TypeInfo(Collection<PartialRelation> supertypes, boolean abstractType) {
+public record TypeInfo(Set<PartialRelation> supertypes, boolean abstractType) {
+        public TypeInfo(Collection<PartialRelation> supertypes, boolean abstractType) {
+                this(Set.copyOf(supertypes), abstractType);
+        }
+
+        public TypeInfo addSupertype(PartialRelation newSupertype) {
+                var newSupertypes = new ArrayList<PartialRelation>(supertypes.size() + 1);
+                newSupertypes.addAll(supertypes);
+                newSupertypes.add(newSupertype);
+                return new TypeInfo(newSupertypes, abstractType);
+        }
 }