42 files changed, 1674 insertions, 0 deletions

diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/AnyPartialSymbolInterpretation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/AnyPartialSymbolInterpretation.java
new file mode 100644
index 00000000..b6b1f2be
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/AnyPartialSymbolInterpretation.java
@@ -0,0 +1,13 @@
+package tools.refinery.store.partial;
+
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+
+public sealed interface AnyPartialSymbolInterpretation permits PartialSymbolInterpretation {
+        PartialInterpretationAdapter getAdapter();
+
+        AnyPartialSymbol getPartialSymbol();
+
+        int countUnfinished();
+
+        int countErrors();
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/MergeResult.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/MergeResult.java
new file mode 100644
index 00000000..82414d87
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/MergeResult.java
@@ -0,0 +1,15 @@
+package tools.refinery.store.partial;
+
+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-partial/src/main/java/tools/refinery/store/partial/PartialInterpretation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretation.java
new file mode 100644
index 00000000..d76f8728
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretation.java
@@ -0,0 +1,24 @@
+package tools.refinery.store.partial;
+
+import tools.refinery.store.partial.internal.PartialInterpretationBuilderImpl;
+import tools.refinery.store.adapter.ModelAdapterBuilderFactory;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.partial.representation.PartialRelation;
+
+public final class PartialInterpretation extends ModelAdapterBuilderFactory<PartialInterpretationAdapter,
+                PartialInterpretationStoreAdapter, PartialInterpretationBuilder> {
+        public static final PartialInterpretation ADAPTER = new PartialInterpretation();
+
+        public static final PartialRelation EXISTS = new PartialRelation("exists", 1);
+
+        public static final PartialRelation EQUALS = new PartialRelation("equals", 1);
+
+        private PartialInterpretation() {
+                super(PartialInterpretationAdapter.class, PartialInterpretationStoreAdapter.class, PartialInterpretationBuilder.class);
+        }
+
+        @Override
+        public PartialInterpretationBuilder createBuilder(ModelStoreBuilder storeBuilder) {
+                return new PartialInterpretationBuilderImpl(storeBuilder);
+        }
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java
new file mode 100644
index 00000000..b811ae7a
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationAdapter.java
@@ -0,0 +1,20 @@
+package tools.refinery.store.partial;
+
+import tools.refinery.store.adapter.ModelAdapter;
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+import tools.refinery.store.partial.representation.PartialSymbol;
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.ResultSet;
+
+public interface PartialInterpretationAdapter extends ModelAdapter {
+        @Override
+        PartialInterpretationStoreAdapter getStoreAdapter();
+
+        default AnyPartialSymbolInterpretation getPartialInterpretation(AnyPartialSymbol partialSymbol) {
+                return getPartialInterpretation((PartialSymbol<?, ?>) partialSymbol);
+        }
+
+        <A, C> PartialSymbolInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol);
+
+        ResultSet getLiftedResultSet(Dnf query);
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java
new file mode 100644
index 00000000..db042466
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationBuilder.java
@@ -0,0 +1,28 @@
+package tools.refinery.store.partial;
+
+import tools.refinery.store.adapter.ModelAdapterBuilder;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.partial.literal.Modality;
+
+import java.util.Collection;
+import java.util.List;
+
+@SuppressWarnings("UnusedReturnValue")
+public interface PartialInterpretationBuilder extends ModelAdapterBuilder {
+        default PartialInterpretationBuilder liftedQueries(Dnf... liftedQueries) {
+                return liftedQueries(List.of(liftedQueries));
+        }
+
+        default PartialInterpretationBuilder liftedQueries(Collection<Dnf> liftedQueries) {
+                liftedQueries.forEach(this::liftedQuery);
+                return this;
+        }
+
+        PartialInterpretationBuilder liftedQuery(Dnf liftedQuery);
+
+        Dnf lift(Modality modality, Dnf query);
+
+        @Override
+        PartialInterpretationStoreAdapter createStoreAdapter(ModelStore store);
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java
new file mode 100644
index 00000000..a1813671
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialInterpretationStoreAdapter.java
@@ -0,0 +1,17 @@
+package tools.refinery.store.partial;
+
+import tools.refinery.store.adapter.ModelStoreAdapter;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+import tools.refinery.store.query.Dnf;
+
+import java.util.Collection;
+
+public interface PartialInterpretationStoreAdapter extends ModelStoreAdapter {
+        Collection<AnyPartialSymbol> getPartialSymbols();
+
+        Collection<Dnf> getLiftedQueries();
+
+        @Override
+        PartialInterpretationAdapter createModelAdapter(Model model);
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialSymbolInterpretation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialSymbolInterpretation.java
new file mode 100644
index 00000000..fa9e9216
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/PartialSymbolInterpretation.java
@@ -0,0 +1,22 @@
+package tools.refinery.store.partial;
+
+import tools.refinery.store.partial.representation.PartialSymbol;
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.tuple.Tuple;
+
+public non-sealed interface PartialSymbolInterpretation<A, C> extends AnyPartialSymbolInterpretation {
+        @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-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java
new file mode 100644
index 00000000..c482d8a2
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationAdapterImpl.java
@@ -0,0 +1,38 @@
+package tools.refinery.store.partial.internal;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.partial.PartialInterpretationAdapter;
+import tools.refinery.store.partial.PartialSymbolInterpretation;
+import tools.refinery.store.partial.representation.PartialSymbol;
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.ResultSet;
+
+public class PartialInterpretationAdapterImpl implements PartialInterpretationAdapter {
+        private final Model model;
+        private final PartialInterpretationStoreAdapterImpl storeAdapter;
+
+        PartialInterpretationAdapterImpl(Model model, PartialInterpretationStoreAdapterImpl storeAdapter) {
+                this.model = model;
+                this.storeAdapter = storeAdapter;
+        }
+
+        @Override
+        public Model getModel() {
+                return model;
+        }
+
+        @Override
+        public PartialInterpretationStoreAdapterImpl getStoreAdapter() {
+                return storeAdapter;
+        }
+
+        @Override
+        public <A, C> PartialSymbolInterpretation<A, C> getPartialInterpretation(PartialSymbol<A, C> partialSymbol) {
+                return null;
+        }
+
+        @Override
+        public ResultSet getLiftedResultSet(Dnf query) {
+                return null;
+        }
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java
new file mode 100644
index 00000000..5853aeaf
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationBuilderImpl.java
@@ -0,0 +1,29 @@
+package tools.refinery.store.partial.internal;
+
+import tools.refinery.store.adapter.AbstractModelAdapterBuilder;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.partial.PartialInterpretationBuilder;
+import tools.refinery.store.partial.literal.Modality;
+import tools.refinery.store.query.Dnf;
+
+public class PartialInterpretationBuilderImpl extends AbstractModelAdapterBuilder implements PartialInterpretationBuilder {
+        public PartialInterpretationBuilderImpl(ModelStoreBuilder storeBuilder) {
+                super(storeBuilder);
+        }
+
+        @Override
+        public PartialInterpretationBuilder liftedQuery(Dnf liftedQuery) {
+                return null;
+        }
+
+        @Override
+        public Dnf lift(Modality modality, Dnf query) {
+                return null;
+        }
+
+        @Override
+        public PartialInterpretationStoreAdapterImpl createStoreAdapter(ModelStore store) {
+                return null;
+        }
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java
new file mode 100644
index 00000000..0486af6e
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/internal/PartialInterpretationStoreAdapterImpl.java
@@ -0,0 +1,37 @@
+package tools.refinery.store.partial.internal;
+
+import tools.refinery.store.partial.PartialInterpretationStoreAdapter;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+import tools.refinery.store.query.Dnf;
+
+import java.util.Collection;
+
+public class PartialInterpretationStoreAdapterImpl implements PartialInterpretationStoreAdapter {
+        private final ModelStore store;
+
+        PartialInterpretationStoreAdapterImpl(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 PartialInterpretationAdapterImpl createModelAdapter(Model model) {
+                return new PartialInterpretationAdapterImpl(model, this);
+        }
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/DnfLifter.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/DnfLifter.java
new file mode 100644
index 00000000..1c35b925
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/DnfLifter.java
@@ -0,0 +1,107 @@
+package tools.refinery.store.partial.lifting;
+
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.partial.literal.ModalDnfCallLiteral;
+import tools.refinery.store.partial.PartialInterpretation;
+import tools.refinery.store.partial.literal.ModalRelationLiteral;
+import tools.refinery.store.partial.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.partial.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(PartialInterpretation.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(PartialInterpretation.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-partial/src/main/java/tools/refinery/store/partial/lifting/ModalDnf.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/ModalDnf.java
new file mode 100644
index 00000000..6fe54ad9
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/lifting/ModalDnf.java
@@ -0,0 +1,11 @@
+package tools.refinery.store.partial.lifting;
+
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
new file mode 100644
index 00000000..a49e0625
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
@@ -0,0 +1,37 @@
+package tools.refinery.store.partial.literal;
+
+import tools.refinery.store.query.Dnf;
+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.LiteralReduction;
+import tools.refinery.store.query.literal.PolarLiteral;
+
+import java.util.List;
+import java.util.Map;
+
+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 ModalDnfCallLiteral substitute(Map<Variable, Variable> 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-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
new file mode 100644
index 00000000..a1b6c83e
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
@@ -0,0 +1,45 @@
+package tools.refinery.store.partial.literal;
+
+import tools.refinery.store.query.RelationLike;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallLiteral;
+import tools.refinery.store.query.literal.CallPolarity;
+
+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 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-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
new file mode 100644
index 00000000..dbaa524f
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
@@ -0,0 +1,31 @@
+package tools.refinery.store.partial.literal;
+
+import tools.refinery.store.partial.representation.PartialRelation;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.PolarLiteral;
+
+import java.util.List;
+import java.util.Map;
+
+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 ModalRelationLiteral substitute(Map<Variable, Variable> 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-partial/src/main/java/tools/refinery/store/partial/literal/Modality.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/Modality.java
new file mode 100644
index 00000000..d647ef0a
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/Modality.java
@@ -0,0 +1,31 @@
+package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java
new file mode 100644
index 00000000..51d388d3
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialLiterals.java
@@ -0,0 +1,33 @@
+package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
new file mode 100644
index 00000000..dc1a1da3
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
@@ -0,0 +1,27 @@
+package tools.refinery.store.partial.literal;
+
+import tools.refinery.store.partial.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 java.util.List;
+import java.util.Map;
+
+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 PartialRelationLiteral substitute(Map<Variable, Variable> substitution) {
+                return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
+        }
+
+        @Override
+        public PartialRelationLiteral negate() {
+                return new PartialRelationLiteral(getPolarity().negate(), getTarget(), getArguments());
+        }
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java
new file mode 100644
index 00000000..1113245e
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialFunction.java
@@ -0,0 +1,4 @@
+package tools.refinery.store.partial.representation;
+
+public sealed interface AnyPartialFunction extends AnyPartialSymbol permits PartialFunction {
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java
new file mode 100644
index 00000000..25096e74
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/AnyPartialSymbol.java
@@ -0,0 +1,11 @@
+package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java
new file mode 100644
index 00000000..3c186f6f
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialFunction.java
@@ -0,0 +1,32 @@
+package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java
new file mode 100644
index 00000000..51c2f28d
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialRelation.java
@@ -0,0 +1,66 @@
+package tools.refinery.store.partial.representation;
+
+import tools.refinery.store.partial.literal.Modality;
+import tools.refinery.store.partial.literal.PartialRelationLiteral;
+import tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java
new file mode 100644
index 00000000..38533fa9
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/representation/PartialSymbol.java
@@ -0,0 +1,12 @@
+package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/rule/RelationRefinementAction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RelationRefinementAction.java
new file mode 100644
index 00000000..6c89653d
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RelationRefinementAction.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.partial.rule;
+
+import tools.refinery.store.partial.PartialInterpretation;
+import tools.refinery.store.partial.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(PartialInterpretation.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-partial/src/main/java/tools/refinery/store/partial/rule/Rule.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/Rule.java
new file mode 100644
index 00000000..c114b8cf
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/Rule.java
@@ -0,0 +1,38 @@
+package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/rule/RuleAction.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleAction.java
new file mode 100644
index 00000000..7a8ede40
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleAction.java
@@ -0,0 +1,12 @@
+package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/rule/RuleActionExecutor.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleActionExecutor.java
new file mode 100644
index 00000000..1c2db5f1
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleActionExecutor.java
@@ -0,0 +1,9 @@
+package tools.refinery.store.partial.rule;
+
+import tools.refinery.store.partial.MergeResult;
+import tools.refinery.store.tuple.TupleLike;
+
+@FunctionalInterface
+public interface RuleActionExecutor {
+        MergeResult execute(TupleLike activationTuple);
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleExecutor.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleExecutor.java
new file mode 100644
index 00000000..41d79306
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/rule/RuleExecutor.java
@@ -0,0 +1,34 @@
+package tools.refinery.store.partial.rule;
+
+import tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/Advice.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Advice.java
new file mode 100644
index 00000000..65040a8e
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Advice.java
@@ -0,0 +1,155 @@
+package tools.refinery.store.partial.translator;
+
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+import tools.refinery.store.partial.representation.PartialRelation;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.literal.Literal;
+
+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 substitution = new HashMap<Variable, Variable>(arity);
+                for (int i = 0; i < arity; i++) {
+                        substitution.put(parameters.get(i), substituteParameters.get(i));
+                }
+                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-partial/src/main/java/tools/refinery/store/partial/translator/AdviceSlot.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/AdviceSlot.java
new file mode 100644
index 00000000..3702a8ac
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/AdviceSlot.java
@@ -0,0 +1,25 @@
+package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/Seed.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Seed.java
new file mode 100644
index 00000000..c56b06ed
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/Seed.java
@@ -0,0 +1,12 @@
+package tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/TranslationUnit.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/TranslationUnit.java
new file mode 100644
index 00000000..26bd909b
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/TranslationUnit.java
@@ -0,0 +1,48 @@
+package tools.refinery.store.partial.translator;
+
+import tools.refinery.store.partial.PartialInterpretationBuilder;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.model.ModelStoreBuilder;
+import tools.refinery.store.partial.AnyPartialSymbolInterpretation;
+import tools.refinery.store.partial.literal.Modality;
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+import tools.refinery.store.partial.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 PartialInterpretationBuilder partialInterpretationBuilder;
+
+        protected PartialInterpretationBuilder getPartialInterpretationBuilder() {
+                return partialInterpretationBuilder;
+        }
+
+        public void setPartialInterpretationBuilder(PartialInterpretationBuilder partialInterpretationBuilder) {
+                this.partialInterpretationBuilder = partialInterpretationBuilder;
+        }
+
+        protected ModelStoreBuilder getModelStoreBuilder() {
+                return partialInterpretationBuilder.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, AnyPartialSymbolInterpretation> createPartialInterpretations(Model model);
+
+        public abstract void initializeModel(Model model, int nodeCount);
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java
new file mode 100644
index 00000000..9adf6bc8
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/EliminatedType.java
@@ -0,0 +1,6 @@
+package tools.refinery.store.partial.translator.typehierarchy;
+
+import tools.refinery.store.partial.representation.PartialRelation;
+
+record EliminatedType(PartialRelation replacement) implements TypeAnalysisResult {
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java
new file mode 100644
index 00000000..d3f66a4c
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/ExtendedTypeInfo.java
@@ -0,0 +1,101 @@
+package tools.refinery.store.partial.translator.typehierarchy;
+
+import org.jetbrains.annotations.NotNull;
+import tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMayTypeRelationView.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMayTypeRelationView.java
new file mode 100644
index 00000000..ff761936
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMayTypeRelationView.java
@@ -0,0 +1,19 @@
+package tools.refinery.store.partial.translator.typehierarchy;
+
+import tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMustTypeRelationView.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMustTypeRelationView.java
new file mode 100644
index 00000000..4eca0a1c
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredMustTypeRelationView.java
@@ -0,0 +1,19 @@
+package tools.refinery.store.partial.translator.typehierarchy;
+
+import tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java
new file mode 100644
index 00000000..729b1fb5
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/InferredType.java
@@ -0,0 +1,30 @@
+package tools.refinery.store.partial.translator.typehierarchy;
+
+import tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java
new file mode 100644
index 00000000..0299ae03
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/PreservedType.java
@@ -0,0 +1,136 @@
+package tools.refinery.store.partial.translator.typehierarchy;
+
+import tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java
new file mode 100644
index 00000000..0745f84e
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalysisResult.java
@@ -0,0 +1,4 @@
+package tools.refinery.store.partial.translator.typehierarchy;
+
+sealed interface TypeAnalysisResult permits EliminatedType, PreservedType {
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java
new file mode 100644
index 00000000..062b4c49
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzer.java
@@ -0,0 +1,202 @@
+package tools.refinery.store.partial.translator.typehierarchy;
+
+import tools.refinery.store.partial.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-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeHierarchyTranslationUnit.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeHierarchyTranslationUnit.java
new file mode 100644
index 00000000..7f438f71
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeHierarchyTranslationUnit.java
@@ -0,0 +1,52 @@
+package tools.refinery.store.partial.translator.typehierarchy;
+
+import tools.refinery.store.partial.AnyPartialSymbolInterpretation;
+import tools.refinery.store.partial.literal.Modality;
+import tools.refinery.store.partial.representation.AnyPartialSymbol;
+import tools.refinery.store.partial.representation.PartialRelation;
+import tools.refinery.store.partial.translator.Advice;
+import tools.refinery.store.partial.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 Map<PartialRelation, TypeInfo> typeInfoMap;
+
+        public TypeHierarchyTranslationUnit(Map<PartialRelation, TypeInfo> typeInfoMap) {
+                this.typeInfoMap = new LinkedHashMap<>(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, AnyPartialSymbolInterpretation> createPartialInterpretations(Model model) {
+                return null;
+        }
+
+        @Override
+        public void initializeModel(Model model, int nodeCount) {
+
+        }
+}
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java
new file mode 100644
index 00000000..1b0922fe
--- /dev/null
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/translator/typehierarchy/TypeInfo.java
@@ -0,0 +1,46 @@
+package tools.refinery.store.partial.translator.typehierarchy;
+
+import tools.refinery.store.partial.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);
+                }
+        }
+}