refactor: rename PartialInterpretation adapter

46 files changed, 2206 insertions, 0 deletions

diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java
new file mode 100644
index 00000000..ebe82c8b
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/AnyPartialInterpretation.java
@@ -0,0 +1,13 @@
+package tools.refinery.store.reasoning;
+
+import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+
+public sealed interface AnyPartialInterpretation permits PartialInterpretation {
+        ReasoningAdapter getAdapter();
+
+        AnyPartialSymbol getPartialSymbol();
+
+        int countUnfinished();
+
+        int countErrors();
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java
new file mode 100644
index 00000000..0d51598b
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/MergeResult.java
@@ -0,0 +1,15 @@
+package tools.refinery.store.reasoning;
+
+public enum MergeResult {
+        UNCHANGED,
+        REFINED,
+        REJECTED;
+
+        public MergeResult andAlso(MergeResult other) {
+                return switch (this) {
+                        case UNCHANGED -> other;
+                        case REFINED -> other == REJECTED ? REJECTED : REFINED;
+                        case REJECTED -> REJECTED;
+                };
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java
new file mode 100644
index 00000000..99656da8
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/PartialInterpretation.java
@@ -0,0 +1,22 @@
+package tools.refinery.store.reasoning;
+
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.tuple.Tuple;
+
+public non-sealed interface PartialInterpretation<A, C> extends AnyPartialInterpretation {
+        @Override
+        PartialSymbol<A, C> getPartialSymbol();
+
+        A get(Tuple key);
+
+        Cursor<Tuple, A> getAll();
+
+        Cursor<Tuple, A> getAllErrors();
+
+        MergeResult merge(Tuple key, A value);
+
+        C getConcrete(Tuple key);
+
+        Cursor<Tuple, C> getAllConcrete();
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/Reasoning.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/Reasoning.java
new file mode 100644
index 00000000..d7d0a999
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/Reasoning.java
@@ -0,0 +1,24 @@
+package tools.refinery.store.reasoning;
+
+import tools.refinery.store.reasoning.internal.ReasoningBuilderImpl;
+import tools.refinery.store.adapter.ModelAdapterBuilderFactory;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+public final class Reasoning extends ModelAdapterBuilderFactory<ReasoningAdapter,
+                ReasoningStoreAdapter, ReasoningBuilder> {
+        public static final Reasoning ADAPTER = new Reasoning();
+
+        public static final PartialRelation EXISTS = new PartialRelation("exists", 1);
+
+        public static final PartialRelation EQUALS = new PartialRelation("equals", 1);
+
+        private Reasoning() {
+                super(ReasoningAdapter.class, ReasoningStoreAdapter.class, ReasoningBuilder.class);
+        }
+
+        @Override
+        public ReasoningBuilder createBuilder(ModelStoreBuilder storeBuilder) {
+                return new ReasoningBuilderImpl(storeBuilder);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java
new file mode 100644
index 00000000..e602242e
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningAdapter.java
@@ -0,0 +1,22 @@
+package tools.refinery.store.reasoning;
+
+import tools.refinery.store.adapter.ModelAdapter;
+import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.ResultSet;
+
+public interface ReasoningAdapter extends ModelAdapter {
+        @Override
+        ReasoningStoreAdapter getStoreAdapter();
+
+        default AnyPartialInterpretation getPartialInterpretation(AnyPartialSymbol partialSymbol) {
+                // Cast to disambiguate overloads.
+                var typedPartialSymbol = (PartialSymbol<?, ?>) partialSymbol;
+                return getPartialInterpretation(typedPartialSymbol);
+        }
+
+        <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol);
+
+        ResultSet getLiftedResultSet(Dnf query);
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java
new file mode 100644
index 00000000..588c2711
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningBuilder.java
@@ -0,0 +1,28 @@
+package tools.refinery.store.reasoning;
+
+import tools.refinery.store.adapter.ModelAdapterBuilder;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.query.Dnf;
+
+import java.util.Collection;
+import java.util.List;
+
+@SuppressWarnings("UnusedReturnValue")
+public interface ReasoningBuilder extends ModelAdapterBuilder {
+        default ReasoningBuilder liftedQueries(Dnf... liftedQueries) {
+                return liftedQueries(List.of(liftedQueries));
+        }
+
+        default ReasoningBuilder liftedQueries(Collection<Dnf> liftedQueries) {
+                liftedQueries.forEach(this::liftedQuery);
+                return this;
+        }
+
+        ReasoningBuilder liftedQuery(Dnf liftedQuery);
+
+        Dnf lift(Modality modality, Dnf query);
+
+        @Override
+        ReasoningStoreAdapter createStoreAdapter(ModelStore store);
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java
new file mode 100644
index 00000000..69c0f5eb
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/ReasoningStoreAdapter.java
@@ -0,0 +1,17 @@
+package tools.refinery.store.reasoning;
+
+import tools.refinery.store.adapter.ModelStoreAdapter;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+import tools.refinery.store.query.Dnf;
+
+import java.util.Collection;
+
+public interface ReasoningStoreAdapter extends ModelStoreAdapter {
+        Collection<AnyPartialSymbol> getPartialSymbols();
+
+        Collection<Dnf> getLiftedQueries();
+
+        @Override
+        ReasoningAdapter createModelAdapter(Model model);
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java
new file mode 100644
index 00000000..a7a56680
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningAdapterImpl.java
@@ -0,0 +1,38 @@
+package tools.refinery.store.reasoning.internal;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.reasoning.ReasoningAdapter;
+import tools.refinery.store.reasoning.PartialInterpretation;
+import tools.refinery.store.reasoning.representation.PartialSymbol;
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.ResultSet;
+
+public class ReasoningAdapterImpl implements ReasoningAdapter {
+        private final Model model;
+        private final ReasoningStoreAdapterImpl storeAdapter;
+
+        ReasoningAdapterImpl(Model model, ReasoningStoreAdapterImpl storeAdapter) {
+                this.model = model;
+                this.storeAdapter = storeAdapter;
+        }
+
+        @Override
+        public Model getModel() {
+                return model;
+        }
+
+        @Override
+        public ReasoningStoreAdapterImpl getStoreAdapter() {
+                return storeAdapter;
+        }
+
+        @Override
+        public <A, C> PartialInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) {
+                return null;
+        }
+
+        @Override
+        public ResultSet getLiftedResultSet(Dnf query) {
+                return null;
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
new file mode 100644
index 00000000..2860e2b9
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningBuilderImpl.java
@@ -0,0 +1,29 @@
+package tools.refinery.store.reasoning.internal;
+
+import tools.refinery.store.adapter.AbstractModelAdapterBuilder;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.reasoning.ReasoningBuilder;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.query.Dnf;
+
+public class ReasoningBuilderImpl extends AbstractModelAdapterBuilder implements ReasoningBuilder {
+        public ReasoningBuilderImpl(ModelStoreBuilder storeBuilder) {
+                super(storeBuilder);
+        }
+
+        @Override
+        public ReasoningBuilder liftedQuery(Dnf liftedQuery) {
+                return null;
+        }
+
+        @Override
+        public Dnf lift(Modality modality, Dnf query) {
+                return null;
+        }
+
+        @Override
+        public ReasoningStoreAdapterImpl createStoreAdapter(ModelStore store) {
+                return null;
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
new file mode 100644
index 00000000..763dad6d
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/internal/ReasoningStoreAdapterImpl.java
@@ -0,0 +1,37 @@
+package tools.refinery.store.reasoning.internal;
+
+import tools.refinery.store.reasoning.ReasoningStoreAdapter;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+import tools.refinery.store.query.Dnf;
+
+import java.util.Collection;
+
+public class ReasoningStoreAdapterImpl implements ReasoningStoreAdapter {
+        private final ModelStore store;
+
+        ReasoningStoreAdapterImpl(ModelStore store) {
+                this.store = store;
+        }
+
+        @Override
+        public ModelStore getStore() {
+                return store;
+        }
+
+        @Override
+        public Collection<AnyPartialSymbol> getPartialSymbols() {
+                return null;
+        }
+
+        @Override
+        public Collection<Dnf> getLiftedQueries() {
+                return null;
+        }
+
+        @Override
+        public ReasoningAdapterImpl createModelAdapter(Model model) {
+                return new ReasoningAdapterImpl(model, this);
+        }
+}
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
new file mode 100644
index 00000000..966e080a
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java
@@ -0,0 +1,107 @@
+package tools.refinery.store.reasoning.lifting;
+
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.reasoning.literal.ModalDnfCallLiteral;
+import tools.refinery.store.reasoning.Reasoning;
+import tools.refinery.store.reasoning.literal.ModalRelationLiteral;
+import tools.refinery.store.reasoning.literal.PartialRelationLiteral;
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.DnfBuilder;
+import tools.refinery.store.query.DnfClause;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.DnfCallLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.util.CycleDetectingMapper;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.List;
+
+public class DnfLifter {
+        private final CycleDetectingMapper<ModalDnf, Dnf> mapper = new CycleDetectingMapper<>(ModalDnf::toString,
+                        this::doLift);
+
+        public Dnf lift(Modality modality, Dnf query) {
+                return mapper.map(new ModalDnf(modality, query));
+        }
+
+        private Dnf doLift(ModalDnf modalDnf) {
+                var modality = modalDnf.modality();
+                var dnf = modalDnf.dnf();
+                var builder = Dnf.builder();
+                builder.parameters(dnf.getParameters());
+                boolean changed = false;
+                for (var clause : dnf.getClauses()) {
+                        if (liftClause(modality, clause, builder)) {
+                                changed = true;
+                        }
+                }
+                if (changed) {
+                        return builder.build();
+                }
+                return dnf;
+        }
+
+        private boolean liftClause(Modality modality, DnfClause clause, DnfBuilder builder) {
+                boolean changed = false;
+                var quantifiedVariables = new HashSet<>(clause.quantifiedVariables());
+                var literals = clause.literals();
+                var liftedLiterals = new ArrayList<Literal>(literals.size());
+                for (var literal : literals) {
+                        Literal liftedLiteral = liftLiteral(modality, literal);
+                        if (liftedLiteral == null) {
+                                liftedLiteral = literal;
+                        } else {
+                                changed = true;
+                        }
+                        liftedLiterals.add(liftedLiteral);
+                        var variable = isExistsLiteralForVariable(modality, liftedLiteral);
+                        if (variable != null) {
+                                // If we already quantify over the existence of the variable with the expected modality,
+                                // we don't need to insert quantification manually.
+                                quantifiedVariables.remove(variable);
+                        }
+                }
+                for (var quantifiedVariable : quantifiedVariables) {
+                        // Quantify over variables that are not already quantified with the expected modality.
+                        liftedLiterals.add(Reasoning.EXISTS.call(CallPolarity.POSITIVE, modality,
+                                        List.of(quantifiedVariable)));
+                }
+                builder.clause(liftedLiterals);
+                return changed || !quantifiedVariables.isEmpty();
+        }
+
+        @Nullable
+        private Variable isExistsLiteralForVariable(Modality modality, Literal literal) {
+                if (literal instanceof ModalRelationLiteral modalRelationLiteral &&
+                                modalRelationLiteral.getPolarity() == CallPolarity.POSITIVE &&
+                                modalRelationLiteral.getModality() == modality &&
+                                modalRelationLiteral.getTarget().equals(Reasoning.EXISTS)) {
+                        return modalRelationLiteral.getArguments().get(0);
+                }
+                return null;
+        }
+
+        @Nullable
+        private Literal liftLiteral(Modality modality, Literal literal) {
+                if (literal instanceof PartialRelationLiteral partialRelationLiteral) {
+                        return new ModalRelationLiteral(modality, partialRelationLiteral);
+                } else if (literal instanceof DnfCallLiteral dnfCallLiteral) {
+                        var polarity = dnfCallLiteral.getPolarity();
+                        var target = dnfCallLiteral.getTarget();
+                        var liftedTarget = lift(modality.commute(polarity), target);
+                        if (target.equals(liftedTarget)) {
+                                return null;
+                        }
+                        return new DnfCallLiteral(polarity, liftedTarget, dnfCallLiteral.getArguments());
+                } else if (literal instanceof ModalDnfCallLiteral modalDnfCallLiteral) {
+                        var liftedTarget = lift(modalDnfCallLiteral.getModality(), modalDnfCallLiteral.getTarget());
+                        return new DnfCallLiteral(modalDnfCallLiteral.getPolarity(), liftedTarget,
+                                        modalDnfCallLiteral.getArguments());
+                } else {
+                        return null;
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java
new file mode 100644
index 00000000..7aa98bf2
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/ModalDnf.java
@@ -0,0 +1,11 @@
+package tools.refinery.store.reasoning.lifting;
+
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.reasoning.literal.Modality;
+
+public record ModalDnf(Modality modality, Dnf dnf) {
+        @Override
+        public String toString() {
+                return "%s %s".formatted(modality, dnf.name());
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalDnfCallLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalDnfCallLiteral.java
new file mode 100644
index 00000000..1090f1ae
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalDnfCallLiteral.java
@@ -0,0 +1,48 @@
+package tools.refinery.store.reasoning.literal;
+
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.DnfCallLiteral;
+import tools.refinery.store.query.literal.LiteralReduction;
+import tools.refinery.store.query.literal.PolarLiteral;
+import tools.refinery.store.query.substitution.Substitution;
+
+import java.util.List;
+
+public class ModalDnfCallLiteral extends ModalLiteral<Dnf> implements PolarLiteral<ModalDnfCallLiteral> {
+        public ModalDnfCallLiteral(CallPolarity polarity, Modality modality, Dnf target, List<Variable> arguments) {
+                super(polarity, modality, target, arguments);
+        }
+
+        public ModalDnfCallLiteral(Modality modality, DnfCallLiteral baseLiteral) {
+                super(modality.commute(baseLiteral.getPolarity()), baseLiteral);
+        }
+
+        @Override
+        public Class<Dnf> getTargetType() {
+                return Dnf.class;
+        }
+
+        @Override
+        protected boolean targetEquals(LiteralEqualityHelper helper, Dnf otherTarget) {
+                return helper.dnfEqual(getTarget(), otherTarget);
+        }
+
+        @Override
+        public ModalDnfCallLiteral substitute(Substitution substitution) {
+                return new ModalDnfCallLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution));
+        }
+
+        @Override
+        public ModalDnfCallLiteral negate() {
+                return new ModalDnfCallLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments());
+        }
+
+        @Override
+        public LiteralReduction getReduction() {
+                var dnfReduction = getTarget().getReduction();
+                return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate();
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalLiteral.java
new file mode 100644
index 00000000..5992f172
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalLiteral.java
@@ -0,0 +1,63 @@
+package tools.refinery.store.reasoning.literal;
+
+import tools.refinery.store.query.RelationLike;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.literal.CallLiteral;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.Literal;
+
+import java.util.List;
+import java.util.Objects;
+
+public abstract class ModalLiteral<T extends RelationLike> extends CallLiteral<T> {
+        private final Modality modality;
+
+        protected ModalLiteral(CallPolarity polarity, Modality modality, T target, List<Variable> arguments) {
+                super(polarity, target, arguments);
+                this.modality = modality;
+        }
+
+        protected ModalLiteral(Modality modality, CallLiteral<? extends T> baseLiteral) {
+                this(baseLiteral.getPolarity(), commute(modality, baseLiteral.getPolarity()), baseLiteral.getTarget(),
+                                baseLiteral.getArguments());
+        }
+
+        public Modality getModality() {
+                return modality;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                // If {@link CallLiteral#equalsWithSubstitution(LiteralEqualityHelper, Literal)} has returned {@code true},
+                // we must have the same dynamic type as {@code other}.
+                var otherModalLiteral = (ModalLiteral<?>) other;
+                return modality == otherModalLiteral.modality;
+        }
+
+        @Override
+        protected String targetToString() {
+                return "%s %s".formatted(modality, super.targetToString());
+        }
+
+        @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;
+                ModalLiteral<?> that = (ModalLiteral<?>) o;
+                return modality == that.modality;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), modality);
+        }
+
+        private static Modality commute(Modality modality, CallPolarity polarity) {
+                return polarity.isPositive() ? modality : modality.negate();
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalRelationLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalRelationLiteral.java
new file mode 100644
index 00000000..9c72bd37
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalRelationLiteral.java
@@ -0,0 +1,37 @@
+package tools.refinery.store.reasoning.literal;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.PolarLiteral;
+import tools.refinery.store.query.substitution.Substitution;
+
+import java.util.List;
+
+public final class ModalRelationLiteral extends ModalLiteral<PartialRelation>
+                implements PolarLiteral<ModalRelationLiteral> {
+        public ModalRelationLiteral(CallPolarity polarity, Modality modality, PartialRelation target,
+                                                 List<Variable> arguments) {
+                super(polarity, modality, target, arguments);
+        }
+
+
+        public ModalRelationLiteral(Modality modality, PartialRelationLiteral baseLiteral) {
+                super(modality, baseLiteral);
+        }
+
+        @Override
+        public Class<PartialRelation> getTargetType() {
+                return PartialRelation.class;
+        }
+
+        @Override
+        public ModalRelationLiteral substitute(Substitution substitution) {
+                return new ModalRelationLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution));
+        }
+
+        @Override
+        public ModalRelationLiteral negate() {
+                return new ModalRelationLiteral(getPolarity().negate(), getModality(), getTarget(), getArguments());
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java
new file mode 100644
index 00000000..f0cb59de
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/Modality.java
@@ -0,0 +1,31 @@
+package tools.refinery.store.reasoning.literal;
+
+import tools.refinery.store.query.literal.CallPolarity;
+
+import java.util.Locale;
+
+public enum Modality {
+        MUST,
+        MAY,
+        CURRENT;
+
+        public Modality negate() {
+                return switch(this) {
+                        case MUST -> MAY;
+                        case MAY -> MUST;
+                        case CURRENT -> CURRENT;
+                };
+        }
+
+        public Modality commute(CallPolarity polarity) {
+                if (polarity.isPositive()) {
+                        return this;
+                }
+                return this.negate();
+        }
+
+        @Override
+        public String toString() {
+                return name().toLowerCase(Locale.ROOT);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java
new file mode 100644
index 00000000..10e4c7f7
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialLiterals.java
@@ -0,0 +1,33 @@
+package tools.refinery.store.reasoning.literal;
+
+import tools.refinery.store.query.literal.DnfCallLiteral;
+
+public final class PartialLiterals {
+        private PartialLiterals() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public ModalRelationLiteral may(PartialRelationLiteral literal) {
+                return new ModalRelationLiteral(Modality.MAY, literal);
+        }
+
+        public ModalRelationLiteral must(PartialRelationLiteral literal) {
+                return new ModalRelationLiteral(Modality.MUST, literal);
+        }
+
+        public ModalRelationLiteral current(PartialRelationLiteral literal) {
+                return new ModalRelationLiteral(Modality.CURRENT, literal);
+        }
+
+        public ModalDnfCallLiteral may(DnfCallLiteral literal) {
+                return new ModalDnfCallLiteral(Modality.MAY, literal);
+        }
+
+        public ModalDnfCallLiteral must(DnfCallLiteral literal) {
+                return new ModalDnfCallLiteral(Modality.MUST, literal);
+        }
+
+        public ModalDnfCallLiteral current(DnfCallLiteral literal) {
+                return new ModalDnfCallLiteral(Modality.CURRENT, literal);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialRelationLiteral.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialRelationLiteral.java
new file mode 100644
index 00000000..aff84538
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/PartialRelationLiteral.java
@@ -0,0 +1,32 @@
+package tools.refinery.store.reasoning.literal;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallLiteral;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.PolarLiteral;
+import tools.refinery.store.query.substitution.Substitution;
+
+import java.util.List;
+
+public final class PartialRelationLiteral extends CallLiteral<PartialRelation>
+                implements PolarLiteral<PartialRelationLiteral> {
+        public PartialRelationLiteral(CallPolarity polarity, PartialRelation target, List<Variable> substitution) {
+                super(polarity, target, substitution);
+        }
+
+        @Override
+        public Class<PartialRelation> getTargetType() {
+                return PartialRelation.class;
+        }
+
+        @Override
+        public PartialRelationLiteral substitute(Substitution substitution) {
+                return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
+        }
+
+        @Override
+        public PartialRelationLiteral negate() {
+                return new PartialRelationLiteral(getPolarity().negate(), getTarget(), getArguments());
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialFunction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialFunction.java
new file mode 100644
index 00000000..e74cd58b
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialFunction.java
@@ -0,0 +1,4 @@
+package tools.refinery.store.reasoning.representation;
+
+public sealed interface AnyPartialFunction extends AnyPartialSymbol permits PartialFunction {
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialSymbol.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialSymbol.java
new file mode 100644
index 00000000..6ff5031b
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/AnyPartialSymbol.java
@@ -0,0 +1,11 @@
+package tools.refinery.store.reasoning.representation;
+
+import tools.refinery.store.representation.AnyAbstractDomain;
+
+public sealed interface AnyPartialSymbol permits AnyPartialFunction, PartialSymbol {
+        String name();
+
+        int arity();
+
+        AnyAbstractDomain abstractDomain();
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java
new file mode 100644
index 00000000..59eeeefe
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialFunction.java
@@ -0,0 +1,32 @@
+package tools.refinery.store.reasoning.representation;
+
+import tools.refinery.store.representation.AbstractDomain;
+
+public record PartialFunction<A, C>(String name, int arity, AbstractDomain<A, C> abstractDomain)
+                implements AnyPartialFunction, PartialSymbol<A, C> {
+        @Override
+        public A defaultValue() {
+                return null;
+        }
+
+        @Override
+        public C defaultConcreteValue() {
+                return null;
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                return this == o;
+        }
+
+        @Override
+        public int hashCode() {
+                // Compare by identity to make hash table lookups more efficient.
+                return System.identityHashCode(this);
+        }
+
+        @Override
+        public String toString() {
+                return "%s/%d".formatted(name, arity);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java
new file mode 100644
index 00000000..f884f8d6
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java
@@ -0,0 +1,66 @@
+package tools.refinery.store.reasoning.representation;
+
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.literal.PartialRelationLiteral;
+import tools.refinery.store.reasoning.literal.ModalRelationLiteral;
+import tools.refinery.store.query.RelationLike;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.representation.AbstractDomain;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.representation.TruthValueDomain;
+
+import java.util.List;
+
+public record PartialRelation(String name, int arity) implements PartialSymbol<TruthValue, Boolean>, RelationLike {
+        @Override
+        public AbstractDomain<TruthValue, Boolean> abstractDomain() {
+                return TruthValueDomain.INSTANCE;
+        }
+
+        @Override
+        public TruthValue defaultValue() {
+                return TruthValue.FALSE;
+        }
+
+        @Override
+        public Boolean defaultConcreteValue() {
+                return false;
+        }
+
+        public ModalRelationLiteral call(CallPolarity polarity, Modality modality, List<Variable> arguments) {
+                return new ModalRelationLiteral(polarity, modality, this, arguments);
+        }
+
+        public PartialRelationLiteral call(CallPolarity polarity, List<Variable> arguments) {
+                return new PartialRelationLiteral(polarity, this, arguments);
+        }
+
+        public PartialRelationLiteral call(CallPolarity polarity, Variable... arguments) {
+                return call(polarity, List.of(arguments));
+        }
+
+        public PartialRelationLiteral call(Variable... arguments) {
+                return call(CallPolarity.POSITIVE, arguments);
+        }
+
+        public PartialRelationLiteral callTransitive(Variable left, Variable right) {
+                return call(CallPolarity.TRANSITIVE, List.of(left, right));
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                return this == o;
+        }
+
+        @Override
+        public int hashCode() {
+                // Compare by identity to make hash table lookups more efficient.
+                return System.identityHashCode(this);
+        }
+
+        @Override
+        public String toString() {
+                return "%s/%d".formatted(name, arity);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java
new file mode 100644
index 00000000..1af11f2e
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialSymbol.java
@@ -0,0 +1,12 @@
+package tools.refinery.store.reasoning.representation;
+
+import tools.refinery.store.representation.AbstractDomain;
+
+public sealed interface PartialSymbol<A, C> extends AnyPartialSymbol permits PartialFunction, PartialRelation {
+        @Override
+        AbstractDomain<A, C> abstractDomain();
+
+        A defaultValue();
+
+        C defaultConcreteValue();
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java
new file mode 100644
index 00000000..c7681b53
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RelationRefinementAction.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.reasoning.rule;
+
+import tools.refinery.store.reasoning.Reasoning;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.List;
+
+public record RelationRefinementAction(PartialRelation target, List<Variable> arguments, TruthValue value)
+                implements RuleAction {
+        public RelationRefinementAction {
+                if (arguments.size() != target.arity()) {
+                        throw new IllegalArgumentException("%s needs %d parameters, but got %s".formatted(target.name(),
+                                        target.arity(), arguments.size()));
+                }
+                if (value == TruthValue.UNKNOWN) {
+                        throw new IllegalArgumentException("Refining with UNKNOWN has no effect");
+                }
+        }
+
+        @Override
+        public RuleActionExecutor createExecutor(int[] argumentIndices, Model model) {
+                var targetInterpretation = model.getAdapter(Reasoning.ADAPTER).getPartialInterpretation(target);
+                return activationTuple -> {
+                        int arity = argumentIndices.length;
+                        var arguments = new int[arity];
+                        for (int i = 0; i < arity; i++) {
+                                arguments[i] = activationTuple.get(argumentIndices[i]);
+                        }
+                        return targetInterpretation.merge(Tuple.of(arguments), value);
+                };
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java
new file mode 100644
index 00000000..8a812518
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/Rule.java
@@ -0,0 +1,38 @@
+package tools.refinery.store.reasoning.rule;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.Dnf;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.List;
+
+public record Rule(Dnf precondition, List<RuleAction> actions) {
+        public Rule {
+                var parameterSet = new HashSet<>(precondition.getParameters());
+                for (var action : actions) {
+                        for (var argument : action.arguments()) {
+                                if (!parameterSet.contains(argument)) {
+                                        throw new IllegalArgumentException(
+                                                        "Argument %s of action %s does not appear in the parameter list %s of %s"
+                                                                        .formatted(argument, action, precondition.getParameters(), precondition.name()));
+                                }
+                        }
+                }
+        }
+
+        public RuleExecutor createExecutor(Model model) {
+                var parameters = precondition.getParameters();
+                var actionExecutors = new ArrayList<RuleActionExecutor>(actions.size());
+                for (var action : actions) {
+                        var arguments = action.arguments();
+                        int arity = arguments.size();
+                        var argumentIndices = new int[arity];
+                        for (int i = 0; i < arity; i++) {
+                                argumentIndices[i] = parameters.indexOf(arguments.get(i));
+                        }
+                        actionExecutors.add(action.createExecutor(argumentIndices, model));
+                }
+                return new RuleExecutor(this, model, actionExecutors);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java
new file mode 100644
index 00000000..bf980759
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleAction.java
@@ -0,0 +1,12 @@
+package tools.refinery.store.reasoning.rule;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.Variable;
+
+import java.util.List;
+
+public interface RuleAction {
+        List<Variable> arguments();
+
+        RuleActionExecutor createExecutor(int[] argumentIndices, Model model);
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleActionExecutor.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleActionExecutor.java
new file mode 100644
index 00000000..80bfa6f8
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleActionExecutor.java
@@ -0,0 +1,9 @@
+package tools.refinery.store.reasoning.rule;
+
+import tools.refinery.store.reasoning.MergeResult;
+import tools.refinery.store.tuple.TupleLike;
+
+@FunctionalInterface
+public interface RuleActionExecutor {
+        MergeResult execute(TupleLike activationTuple);
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleExecutor.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleExecutor.java
new file mode 100644
index 00000000..1e5322b4
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/rule/RuleExecutor.java
@@ -0,0 +1,34 @@
+package tools.refinery.store.reasoning.rule;
+
+import tools.refinery.store.reasoning.MergeResult;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.tuple.TupleLike;
+
+import java.util.List;
+
+public final class RuleExecutor {
+        private final Rule rule;
+        private final Model model;
+        private final List<RuleActionExecutor> actionExecutors;
+
+        RuleExecutor(Rule rule, Model model, List<RuleActionExecutor> actionExecutors) {
+                this.rule = rule;
+                this.model = model;
+                this.actionExecutors = actionExecutors;
+        }
+
+        public Rule getRule() {
+                return rule;
+        }
+
+        public Model getModel() {
+                return model;
+        }
+        public MergeResult execute(TupleLike activationTuple) {
+                MergeResult mergeResult = MergeResult.UNCHANGED;
+                for (var actionExecutor : actionExecutors) {
+                        mergeResult = mergeResult.andAlso(actionExecutor.execute(activationTuple));
+                }
+                return mergeResult;
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java
new file mode 100644
index 00000000..7909a7e1
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java
@@ -0,0 +1,159 @@
+package tools.refinery.store.reasoning.translator;
+
+import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.substitution.Substitutions;
+
+import java.util.*;
+
+public final class Advice {
+        private final AnyPartialSymbol source;
+        private final PartialRelation target;
+        private final AdviceSlot slot;
+        private final boolean mandatory;
+        private final List<Variable> parameters;
+        private final List<Literal> literals;
+        private boolean processed;
+
+        public Advice(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot, boolean mandatory, List<Variable> parameters, List<Literal> literals) {
+                if (mandatory && !slot.isMonotonic()) {
+                        throw new IllegalArgumentException("Only monotonic advice can be mandatory");
+                }
+                this.source = source;
+                this.target = target;
+                this.slot = slot;
+                this.mandatory = mandatory;
+                checkArity(parameters);
+                this.parameters = parameters;
+                this.literals = literals;
+        }
+
+        public AnyPartialSymbol source() {
+                return source;
+        }
+
+        public PartialRelation target() {
+                return target;
+        }
+
+        public AdviceSlot slot() {
+                return slot;
+        }
+
+        public boolean mandatory() {
+                return mandatory;
+        }
+
+        public List<Variable> parameters() {
+                return parameters;
+        }
+
+        public List<Literal> literals() {
+                return literals;
+        }
+
+        public boolean processed() {
+                return processed;
+        }
+
+        public List<Literal> substitute(List<Variable> substituteParameters) {
+                checkArity(substituteParameters);
+                markProcessed();
+                int arity = parameters.size();
+                var variableMap = new HashMap<Variable, Variable>(arity);
+                for (int i = 0; i < arity; i++) {
+                        variableMap.put(parameters.get(i), substituteParameters.get(i));
+                }
+                // Use a renewing substitution to remove any non-parameter variables and avoid clashed between variables
+                // coming from different advice in the same clause.
+                var substitution = Substitutions.renewing(variableMap);
+                return literals.stream().map(literal -> literal.substitute(substitution)).toList();
+        }
+
+        private void markProcessed() {
+                processed = true;
+        }
+
+        public void checkProcessed() {
+                if (mandatory && !processed) {
+                        throw new IllegalStateException("Mandatory advice %s was not processed".formatted(this));
+                }
+        }
+
+        private void checkArity(List<Variable> toCheck) {
+                if (toCheck.size() != target.arity()) {
+                        throw new IllegalArgumentException("%s needs %d parameters, but got %s".formatted(target.name(),
+                                        target.arity(), parameters.size()));
+                }
+        }
+
+        public static Builder builderFor(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) {
+                return new Builder(source, target, slot);
+        }
+
+
+        @Override
+        public String toString() {
+                return "Advice[source=%s, target=%s, slot=%s, mandatory=%s, parameters=%s, literals=%s]".formatted(source,
+                                target, slot, mandatory, parameters, literals);
+        }
+
+        public static class Builder {
+                private final AnyPartialSymbol source;
+                private final PartialRelation target;
+                private final AdviceSlot slot;
+                private boolean mandatory;
+                private final List<Variable> parameters = new ArrayList<>();
+                private final List<Literal> literals = new ArrayList<>();
+
+                private Builder(AnyPartialSymbol source, PartialRelation target, AdviceSlot slot) {
+                        this.source = source;
+                        this.target = target;
+                        this.slot = slot;
+                }
+
+                public Builder mandatory(boolean mandatory) {
+                        this.mandatory = mandatory;
+                        return this;
+                }
+
+                public Builder mandatory() {
+                        return mandatory(false);
+                }
+
+                public Builder parameters(List<Variable> variables) {
+                        parameters.addAll(variables);
+                        return this;
+                }
+
+                public Builder parameters(Variable... variables) {
+                        return parameters(List.of(variables));
+                }
+
+                public Builder parameter(Variable variable) {
+                        parameters.add(variable);
+                        return this;
+                }
+
+                public Builder literals(Collection<Literal> literals) {
+                        this.literals.addAll(literals);
+                        return this;
+                }
+
+                public Builder literals(Literal... literals) {
+                        return literals(List.of(literals));
+                }
+
+                public Builder literal(Literal literal) {
+                        literals.add(literal);
+                        return this;
+                }
+
+                public Advice build() {
+                        return new Advice(source, target, slot, mandatory, Collections.unmodifiableList(parameters),
+                                        Collections.unmodifiableList(literals));
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java
new file mode 100644
index 00000000..f3bd9c5e
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/AdviceSlot.java
@@ -0,0 +1,25 @@
+package tools.refinery.store.reasoning.translator;
+
+import tools.refinery.store.representation.TruthValue;
+
+public enum AdviceSlot {
+        EXTEND_MUST(true),
+
+        RESTRICT_MAY(true),
+
+        /**
+         * Same as {@link #RESTRICT_MAY}, but only active if the value of the relation is not {@link TruthValue#TRUE} or
+         * {@link TruthValue#ERROR}.
+         */
+        RESTRICT_NEW(false);
+
+        private final boolean monotonic;
+
+        AdviceSlot(boolean monotonic) {
+                this.monotonic = monotonic;
+        }
+
+        public boolean isMonotonic() {
+                return monotonic;
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Seed.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Seed.java
new file mode 100644
index 00000000..779eadbe
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Seed.java
@@ -0,0 +1,12 @@
+package tools.refinery.store.reasoning.translator;
+
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.tuple.Tuple;
+
+public interface Seed<T> {
+        int arity();
+
+        T get(Tuple key);
+
+        Cursor<Tuple, T> getCursor(T defaultValue, int nodeCount);
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java
new file mode 100644
index 00000000..e45d20c8
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/TranslationUnit.java
@@ -0,0 +1,48 @@
+package tools.refinery.store.reasoning.translator;
+
+import tools.refinery.store.reasoning.ReasoningBuilder;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.reasoning.AnyPartialInterpretation;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.Literal;
+
+import java.util.Collection;
+import java.util.List;
+import java.util.Map;
+
+public abstract class TranslationUnit {
+        private ReasoningBuilder reasoningBuilder;
+
+        protected ReasoningBuilder getPartialInterpretationBuilder() {
+                return reasoningBuilder;
+        }
+
+        public void setPartialInterpretationBuilder(ReasoningBuilder reasoningBuilder) {
+                this.reasoningBuilder = reasoningBuilder;
+        }
+
+        protected ModelStoreBuilder getModelStoreBuilder() {
+                return reasoningBuilder.getStoreBuilder();
+        }
+
+        public abstract Collection<AnyPartialSymbol> getTranslatedPartialSymbols();
+
+        public Collection<Advice> computeAdvices() {
+                // No advices to give by default.
+                return List.of();
+        }
+
+        public abstract void configure(Collection<Advice> advices);
+
+        public abstract List<Literal> call(CallPolarity polarity, Modality modality, PartialRelation target,
+                                                                           List<Variable> arguments);
+
+        public abstract Map<AnyPartialSymbol, AnyPartialInterpretation> createPartialInterpretations(Model model);
+
+        public abstract void initializeModel(Model model, int nodeCount);
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java
new file mode 100644
index 00000000..1b8d7cc9
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/EliminatedType.java
@@ -0,0 +1,6 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+record EliminatedType(PartialRelation replacement) implements TypeAnalysisResult {
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/ExtendedTypeInfo.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/ExtendedTypeInfo.java
new file mode 100644
index 00000000..43b8e1dd
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/ExtendedTypeInfo.java
@@ -0,0 +1,101 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import org.jetbrains.annotations.NotNull;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+import java.util.HashSet;
+import java.util.LinkedHashSet;
+import java.util.Objects;
+import java.util.Set;
+
+final class ExtendedTypeInfo implements Comparable<ExtendedTypeInfo> {
+        private final int index;
+        private final PartialRelation type;
+        private final TypeInfo typeInfo;
+        private final Set<PartialRelation> allSubtypes = new LinkedHashSet<>();
+        private final Set<PartialRelation> allSupertypes;
+        private final Set<PartialRelation> concreteSubtypesAndSelf = new LinkedHashSet<>();
+        private Set<PartialRelation> directSubtypes;
+        private final Set<PartialRelation> unsortedDirectSupertypes = new HashSet<>();
+
+        public ExtendedTypeInfo(int index, PartialRelation type, TypeInfo typeInfo) {
+                this.index = index;
+                this.type = type;
+                this.typeInfo = typeInfo;
+                this.allSupertypes = new LinkedHashSet<>(typeInfo.supertypes());
+        }
+
+        public PartialRelation getType() {
+                return type;
+        }
+
+        public TypeInfo getTypeInfo() {
+                return typeInfo;
+        }
+
+        public boolean isAbstractType() {
+                return getTypeInfo().abstractType();
+        }
+
+        public Set<PartialRelation> getAllSubtypes() {
+                return allSubtypes;
+        }
+
+        public Set<PartialRelation> getAllSupertypes() {
+                return allSupertypes;
+        }
+
+        public Set<PartialRelation> getAllSupertypesAndSelf() {
+                var allSubtypesAndSelf = new HashSet<PartialRelation>(allSupertypes.size() + 1);
+                addMust(allSubtypesAndSelf);
+                return allSubtypesAndSelf;
+        }
+
+        public Set<PartialRelation> getConcreteSubtypesAndSelf() {
+                return concreteSubtypesAndSelf;
+        }
+
+        public Set<PartialRelation> getDirectSubtypes() {
+                return directSubtypes;
+        }
+
+        public Set<PartialRelation> getUnsortedDirectSupertypes() {
+                return unsortedDirectSupertypes;
+        }
+
+        public void setDirectSubtypes(Set<PartialRelation> directSubtypes) {
+                this.directSubtypes = directSubtypes;
+        }
+
+        public boolean allowsAllConcreteTypes(Set<PartialRelation> concreteTypes) {
+                for (var concreteType : concreteTypes) {
+                        if (!concreteSubtypesAndSelf.contains(concreteType)) {
+                                return false;
+                        }
+                }
+                return true;
+        }
+
+        public void addMust(Set<PartialRelation> mustTypes) {
+                mustTypes.add(type);
+                mustTypes.addAll(allSupertypes);
+        }
+
+        @Override
+        public int compareTo(@NotNull ExtendedTypeInfo extendedTypeInfo) {
+                return Integer.compare(index, extendedTypeInfo.index);
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                ExtendedTypeInfo that = (ExtendedTypeInfo) o;
+                return index == that.index;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(index);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeRelationView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeRelationView.java
new file mode 100644
index 00000000..12c37c86
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMayTypeRelationView.java
@@ -0,0 +1,19 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.query.view.TuplePreservingRelationView;
+import tools.refinery.store.tuple.Tuple;
+
+class InferredMayTypeRelationView extends TuplePreservingRelationView<InferredType> {
+        private final PartialRelation type;
+
+        InferredMayTypeRelationView(PartialRelation type) {
+                super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#may".formatted(type));
+                this.type = type;
+        }
+
+        @Override
+        public boolean filter(Tuple key, InferredType value) {
+                return value.mayConcreteTypes().contains(type);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeRelationView.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeRelationView.java
new file mode 100644
index 00000000..975f627e
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredMustTypeRelationView.java
@@ -0,0 +1,19 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.query.view.TuplePreservingRelationView;
+import tools.refinery.store.tuple.Tuple;
+
+class InferredMustTypeRelationView extends TuplePreservingRelationView<InferredType> {
+        private final PartialRelation type;
+
+        InferredMustTypeRelationView(PartialRelation type) {
+                super(TypeHierarchyTranslationUnit.INFERRED_TYPE_SYMBOL, "%s#must".formatted(type));
+                this.type = type;
+        }
+
+        @Override
+        public boolean filter(Tuple key, InferredType value) {
+                return value.mustTypes().contains(type);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java
new file mode 100644
index 00000000..a366e262
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredType.java
@@ -0,0 +1,30 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+import java.util.Collections;
+import java.util.Set;
+
+record InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes,
+                                        PartialRelation currentType) {
+        public static final InferredType UNTYPED = new InferredType(Set.of(), Set.of(), null);
+
+        public InferredType(Set<PartialRelation> mustTypes, Set<PartialRelation> mayConcreteTypes,
+                                                PartialRelation currentType) {
+                this.mustTypes = Collections.unmodifiableSet(mustTypes);
+                this.mayConcreteTypes = Collections.unmodifiableSet(mayConcreteTypes);
+                this.currentType = currentType;
+        }
+
+        public boolean isConsistent() {
+                return currentType != null || mustTypes.isEmpty();
+        }
+
+        public boolean isMust(PartialRelation partialRelation) {
+                return mustTypes.contains(partialRelation);
+        }
+
+        public boolean isMayConcrete(PartialRelation partialRelation) {
+                return mayConcreteTypes.contains(partialRelation);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java
new file mode 100644
index 00000000..63dba964
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/PreservedType.java
@@ -0,0 +1,136 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.TruthValue;
+
+import java.util.*;
+
+final class PreservedType implements TypeAnalysisResult {
+        private final ExtendedTypeInfo extendedTypeInfo;
+        private final List<PartialRelation> directSubtypes;
+        private final List<ExtendedTypeInfo> allExternalTypeInfoList;
+        private final InferredType inferredType;
+
+        public PreservedType(ExtendedTypeInfo extendedTypeInfo, List<ExtendedTypeInfo> allExternalTypeInfoList) {
+                this.extendedTypeInfo = extendedTypeInfo;
+                directSubtypes = List.copyOf(extendedTypeInfo.getDirectSubtypes());
+                this.allExternalTypeInfoList = allExternalTypeInfoList;
+                inferredType = propagateMust(extendedTypeInfo.getAllSupertypesAndSelf(),
+                                extendedTypeInfo.getConcreteSubtypesAndSelf());
+        }
+
+        public PartialRelation type() {
+                return extendedTypeInfo.getType();
+        }
+
+        public List<PartialRelation> getDirectSubtypes() {
+                return directSubtypes;
+        }
+
+        public boolean isAbstractType() {
+                return extendedTypeInfo.isAbstractType();
+        }
+
+        public boolean isVacuous() {
+                return isAbstractType() && directSubtypes.isEmpty();
+        }
+
+        public InferredType asInferredType() {
+                return inferredType;
+        }
+
+        public InferredType merge(InferredType inferredType, TruthValue value) {
+                return switch (value) {
+                        case UNKNOWN -> inferredType;
+                        case TRUE -> addMust(inferredType);
+                        case FALSE -> removeMay(inferredType);
+                        case ERROR -> addError(inferredType);
+                };
+        }
+
+        private InferredType addMust(InferredType inferredType) {
+                var originalMustTypes = inferredType.mustTypes();
+                if (originalMustTypes.contains(type())) {
+                        return inferredType;
+                }
+                var mustTypes = new HashSet<>(originalMustTypes);
+                extendedTypeInfo.addMust(mustTypes);
+                var originalMayConcreteTypes = inferredType.mayConcreteTypes();
+                var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes);
+                Set<PartialRelation> mayConcreteTypesResult;
+                if (mayConcreteTypes.retainAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) {
+                        mayConcreteTypesResult = mayConcreteTypes;
+                } else {
+                        mayConcreteTypesResult = originalMayConcreteTypes;
+                }
+                return propagateMust(mustTypes, mayConcreteTypesResult);
+        }
+
+        private InferredType removeMay(InferredType inferredType) {
+                var originalMayConcreteTypes = inferredType.mayConcreteTypes();
+                var mayConcreteTypes = new LinkedHashSet<>(originalMayConcreteTypes);
+                if (!mayConcreteTypes.removeAll(extendedTypeInfo.getConcreteSubtypesAndSelf())) {
+                        return inferredType;
+                }
+                return propagateMust(inferredType.mustTypes(), mayConcreteTypes);
+        }
+
+        private InferredType addError(InferredType inferredType) {
+                var originalMustTypes = inferredType.mustTypes();
+                if (originalMustTypes.contains(type())) {
+                        if (inferredType.mayConcreteTypes().isEmpty()) {
+                                return inferredType;
+                        }
+                        return new InferredType(originalMustTypes, Set.of(), null);
+                }
+                var mustTypes = new HashSet<>(originalMustTypes);
+                extendedTypeInfo.addMust(mustTypes);
+                return new InferredType(mustTypes, Set.of(), null);
+        }
+
+        private InferredType propagateMust(Set<PartialRelation> originalMustTypes,
+                                                                           Set<PartialRelation> mayConcreteTypes) {
+                // It is possible that there is not type at all, do not force one by propagation.
+                var maybeUntyped = originalMustTypes.isEmpty();
+                // Para-consistent case, do not propagate must types to avoid logical explosion.
+                var paraConsistentOrSurelyUntyped = mayConcreteTypes.isEmpty();
+                if (maybeUntyped || paraConsistentOrSurelyUntyped) {
+                        return new InferredType(originalMustTypes, mayConcreteTypes, null);
+                }
+                var currentType = computeCurrentType(mayConcreteTypes);
+                var mustTypes = new HashSet<>(originalMustTypes);
+                boolean changed = false;
+                for (var newMustExtendedTypeInfo : allExternalTypeInfoList) {
+                        var newMustType = newMustExtendedTypeInfo.getType();
+                        if (mustTypes.contains(newMustType)) {
+                                continue;
+                        }
+                        if (newMustExtendedTypeInfo.allowsAllConcreteTypes(mayConcreteTypes)) {
+                                newMustExtendedTypeInfo.addMust(mustTypes);
+                                changed = true;
+                        }
+                }
+                if (!changed) {
+                        return new InferredType(originalMustTypes, mayConcreteTypes, currentType);
+                }
+                return new InferredType(mustTypes, mayConcreteTypes, currentType);
+        }
+
+        /**
+         * Returns a concrete type that is allowed by a (consistent, i.e., nonempty) set of <b>may</b> concrete types.
+         *
+         * @param mayConcreteTypes The set of allowed concrete types. Must not be empty.
+         * @return The first concrete type that is allowed by {@code matConcreteTypes}.
+         */
+        private PartialRelation computeCurrentType(Set<PartialRelation> mayConcreteTypes) {
+                for (var concreteExtendedTypeInfo : allExternalTypeInfoList) {
+                        var concreteType = concreteExtendedTypeInfo.getType();
+                        if (!concreteExtendedTypeInfo.isAbstractType() && mayConcreteTypes.contains(concreteType)) {
+                                return concreteType;
+                        }
+                }
+                // We have already filtered out the para-consistent case in {@link #propagateMust(Set<PartialRelation>,
+                // Set<PartialRelation>}.
+                throw new AssertionError("No concrete type in %s".formatted(mayConcreteTypes));
+        }
+}
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
new file mode 100644
index 00000000..4f915108
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalysisResult.java
@@ -0,0 +1,4 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+sealed interface TypeAnalysisResult permits EliminatedType, PreservedType {
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzer.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzer.java
new file mode 100644
index 00000000..62f8e750
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzer.java
@@ -0,0 +1,202 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+import java.util.*;
+
+class TypeAnalyzer {
+        private final Map<PartialRelation, ExtendedTypeInfo> extendedTypeInfoMap;
+        private final Map<PartialRelation, PartialRelation> replacements = new LinkedHashMap<>();
+        private final InferredType unknownType;
+        private final Map<PartialRelation, TypeAnalysisResult> analysisResults;
+
+        public TypeAnalyzer(Map<PartialRelation, TypeInfo> typeInfoMap) {
+                int size = typeInfoMap.size();
+                extendedTypeInfoMap = new LinkedHashMap<>(size);
+                var concreteTypes = new LinkedHashSet<PartialRelation>();
+                int index = 0;
+                for (var entry : typeInfoMap.entrySet()) {
+                        var type = entry.getKey();
+                        var typeInfo = entry.getValue();
+                        extendedTypeInfoMap.put(type, new ExtendedTypeInfo(index, type, typeInfo));
+                        if (!typeInfo.abstractType()) {
+                                concreteTypes.add(type);
+                        }
+                        index++;
+                }
+                unknownType = new InferredType(Set.of(), concreteTypes, null);
+                computeAllSupertypes();
+                computeAllAndConcreteSubtypes();
+                computeDirectSubtypes();
+                eliminateTrivialSupertypes();
+                analysisResults = computeAnalysisResults();
+        }
+
+        public InferredType getUnknownType() {
+                return unknownType;
+        }
+
+        public Map<PartialRelation, TypeAnalysisResult> getAnalysisResults() {
+                return analysisResults;
+        }
+
+        private void computeAllSupertypes() {
+                boolean changed;
+                do {
+                        changed = false;
+                        for (var extendedTypeInfo : extendedTypeInfoMap.values()) {
+                                var found = new HashSet<PartialRelation>();
+                                var allSupertypes = extendedTypeInfo.getAllSupertypes();
+                                for (var supertype : allSupertypes) {
+                                        found.addAll(extendedTypeInfoMap.get(supertype).getAllSupertypes());
+                                }
+                                if (allSupertypes.addAll(found)) {
+                                        changed = true;
+                                }
+                        }
+                } while (changed);
+        }
+
+        private void computeAllAndConcreteSubtypes() {
+                for (var extendedTypeInfo : extendedTypeInfoMap.values()) {
+                        var type = extendedTypeInfo.getType();
+                        if (!extendedTypeInfo.isAbstractType()) {
+                                extendedTypeInfo.getConcreteSubtypesAndSelf().add(type);
+                        }
+                        for (var supertype : extendedTypeInfo.getAllSupertypes()) {
+                                if (type.equals(supertype)) {
+                                        throw new IllegalArgumentException("%s cannot be a supertype of itself".formatted(type));
+                                }
+                                var supertypeInfo = extendedTypeInfoMap.get(supertype);
+                                supertypeInfo.getAllSubtypes().add(type);
+                                if (!extendedTypeInfo.isAbstractType()) {
+                                        supertypeInfo.getConcreteSubtypesAndSelf().add(type);
+                                }
+                        }
+                }
+        }
+
+        private void computeDirectSubtypes() {
+                for (var extendedTypeInfo : extendedTypeInfoMap.values()) {
+                        var allSubtypes = extendedTypeInfo.getAllSubtypes();
+                        var directSubtypes = new LinkedHashSet<>(allSubtypes);
+                        var indirectSubtypes = new LinkedHashSet<PartialRelation>(allSubtypes.size());
+                        for (var subtype : allSubtypes) {
+                                indirectSubtypes.addAll(extendedTypeInfoMap.get(subtype).getAllSubtypes());
+                        }
+                        directSubtypes.removeAll(indirectSubtypes);
+                        extendedTypeInfo.setDirectSubtypes(directSubtypes);
+                }
+        }
+
+        private void eliminateTrivialSupertypes() {
+                boolean changed;
+                do {
+                        var toRemove = new ArrayList<PartialRelation>();
+                        for (var entry : extendedTypeInfoMap.entrySet()) {
+                                var extendedTypeInfo = entry.getValue();
+                                boolean isAbstract = extendedTypeInfo.isAbstractType();
+                                // Do not eliminate abstract types with 0 subtypes, because they can be used para-consistently, i.e.,
+                                // an object determined to <b>must</b> have an abstract type with 0 subtypes <b>may not</b> ever exist.
+                                boolean hasSingleDirectSubtype = extendedTypeInfo.getDirectSubtypes().size() == 1;
+                                if (isAbstract && hasSingleDirectSubtype) {
+                                        toRemove.add(entry.getKey());
+                                }
+                        }
+                        toRemove.forEach(this::removeTrivialType);
+                        changed = !toRemove.isEmpty();
+                } while (changed);
+        }
+
+        private void removeTrivialType(PartialRelation trivialType) {
+                var extendedTypeInfo = extendedTypeInfoMap.get(trivialType);
+                var iterator = extendedTypeInfo.getDirectSubtypes().iterator();
+                if (!iterator.hasNext()) {
+                        throw new AssertionError("Expected trivial supertype %s to have a direct subtype"
+                                        .formatted(trivialType));
+                }
+                PartialRelation replacement = setReplacement(trivialType, iterator.next());
+                if (iterator.hasNext()) {
+                        throw new AssertionError("Expected trivial supertype %s to have at most 1 direct subtype"
+                                        .formatted(trivialType));
+                }
+                replacements.put(trivialType, replacement);
+                for (var supertype : extendedTypeInfo.getAllSupertypes()) {
+                        var extendedSupertypeInfo = extendedTypeInfoMap.get(supertype);
+                        if (!extendedSupertypeInfo.getAllSubtypes().remove(trivialType)) {
+                                throw new AssertionError("Expected %s to be subtype of %s".formatted(trivialType, supertype));
+                        }
+                        var directSubtypes = extendedSupertypeInfo.getDirectSubtypes();
+                        if (directSubtypes.remove(trivialType)) {
+                                directSubtypes.add(replacement);
+                        }
+                }
+                for (var subtype : extendedTypeInfo.getAllSubtypes()) {
+                        var extendedSubtypeInfo = extendedTypeInfoMap.get(subtype);
+                        if (!extendedSubtypeInfo.getAllSupertypes().remove(trivialType)) {
+                                throw new AssertionError("Expected %s to be supertype of %s".formatted(trivialType, subtype));
+                        }
+                }
+                extendedTypeInfoMap.remove(trivialType);
+        }
+
+        private PartialRelation setReplacement(PartialRelation trivialRelation, PartialRelation replacement) {
+                if (replacement == null) {
+                        return trivialRelation;
+                }
+                var resolved = setReplacement(replacement, replacements.get(replacement));
+                replacements.put(trivialRelation, resolved);
+                return resolved;
+        }
+
+        private Map<PartialRelation, TypeAnalysisResult> computeAnalysisResults() {
+                var allExtendedTypeInfoList = sortTypes();
+                var results = new LinkedHashMap<PartialRelation, TypeAnalysisResult>(
+                                allExtendedTypeInfoList.size() + replacements.size());
+                for (var extendedTypeInfo : allExtendedTypeInfoList) {
+                        var type = extendedTypeInfo.getType();
+                        results.put(type, new PreservedType(extendedTypeInfo, allExtendedTypeInfoList));
+                }
+                for (var entry : replacements.entrySet()) {
+                        var type = entry.getKey();
+                        results.put(type, new EliminatedType(entry.getValue()));
+                }
+                return Collections.unmodifiableMap(results);
+        }
+
+        private List<ExtendedTypeInfo> sortTypes() {
+                // Invert {@code directSubtypes} to keep track of the out-degree of types.
+                for (var extendedTypeInfo : extendedTypeInfoMap.values()) {
+                        for (var directSubtype : extendedTypeInfo.getDirectSubtypes()) {
+                                var extendedDirectSubtypeInfo = extendedTypeInfoMap.get(directSubtype);
+                                extendedDirectSubtypeInfo.getUnsortedDirectSupertypes().add(extendedTypeInfo.getType());
+                        }
+                }
+                // Build a <i>inverse</i> topological order ({@code extends} edges always points to earlier nodes in the order,
+                // breaking ties according to the original order ({@link ExtendedTypeInfo#index}) to form a 'stable' sort.
+                // See, e.g., https://stackoverflow.com/a/11236027.
+                var priorityQueue = new PriorityQueue<ExtendedTypeInfo>();
+                for (var extendedTypeInfo : extendedTypeInfoMap.values()) {
+                        if (extendedTypeInfo.getUnsortedDirectSupertypes().isEmpty()) {
+                                priorityQueue.add(extendedTypeInfo);
+                        }
+                }
+                var sorted = new ArrayList<ExtendedTypeInfo>(extendedTypeInfoMap.size());
+                while (!priorityQueue.isEmpty()) {
+                        var extendedTypeInfo = priorityQueue.remove();
+                        sorted.add(extendedTypeInfo);
+                        for (var directSubtype : extendedTypeInfo.getDirectSubtypes()) {
+                                var extendedDirectSubtypeInfo = extendedTypeInfoMap.get(directSubtype);
+                                var unsortedDirectSupertypes = extendedDirectSubtypeInfo.getUnsortedDirectSupertypes();
+                                if (!unsortedDirectSupertypes.remove(extendedTypeInfo.getType())) {
+                                        throw new AssertionError("Expected %s to be a direct supertype of %s"
+                                                        .formatted(extendedTypeInfo.getType(), directSubtype));
+                                }
+                                if (unsortedDirectSupertypes.isEmpty()) {
+                                        priorityQueue.add(extendedDirectSubtypeInfo);
+                                }
+                        }
+                }
+                return Collections.unmodifiableList(sorted);
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java
new file mode 100644
index 00000000..c800b4cd
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeHierarchyTranslationUnit.java
@@ -0,0 +1,52 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.reasoning.AnyPartialInterpretation;
+import tools.refinery.store.reasoning.literal.Modality;
+import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.reasoning.translator.Advice;
+import tools.refinery.store.reasoning.translator.TranslationUnit;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.representation.Symbol;
+
+import java.util.*;
+
+public class TypeHierarchyTranslationUnit extends TranslationUnit {
+        static final Symbol<InferredType> INFERRED_TYPE_SYMBOL = new Symbol<>("inferredType", 1,
+                        InferredType.class, InferredType.UNTYPED);
+
+        private final TypeAnalyzer typeAnalyzer;
+
+        public TypeHierarchyTranslationUnit(Map<PartialRelation, TypeInfo> typeInfoMap) {
+                typeAnalyzer = new TypeAnalyzer(typeInfoMap);
+        }
+
+        @Override
+        public Collection<AnyPartialSymbol> getTranslatedPartialSymbols() {
+                return null;
+        }
+
+        @Override
+        public void configure(Collection<Advice> advices) {
+
+        }
+
+        @Override
+        public List<Literal> call(CallPolarity polarity, Modality modality, PartialRelation target,
+                                                          List<Variable> arguments) {
+                return null;
+        }
+
+        @Override
+        public Map<AnyPartialSymbol, AnyPartialInterpretation> createPartialInterpretations(Model model) {
+                return null;
+        }
+
+        @Override
+        public void initializeModel(Model model, int nodeCount) {
+
+        }
+}
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
new file mode 100644
index 00000000..313df4df
--- /dev/null
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeInfo.java
@@ -0,0 +1,46 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+import java.util.*;
+
+public record TypeInfo(Collection<PartialRelation> supertypes, boolean abstractType) {
+        public static Builder builder() {
+                return new Builder();
+        }
+
+        public static class Builder {
+                private final Set<PartialRelation> supertypes = new LinkedHashSet<>();
+                private boolean abstractType;
+
+                private Builder() {
+                }
+
+                public Builder supertypes(Collection<PartialRelation> supertypes) {
+                        this.supertypes.addAll(supertypes);
+                        return this;
+                }
+
+                public Builder supertypes(PartialRelation... supertypes) {
+                        return supertypes(List.of(supertypes));
+                }
+
+                public Builder supertype(PartialRelation supertype) {
+                        supertypes.add(supertype);
+                        return this;
+                }
+
+                public Builder abstractType(boolean abstractType) {
+                        this.abstractType = abstractType;
+                        return this;
+                }
+
+                public Builder abstractType() {
+                        return abstractType(true);
+                }
+
+                public TypeInfo build() {
+                        return new TypeInfo(Collections.unmodifiableSet(supertypes), abstractType);
+                }
+        }
+}
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeTest.java
new file mode 100644
index 00000000..a8df2312
--- /dev/null
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/InferredTypeTest.java
@@ -0,0 +1,32 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+import java.util.Set;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+
+class InferredTypeTest {
+        private final PartialRelation c1 = new PartialRelation("C1", 1);
+        private final PartialRelation c2 = new PartialRelation("C2", 1);
+
+        @Test
+        void untypedIsConsistentTest() {
+                var sut = new InferredType(Set.of(), Set.of(c1, c2), null);
+                assertThat(sut.isConsistent(), is(true));
+        }
+
+        @Test
+        void typedIsConsistentTest() {
+                var sut = new InferredType(Set.of(c1), Set.of(c1, c2), c1);
+                assertThat(sut.isConsistent(), is(true));
+        }
+
+        @Test
+        void typedIsInconsistentTest() {
+                var sut = new InferredType(Set.of(c1), Set.of(), null);
+                assertThat(sut.isConsistent(), is(false));
+        }
+}
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
new file mode 100644
index 00000000..b2c1ef1b
--- /dev/null
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
@@ -0,0 +1,203 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.TruthValue;
+
+import java.util.LinkedHashMap;
+import java.util.Set;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+import static org.junit.jupiter.api.Assertions.assertAll;
+
+class TypeAnalyzerExampleHierarchyTest {
+        private final PartialRelation a1 = new PartialRelation("A1", 1);
+        private final PartialRelation a2 = new PartialRelation("A2", 1);
+        private final PartialRelation a3 = new PartialRelation("A3", 1);
+        private final PartialRelation a4 = new PartialRelation("A4", 1);
+        private final PartialRelation a5 = new PartialRelation("A5", 1);
+        private final PartialRelation c1 = new PartialRelation("C1", 1);
+        private final PartialRelation c2 = new PartialRelation("C2", 1);
+        private final PartialRelation c3 = new PartialRelation("C3", 1);
+        private final PartialRelation c4 = new PartialRelation("C4", 1);
+
+        private TypeAnalyzer sut;
+        private TypeAnalyzerTester tester;
+
+        @BeforeEach
+        void beforeEach() {
+                var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>();
+                typeInfoMap.put(a1, TypeInfo.builder().abstractType().build());
+                typeInfoMap.put(a2, TypeInfo.builder().abstractType().build());
+                typeInfoMap.put(a3, TypeInfo.builder().abstractType().build());
+                typeInfoMap.put(a4, TypeInfo.builder().abstractType().build());
+                typeInfoMap.put(a5, TypeInfo.builder().abstractType().build());
+                typeInfoMap.put(c1, TypeInfo.builder().supertypes(a1, a4).build());
+                typeInfoMap.put(c2, TypeInfo.builder().supertypes(a1, a2, a3, a4).build());
+                typeInfoMap.put(c3, TypeInfo.builder().supertype(a3).build());
+                typeInfoMap.put(c4, TypeInfo.builder().supertype(a4).build());
+                sut = new TypeAnalyzer(typeInfoMap);
+                tester = new TypeAnalyzerTester(sut);
+        }
+
+        @Test
+        void analysisResultsTest() {
+                assertAll(
+                                () -> tester.assertAbstractType(a1, c1, c2),
+                                () -> tester.assertEliminatedType(a2, c2),
+                                () -> tester.assertAbstractType(a3, c2, c3),
+                                () -> tester.assertAbstractType(a4, c1, c2, c4),
+                                () -> tester.assertVacuousType(a5),
+                                () -> tester.assertConcreteType(c1),
+                                () -> tester.assertConcreteType(c2),
+                                () -> tester.assertConcreteType(c3),
+                                () -> tester.assertConcreteType(c4)
+                );
+        }
+
+        @Test
+        void inferredTypesTest() {
+                assertAll(
+                                () -> assertThat(sut.getUnknownType(), is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))),
+                                () -> assertThat(tester.getInferredType(a1), is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))),
+                                () -> assertThat(tester.getInferredType(a3), is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))),
+                                () -> assertThat(tester.getInferredType(a4), is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))),
+                                () -> assertThat(tester.getInferredType(a5), is(new InferredType(Set.of(a5), Set.of(), null))),
+                                () -> assertThat(tester.getInferredType(c1), is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
+                                () -> assertThat(tester.getInferredType(c2),
+                                                is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))),
+                                () -> assertThat(tester.getInferredType(c3), is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
+                                () -> assertThat(tester.getInferredType(c4), is(new InferredType(Set.of(a4, c4), Set.of(c4), c4)))
+                );
+        }
+
+        @Test
+        void consistentMustTest() {
+                var a1Result = tester.getPreservedType(a1);
+                var a3Result = tester.getPreservedType(a3);
+                var expected = new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2);
+                assertAll(
+                                () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), is(expected)),
+                                () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), is(expected)),
+                                () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a1Result.asInferredType())),
+                                () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a3Result.asInferredType())),
+                                () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.TRUE),
+                                                is(a1Result.asInferredType()))
+                );
+        }
+
+        @Test
+        void consistentMayNotTest() {
+                var a1Result = tester.getPreservedType(a1);
+                var a3Result = tester.getPreservedType(a3);
+                var a4Result = tester.getPreservedType(a4);
+                assertAll(
+                                () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.FALSE),
+                                                is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
+                                () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
+                                                is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
+                                () -> assertThat(a4Result.merge(a3Result.asInferredType(), TruthValue.FALSE),
+                                                is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
+                                () -> assertThat(a3Result.merge(a4Result.asInferredType(), TruthValue.FALSE),
+                                                is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))),
+                                () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.FALSE),
+                                                is(new InferredType(Set.of(), Set.of(c3, c4), null))),
+                                () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.FALSE),
+                                                is(new InferredType(Set.of(), Set.of(c1, c4), null))),
+                                () -> assertThat(a4Result.merge(sut.getUnknownType(), TruthValue.FALSE),
+                                                is(new InferredType(Set.of(), Set.of(c3), null)))
+                );
+        }
+
+        @Test
+        void consistentErrorTest() {
+                var c1Result = tester.getPreservedType(c1);
+                var a4Result = tester.getPreservedType(a4);
+                var expected = new InferredType(Set.of(c1, a1, a4), Set.of(), null);
+                assertAll(
+                                () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), is(expected)),
+                                () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), is(expected))
+                );
+        }
+
+        @Test
+        void consistentUnknownTest() {
+                var c1Result = tester.getPreservedType(c1);
+                var a4Result = tester.getPreservedType(a4);
+                assertAll(
+                                () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.UNKNOWN),
+                                                is(a4Result.asInferredType())),
+                                () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.UNKNOWN),
+                                                is(c1Result.asInferredType()))
+                );
+        }
+
+        @Test
+        void inconsistentMustTest() {
+                var a1Result = tester.getPreservedType(a1);
+                var c3Result = tester.getPreservedType(c3);
+                assertAll(
+                                () -> assertThat(a1Result.merge(c3Result.asInferredType(), TruthValue.TRUE),
+                                                is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))),
+                                () -> assertThat(c3Result.merge(a1Result.asInferredType(), TruthValue.TRUE),
+                                                is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null)))
+                );
+        }
+
+        @Test
+        void inconsistentMayNotTest() {
+                var a1Result = tester.getPreservedType(a1);
+                var a4Result = tester.getPreservedType(a4);
+                var c1Result = tester.getPreservedType(c1);
+                assertAll(
+                                () -> assertThat(a4Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
+                                                is(new InferredType(Set.of(a1, a4), Set.of(), null))),
+                                () -> assertThat(a1Result.merge(c1Result.asInferredType(), TruthValue.FALSE),
+                                                is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
+                                () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.FALSE),
+                                                is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
+                                () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
+                                                is(new InferredType(Set.of(a1, a4), Set.of(), null)))
+                );
+        }
+
+        @Test
+        void vacuousMustTest() {
+                var c1Result = tester.getPreservedType(c1);
+                var a5Result = tester.getPreservedType(a5);
+                assertAll(
+                                () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.TRUE),
+                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
+                                () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.TRUE),
+                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null)))
+                );
+        }
+
+        @Test
+        void vacuousMayNotTest() {
+                var c1Result = tester.getPreservedType(c1);
+                var a5Result = tester.getPreservedType(a5);
+                assertAll(
+                                () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.FALSE),
+                                                is(a5Result.asInferredType())),
+                                () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.FALSE),
+                                                is(c1Result.asInferredType()))
+                );
+        }
+
+        @Test
+        void vacuousErrorTest() {
+                var c1Result = tester.getPreservedType(c1);
+                var a5Result = tester.getPreservedType(a5);
+                assertAll(
+                                () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.ERROR),
+                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
+                                () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.ERROR),
+                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
+                                () -> assertThat(a5Result.merge(a5Result.asInferredType(), TruthValue.ERROR),
+                                                is(a5Result.asInferredType()))
+                );
+        }
+}
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java
new file mode 100644
index 00000000..b7b69ed8
--- /dev/null
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTest.java
@@ -0,0 +1,200 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.reasoning.representation.PartialRelation;
+import tools.refinery.store.representation.TruthValue;
+
+import java.util.LinkedHashMap;
+import java.util.Set;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+import static org.junit.jupiter.api.Assertions.assertAll;
+import static org.junit.jupiter.api.Assertions.assertThrows;
+
+class TypeAnalyzerTest {
+        @Test
+        void directSupertypesTest() {
+                var c1 = new PartialRelation("C1", 1);
+                var c2 = new PartialRelation("C2", 1);
+                var c3 = new PartialRelation("C3", 1);
+                var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>();
+                typeInfoMap.put(c1, TypeInfo.builder().supertypes(c2, c3).build());
+                typeInfoMap.put(c2, TypeInfo.builder().supertype(c3).build());
+                typeInfoMap.put(c3, TypeInfo.builder().build());
+
+                var sut = new TypeAnalyzer(typeInfoMap);
+                var tester = new TypeAnalyzerTester(sut);
+
+                assertAll(
+                                () -> tester.assertConcreteType(c1),
+                                () -> tester.assertConcreteType(c2, c1),
+                                () -> tester.assertConcreteType(c3, c2)
+                );
+        }
+
+        @Test
+        void typeEliminationAbstractToConcreteTest() {
+                var c1 = new PartialRelation("C1", 1);
+                var c2 = new PartialRelation("C2", 1);
+                var a11 = new PartialRelation("A11", 1);
+                var a12 = new PartialRelation("A12", 1);
+                var a21 = new PartialRelation("A21", 1);
+                var a22 = new PartialRelation("A22", 1);
+                var a3 = new PartialRelation("A3", 1);
+                var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>();
+                typeInfoMap.put(a3, TypeInfo.builder().abstractType().build());
+                typeInfoMap.put(a21, TypeInfo.builder().abstractType().supertype(a3).build());
+                typeInfoMap.put(a22, TypeInfo.builder().abstractType().supertype(a3).build());
+                typeInfoMap.put(a11, TypeInfo.builder().abstractType().supertypes(a21, a22).build());
+                typeInfoMap.put(a12, TypeInfo.builder().abstractType().supertypes(a21, a22).build());
+                typeInfoMap.put(c1, TypeInfo.builder().supertypes(a11, a12).build());
+                typeInfoMap.put(c2, TypeInfo.builder().supertype(a3).build());
+
+                var sut = new TypeAnalyzer(typeInfoMap);
+                var tester = new TypeAnalyzerTester(sut);
+
+                assertAll(
+                                () -> tester.assertConcreteType(c1),
+                                () -> tester.assertConcreteType(c2),
+                                () -> tester.assertEliminatedType(a11, c1),
+                                () -> tester.assertEliminatedType(a12, c1),
+                                () -> tester.assertEliminatedType(a21, c1),
+                                () -> tester.assertEliminatedType(a22, c1),
+                                () -> tester.assertAbstractType(a3, c1, c2)
+                );
+        }
+
+        @Test
+        void typeEliminationConcreteToAbstractTest() {
+                var c1 = new PartialRelation("C1", 1);
+                var c2 = new PartialRelation("C2", 1);
+                var a11 = new PartialRelation("A11", 1);
+                var a12 = new PartialRelation("A12", 1);
+                var a21 = new PartialRelation("A21", 1);
+                var a22 = new PartialRelation("A22", 1);
+                var a3 = new PartialRelation("A3", 1);
+                var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>();
+                typeInfoMap.put(c1, TypeInfo.builder().supertypes(a11, a12).build());
+                typeInfoMap.put(c2, TypeInfo.builder().supertype(a3).build());
+                typeInfoMap.put(a11, TypeInfo.builder().abstractType().supertypes(a21, a22).build());
+                typeInfoMap.put(a12, TypeInfo.builder().abstractType().supertypes(a21, a22).build());
+                typeInfoMap.put(a21, TypeInfo.builder().abstractType().supertype(a3).build());
+                typeInfoMap.put(a22, TypeInfo.builder().abstractType().supertype(a3).build());
+                typeInfoMap.put(a3, TypeInfo.builder().abstractType().build());
+
+                var sut = new TypeAnalyzer(typeInfoMap);
+                var tester = new TypeAnalyzerTester(sut);
+
+                assertAll(
+                                () -> tester.assertConcreteType(c1),
+                                () -> tester.assertConcreteType(c2),
+                                () -> tester.assertEliminatedType(a11, c1),
+                                () -> tester.assertEliminatedType(a12, c1),
+                                () -> tester.assertEliminatedType(a21, c1),
+                                () -> tester.assertEliminatedType(a22, c1),
+                                () -> tester.assertAbstractType(a3, c1, c2)
+                );
+        }
+
+        @Test
+        void preserveConcreteTypeTest() {
+                var c1 = new PartialRelation("C1", 1);
+                var a1 = new PartialRelation("A1", 1);
+                var c2 = new PartialRelation("C2", 1);
+                var a2 = new PartialRelation("A2", 1);
+                var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>();
+                typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build());
+                typeInfoMap.put(a1, TypeInfo.builder().abstractType().supertype(c2).build());
+                typeInfoMap.put(c2, TypeInfo.builder().supertype(a2).build());
+                typeInfoMap.put(a2, TypeInfo.builder().abstractType().build());
+
+                var sut = new TypeAnalyzer(typeInfoMap);
+                var tester = new TypeAnalyzerTester(sut);
+
+                assertAll(
+                                () -> tester.assertConcreteType(c1),
+                                () -> tester.assertEliminatedType(a1, c1),
+                                () -> tester.assertConcreteType(c2, c1),
+                                () -> tester.assertEliminatedType(a2, c2)
+                );
+        }
+
+        @Test
+        void mostGeneralCurrentTypeTest() {
+                var c1 = new PartialRelation("C1", 1);
+                var c2 = new PartialRelation("C2", 1);
+                var c3 = new PartialRelation("C3", 1);
+                var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>();
+                typeInfoMap.put(c1, TypeInfo.builder().supertype(c3).build());
+                typeInfoMap.put(c2, TypeInfo.builder().supertype(c3).build());
+                typeInfoMap.put(c3, TypeInfo.builder().build());
+
+                var sut = new TypeAnalyzer(typeInfoMap);
+                var tester = new TypeAnalyzerTester(sut);
+                var c3Result = tester.getPreservedType(c3);
+
+                var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3);
+                assertAll(
+                                () -> assertThat(tester.getInferredType(c3), is(expected)),
+                                () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(expected))
+                );
+        }
+
+        @Test
+        void preferFirstConcreteTypeTest() {
+                var a1 = new PartialRelation("A1", 1);
+                var c1 = new PartialRelation("C1", 1);
+                var c2 = new PartialRelation("C2", 1);
+                var c3 = new PartialRelation("C3", 1);
+                var c4 = new PartialRelation("C4", 1);
+                var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>();
+                typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build());
+                typeInfoMap.put(c2, TypeInfo.builder().supertype(a1).build());
+                typeInfoMap.put(c3, TypeInfo.builder().supertype(a1).build());
+                typeInfoMap.put(c4, TypeInfo.builder().supertype(c3).build());
+                typeInfoMap.put(a1, TypeInfo.builder().abstractType().build());
+
+                var sut = new TypeAnalyzer(typeInfoMap);
+                var tester = new TypeAnalyzerTester(sut);
+                var c1Result = tester.getPreservedType(c1);
+                var a1Result = tester.getPreservedType(a1);
+
+                assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
+                                is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2)));
+        }
+
+        @Test
+        void preferFirstMostGeneralConcreteTypeTest() {
+                var a1 = new PartialRelation("A1", 1);
+                var c1 = new PartialRelation("C1", 1);
+                var c2 = new PartialRelation("C2", 1);
+                var c3 = new PartialRelation("C3", 1);
+                var c4 = new PartialRelation("C4", 1);
+                var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>();
+                typeInfoMap.put(c4, TypeInfo.builder().supertype(c3).build());
+                typeInfoMap.put(c3, TypeInfo.builder().supertype(a1).build());
+                typeInfoMap.put(c2, TypeInfo.builder().supertype(a1).build());
+                typeInfoMap.put(c1, TypeInfo.builder().supertype(a1).build());
+                typeInfoMap.put(a1, TypeInfo.builder().abstractType().build());
+
+                var sut = new TypeAnalyzer(typeInfoMap);
+                var tester = new TypeAnalyzerTester(sut);
+                var c1Result = tester.getPreservedType(c1);
+                var a1Result = tester.getPreservedType(a1);
+
+                assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
+                                is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3)));
+        }
+
+        @Test
+        void circularTypeHierarchyTest() {
+                var c1 = new PartialRelation("C1", 1);
+                var c2 = new PartialRelation("C2", 1);
+                var typeInfoMap = new LinkedHashMap<PartialRelation, TypeInfo>();
+                typeInfoMap.put(c1, TypeInfo.builder().supertype(c2).build());
+                typeInfoMap.put(c2, TypeInfo.builder().supertype(c1).build());
+
+                assertThrows(IllegalArgumentException.class, () -> new TypeAnalyzer(typeInfoMap));
+        }
+}
diff --git a/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTester.java b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTester.java
new file mode 100644
index 00000000..56407730
--- /dev/null
+++ b/subprojects/store-reasoning/src/test/java/tools/refinery/store/reasoning/translator/typehierarchy/TypeAnalyzerTester.java
@@ -0,0 +1,51 @@
+package tools.refinery.store.reasoning.translator.typehierarchy;
+
+import tools.refinery.store.reasoning.representation.PartialRelation;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.*;
+import static org.hamcrest.Matchers.is;
+
+class TypeAnalyzerTester {
+        private final TypeAnalyzer sut;
+
+        public TypeAnalyzerTester(TypeAnalyzer sut) {
+                this.sut = sut;
+        }
+
+        public void assertAbstractType(PartialRelation partialRelation, PartialRelation... directSubtypes) {
+                assertPreservedType(partialRelation, true, false, directSubtypes);
+        }
+
+        public void assertVacuousType(PartialRelation partialRelation) {
+                assertPreservedType(partialRelation, true, true);
+        }
+
+        public void assertConcreteType(PartialRelation partialRelation, PartialRelation... directSubtypes) {
+                assertPreservedType(partialRelation, false, false, directSubtypes);
+        }
+
+        private void assertPreservedType(PartialRelation partialRelation, boolean isAbstract, boolean isVacuous,
+                                                                         PartialRelation... directSubtypes) {
+                var result = sut.getAnalysisResults().get(partialRelation);
+                assertThat(result, is(instanceOf(PreservedType.class)));
+                var preservedResult = (PreservedType) result;
+                assertThat(preservedResult.isAbstractType(), is(isAbstract));
+                assertThat(preservedResult.isVacuous(), is(isVacuous));
+                assertThat(preservedResult.getDirectSubtypes(), hasItems(directSubtypes));
+        }
+
+        public void assertEliminatedType(PartialRelation partialRelation, PartialRelation replacement) {
+                var result = sut.getAnalysisResults().get(partialRelation);
+                assertThat(result, is(instanceOf(EliminatedType.class)));
+                assertThat(((EliminatedType) result).replacement(), is(replacement));
+        }
+
+        public PreservedType getPreservedType(PartialRelation partialRelation) {
+                return (PreservedType) sut.getAnalysisResults().get(partialRelation);
+        }
+
+        public InferredType getInferredType(PartialRelation partialRelation) {
+                return getPreservedType(partialRelation).asInferredType();
+        }
+}