Merge pull request #24 from kris7t/partial-interpretation

Changes for supporting partial interpretation

105 files changed, 4684 insertions, 0 deletions

diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/AnyResultSet.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/AnyResultSet.java
new file mode 100644
index 00000000..6d411212
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/AnyResultSet.java
@@ -0,0 +1,11 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.query.dnf.AnyQuery;
+
+public sealed interface AnyResultSet permits ResultSet {
+        ModelQueryAdapter getAdapter();
+
+        AnyQuery getQuery();
+
+        int size();
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java
new file mode 100644
index 00000000..cec4c19f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java
@@ -0,0 +1,65 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.literal.*;
+import tools.refinery.store.query.term.*;
+
+import java.util.List;
+
+public interface Constraint {
+        String name();
+
+        List<Sort> getSorts();
+
+        default int arity() {
+                return getSorts().size();
+        }
+
+        default boolean invalidIndex(int i) {
+                return i < 0 || i >= arity();
+        }
+
+        default LiteralReduction getReduction() {
+                return LiteralReduction.NOT_REDUCIBLE;
+        }
+
+        default boolean equals(LiteralEqualityHelper helper, Constraint other) {
+                return equals(other);
+        }
+
+        String toReferenceString();
+
+        default CallLiteral call(CallPolarity polarity, List<Variable> arguments) {
+                return new CallLiteral(polarity, this, arguments);
+        }
+
+        default CallLiteral call(CallPolarity polarity, Variable... arguments) {
+                return call(polarity, List.of(arguments));
+        }
+
+        default CallLiteral call(Variable... arguments) {
+                return call(CallPolarity.POSITIVE, arguments);
+        }
+
+        default CallLiteral callTransitive(NodeVariable left, NodeVariable right) {
+                return call(CallPolarity.TRANSITIVE, List.of(left, right));
+        }
+
+        default AssignedValue<Integer> count(List<Variable> arguments) {
+                return targetVariable -> new CountLiteral(targetVariable, this, arguments);
+        }
+
+        default AssignedValue<Integer> count(Variable... arguments) {
+                return count(List.of(arguments));
+        }
+
+        default <R, T> AssignedValue<R> aggregate(DataVariable<T> inputVariable, Aggregator<R, T> aggregator,
+                                                                                          List<Variable> arguments) {
+                return targetVariable -> new AggregationLiteral<>(targetVariable, aggregator, inputVariable, this, arguments);
+        }
+
+        default <R, T> AssignedValue<R> aggregate(DataVariable<T> inputVariable, Aggregator<R, T> aggregator,
+                                                                                          Variable... arguments) {
+                return aggregate(inputVariable, aggregator, List.of(arguments));
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java
new file mode 100644
index 00000000..9af73bdd
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java
@@ -0,0 +1,34 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.map.Cursors;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.tuple.TupleLike;
+
+public record EmptyResultSet<T>(ModelQueryAdapter adapter, Query<T> query) implements ResultSet<T> {
+        @Override
+        public ModelQueryAdapter getAdapter() {
+                return adapter;
+        }
+
+        @Override
+        public Query<T> getQuery() {
+                return query;
+        }
+
+        @Override
+        public T get(TupleLike parameters) {
+                return query.defaultValue();
+        }
+
+
+        @Override
+        public Cursor<TupleLike, T> getAll() {
+                return Cursors.empty();
+        }
+
+        @Override
+        public int size() {
+                return 0;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQuery.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQuery.java
new file mode 100644
index 00000000..6a1aeabb
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQuery.java
@@ -0,0 +1,11 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.adapter.ModelAdapterType;
+
+public final class ModelQuery extends ModelAdapterType<ModelQueryAdapter, ModelQueryStoreAdapter, ModelQueryBuilder> {
+        public static final ModelQuery ADAPTER = new ModelQuery();
+
+        private ModelQuery() {
+                super(ModelQueryAdapter.class, ModelQueryStoreAdapter.class, ModelQueryBuilder.class);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java
new file mode 100644
index 00000000..2e30fec4
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryAdapter.java
@@ -0,0 +1,19 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.adapter.ModelAdapter;
+import tools.refinery.store.query.dnf.AnyQuery;
+import tools.refinery.store.query.dnf.Query;
+
+public interface ModelQueryAdapter extends ModelAdapter {
+        ModelQueryStoreAdapter getStoreAdapter();
+
+        default AnyResultSet getResultSet(AnyQuery query) {
+                return getResultSet((Query<?>) query);
+        }
+
+        <T> ResultSet<T> getResultSet(Query<T> query);
+
+        boolean hasPendingChanges();
+
+        void flushChanges();
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java
new file mode 100644
index 00000000..4fdc9210
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryBuilder.java
@@ -0,0 +1,25 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.adapter.ModelAdapterBuilder;
+import tools.refinery.store.model.ModelStore;
+import tools.refinery.store.query.dnf.AnyQuery;
+
+import java.util.Collection;
+import java.util.List;
+
+@SuppressWarnings("UnusedReturnValue")
+public interface ModelQueryBuilder extends ModelAdapterBuilder {
+        default ModelQueryBuilder queries(AnyQuery... queries) {
+                return queries(List.of(queries));
+        }
+
+        default ModelQueryBuilder queries(Collection<? extends AnyQuery> queries) {
+                queries.forEach(this::query);
+                return this;
+        }
+
+        ModelQueryBuilder query(AnyQuery query);
+
+        @Override
+        ModelQueryStoreAdapter createStoreAdapter(ModelStore store);
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java
new file mode 100644
index 00000000..514e582b
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ModelQueryStoreAdapter.java
@@ -0,0 +1,17 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.adapter.ModelStoreAdapter;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.dnf.AnyQuery;
+import tools.refinery.store.query.view.AnyRelationView;
+
+import java.util.Collection;
+
+public interface ModelQueryStoreAdapter extends ModelStoreAdapter {
+        Collection<AnyRelationView> getRelationViews();
+
+        Collection<AnyQuery> getQueries();
+
+        @Override
+        ModelQueryAdapter createModelAdapter(Model model);
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/ResultSet.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/ResultSet.java
new file mode 100644
index 00000000..3f6bc06f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/ResultSet.java
@@ -0,0 +1,13 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.map.Cursor;
+import tools.refinery.store.query.dnf.Query;
+import tools.refinery.store.tuple.TupleLike;
+
+public non-sealed interface ResultSet<T> extends AnyResultSet {
+        Query<T> getQuery();
+
+        T get(TupleLike parameters);
+
+        Cursor<TupleLike, T> getAll();
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/AnyQuery.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/AnyQuery.java
new file mode 100644
index 00000000..d0a2367f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/AnyQuery.java
@@ -0,0 +1,11 @@
+package tools.refinery.store.query.dnf;
+
+public sealed interface AnyQuery permits Query {
+        String name();
+
+        int arity();
+
+        Class<?> valueType();
+
+        Dnf getDnf();
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java
new file mode 100644
index 00000000..1b7759c7
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java
@@ -0,0 +1,194 @@
+package tools.refinery.store.query.dnf;
+
+import tools.refinery.store.query.equality.DnfEqualityChecker;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.literal.LiteralReduction;
+import tools.refinery.store.query.term.Sort;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+
+public final class Dnf implements Constraint {
+        private static final String INDENTATION = "    ";
+
+        private final String name;
+
+        private final String uniqueName;
+
+        private final List<Variable> parameters;
+
+        private final List<FunctionalDependency<Variable>> functionalDependencies;
+
+        private final List<DnfClause> clauses;
+
+        Dnf(String name, List<Variable> parameters, List<FunctionalDependency<Variable>> functionalDependencies,
+                List<DnfClause> clauses) {
+                validateFunctionalDependencies(parameters, functionalDependencies);
+                this.name = name;
+                this.uniqueName = DnfUtils.generateUniqueName(name);
+                this.parameters = parameters;
+                this.functionalDependencies = functionalDependencies;
+                this.clauses = clauses;
+        }
+
+        private static void validateFunctionalDependencies(
+                        Collection<Variable> parameters, Collection<FunctionalDependency<Variable>> functionalDependencies) {
+                var parameterSet = new HashSet<>(parameters);
+                for (var functionalDependency : functionalDependencies) {
+                        validateParameters(parameters, parameterSet, functionalDependency.forEach(), functionalDependency);
+                        validateParameters(parameters, parameterSet, functionalDependency.unique(), functionalDependency);
+                }
+        }
+
+        private static void validateParameters(Collection<Variable> parameters, Set<Variable> parameterSet,
+                                                                                   Collection<Variable> toValidate,
+                                                                                   FunctionalDependency<Variable> functionalDependency) {
+                for (var variable : toValidate) {
+                        if (!parameterSet.contains(variable)) {
+                                throw new IllegalArgumentException(
+                                                "Variable %s of functional dependency %s does not appear in the parameter list %s"
+                                                                .formatted(variable, functionalDependency, parameters));
+                        }
+                }
+        }
+
+        @Override
+        public String name() {
+                return name == null ? uniqueName : name;
+        }
+
+        public boolean isExplicitlyNamed() {
+                return name == null;
+        }
+
+        public String getUniqueName() {
+                return uniqueName;
+        }
+
+        public List<Variable> getParameters() {
+                return parameters;
+        }
+
+        @Override
+        public List<Sort> getSorts() {
+                return parameters.stream().map(Variable::getSort).toList();
+        }
+
+        public List<FunctionalDependency<Variable>> getFunctionalDependencies() {
+                return functionalDependencies;
+        }
+
+        @Override
+        public int arity() {
+                return parameters.size();
+        }
+
+        public List<DnfClause> getClauses() {
+                return clauses;
+        }
+
+        public RelationalQuery asRelation() {
+                return new RelationalQuery(this);
+        }
+
+        public <T> FunctionalQuery<T> asFunction(Class<T> type) {
+                return new FunctionalQuery<>(this, type);
+        }
+
+        @Override
+        public LiteralReduction getReduction() {
+                if (clauses.isEmpty()) {
+                        return LiteralReduction.ALWAYS_FALSE;
+                }
+                for (var clause : clauses) {
+                        if (clause.literals().isEmpty()) {
+                                return LiteralReduction.ALWAYS_TRUE;
+                        }
+                }
+                return LiteralReduction.NOT_REDUCIBLE;
+        }
+
+        public boolean equalsWithSubstitution(DnfEqualityChecker callEqualityChecker, Dnf other) {
+                if (arity() != other.arity()) {
+                        return false;
+                }
+                int numClauses = clauses.size();
+                if (numClauses != other.clauses.size()) {
+                        return false;
+                }
+                for (int i = 0; i < numClauses; i++) {
+                        var literalEqualityHelper = new LiteralEqualityHelper(callEqualityChecker, parameters, other.parameters);
+                        if (!clauses.get(i).equalsWithSubstitution(literalEqualityHelper, other.clauses.get(i))) {
+                                return false;
+                        }
+                }
+                return true;
+        }
+
+        @Override
+        public boolean equals(LiteralEqualityHelper helper, Constraint other) {
+                if (other instanceof Dnf otherDnf) {
+                        return helper.dnfEqual(this, otherDnf);
+                }
+                return false;
+        }
+
+        @Override
+        public String toString() {
+                return "%s/%d".formatted(name, arity());
+        }
+
+        @Override
+        public String toReferenceString() {
+                return "@Dnf " + name;
+        }
+
+        public String toDefinitionString() {
+                var builder = new StringBuilder();
+                builder.append("pred ").append(name()).append("(");
+                var parameterIterator = parameters.iterator();
+                if (parameterIterator.hasNext()) {
+                        builder.append(parameterIterator.next());
+                        while (parameterIterator.hasNext()) {
+                                builder.append(", ").append(parameterIterator.next());
+                        }
+                }
+                builder.append(") <->");
+                var clauseIterator = clauses.iterator();
+                if (clauseIterator.hasNext()) {
+                        appendClause(clauseIterator.next(), builder);
+                        while (clauseIterator.hasNext()) {
+                                builder.append("\n;");
+                                appendClause(clauseIterator.next(), builder);
+                        }
+                } else {
+                        builder.append("\n").append(INDENTATION).append("<no clauses>");
+                }
+                builder.append(".\n");
+                return builder.toString();
+        }
+
+        private static void appendClause(DnfClause clause, StringBuilder builder) {
+                var iterator = clause.literals().iterator();
+                if (!iterator.hasNext()) {
+                        builder.append("\n").append(INDENTATION).append("<empty>");
+                        return;
+                }
+                builder.append("\n").append(INDENTATION).append(iterator.next());
+                while (iterator.hasNext()) {
+                        builder.append(",\n").append(INDENTATION).append(iterator.next());
+                }
+        }
+
+        public static DnfBuilder builder() {
+                return builder(null);
+        }
+
+        public static DnfBuilder builder(String name) {
+                return new DnfBuilder(name);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java
new file mode 100644
index 00000000..aad5a85f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java
@@ -0,0 +1,110 @@
+package tools.refinery.store.query.dnf;
+
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.*;
+
+@SuppressWarnings("UnusedReturnValue")
+public final class DnfBuilder {
+        private final String name;
+
+        private final List<Variable> parameters = new ArrayList<>();
+
+        private final List<FunctionalDependency<Variable>> functionalDependencies = new ArrayList<>();
+
+        private final List<List<Literal>> clauses = new ArrayList<>();
+
+        DnfBuilder(String name) {
+                this.name = name;
+        }
+
+        public DnfBuilder parameter(Variable variable) {
+                if (parameters.contains(variable)) {
+                        throw new IllegalArgumentException("Duplicate parameter: " + variable);
+                }
+                parameters.add(variable);
+                return this;
+        }
+
+        public DnfBuilder parameters(Variable... variables) {
+                return parameters(List.of(variables));
+        }
+
+        public DnfBuilder parameters(Collection<? extends Variable> variables) {
+                parameters.addAll(variables);
+                return this;
+        }
+
+        public DnfBuilder functionalDependencies(Collection<FunctionalDependency<Variable>> functionalDependencies) {
+                this.functionalDependencies.addAll(functionalDependencies);
+                return this;
+        }
+
+        public DnfBuilder functionalDependency(FunctionalDependency<Variable> functionalDependency) {
+                functionalDependencies.add(functionalDependency);
+                return this;
+        }
+
+        public DnfBuilder functionalDependency(Set<? extends Variable> forEach, Set<? extends Variable> unique) {
+                return functionalDependency(new FunctionalDependency<>(Set.copyOf(forEach), Set.copyOf(unique)));
+        }
+
+        public DnfBuilder clause(Literal... literals) {
+                clause(List.of(literals));
+                return this;
+        }
+
+        public DnfBuilder clause(Collection<? extends Literal> literals) {
+                // Remove duplicates by using a hashed data structure.
+                var filteredLiterals = new LinkedHashSet<Literal>(literals.size());
+                for (var literal : literals) {
+                        var reduction = literal.getReduction();
+                        switch (reduction) {
+                        case NOT_REDUCIBLE -> filteredLiterals.add(literal);
+                        case ALWAYS_TRUE -> {
+                                // Literals reducible to {@code true} can be omitted, because the model is always assumed to have at
+                                // least on object.
+                        }
+                        case ALWAYS_FALSE -> {
+                                // Clauses with {@code false} literals can be omitted entirely.
+                                return this;
+                        }
+                        default -> throw new IllegalArgumentException("Invalid reduction: " + reduction);
+                        }
+                }
+                clauses.add(List.copyOf(filteredLiterals));
+                return this;
+        }
+
+        public Dnf build() {
+                var postProcessedClauses = postProcessClauses();
+                return new Dnf(name, Collections.unmodifiableList(parameters),
+                                Collections.unmodifiableList(functionalDependencies),
+                                Collections.unmodifiableList(postProcessedClauses));
+        }
+
+        <T> void output(DataVariable<T> outputVariable) {
+                functionalDependency(Set.copyOf(parameters), Set.of(outputVariable));
+                parameter(outputVariable);
+        }
+
+        private List<DnfClause> postProcessClauses() {
+                var postProcessedClauses = new ArrayList<DnfClause>(clauses.size());
+                for (var literals : clauses) {
+                        if (literals.isEmpty()) {
+                                // Predicate will always match, the other clauses are irrelevant.
+                                return List.of(new DnfClause(Set.of(), List.of()));
+                        }
+                        var variables = new HashSet<Variable>();
+                        for (var literal : literals) {
+                                variables.addAll(literal.getBoundVariables());
+                        }
+                        parameters.forEach(variables::remove);
+                        postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables),
+                                        Collections.unmodifiableList(literals)));
+                }
+                return postProcessedClauses;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java
new file mode 100644
index 00000000..01830af1
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java
@@ -0,0 +1,23 @@
+package tools.refinery.store.query.dnf;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.List;
+import java.util.Set;
+
+public record DnfClause(Set<Variable> boundVariables, List<Literal> literals) {
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, DnfClause other) {
+                int size = literals.size();
+                if (size != other.literals.size()) {
+                        return false;
+                }
+                for (int i = 0; i < size; i++) {
+                        if (!literals.get(i).equalsWithSubstitution(helper, other.literals.get(i))) {
+                                return false;
+                        }
+                }
+                return true;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfUtils.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfUtils.java
new file mode 100644
index 00000000..9bcf944c
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfUtils.java
@@ -0,0 +1,19 @@
+package tools.refinery.store.query.dnf;
+
+import java.util.UUID;
+
+public final class DnfUtils {
+        private DnfUtils() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static String generateUniqueName(String originalName) {
+                UUID uuid = UUID.randomUUID();
+                String uniqueString = "_" + uuid.toString().replace('-', '_');
+                if (originalName == null) {
+                        return uniqueString;
+                } else {
+                        return originalName + uniqueString;
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalDependency.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalDependency.java
new file mode 100644
index 00000000..f4cd109f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalDependency.java
@@ -0,0 +1,15 @@
+package tools.refinery.store.query.dnf;
+
+import java.util.HashSet;
+import java.util.Set;
+
+public record FunctionalDependency<T>(Set<T> forEach, Set<T> unique) {
+        public FunctionalDependency {
+                var uniqueForEach = new HashSet<>(unique);
+                uniqueForEach.retainAll(forEach);
+                if (!uniqueForEach.isEmpty()) {
+                        throw new IllegalArgumentException("Variables %s appear on both sides of the functional dependency"
+                                        .formatted(uniqueForEach));
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQuery.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQuery.java
new file mode 100644
index 00000000..5bf6f8c5
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQuery.java
@@ -0,0 +1,103 @@
+package tools.refinery.store.query.dnf;
+
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.term.*;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Objects;
+
+public final class FunctionalQuery<T> implements Query<T> {
+        private final Dnf dnf;
+        private final Class<T> type;
+
+        FunctionalQuery(Dnf dnf, Class<T> type) {
+                var parameters = dnf.getParameters();
+                int outputIndex = dnf.arity() - 1;
+                for (int i = 0; i < outputIndex; i++) {
+                        var parameter = parameters.get(i);
+                        if (!(parameter instanceof NodeVariable)) {
+                                throw new IllegalArgumentException("Expected parameter %s of %s to be of sort %s, but got %s instead"
+                                                .formatted(parameter, dnf, NodeSort.INSTANCE, parameter.getSort()));
+                        }
+                }
+                var outputParameter = parameters.get(outputIndex);
+                if (!(outputParameter instanceof DataVariable<?> dataOutputParameter) ||
+                                !dataOutputParameter.getType().equals(type)) {
+                        throw new IllegalArgumentException("Expected parameter %s of %s to be of sort %s, but got %s instead"
+                                        .formatted(outputParameter, dnf, type, outputParameter.getSort()));
+                }
+                this.dnf = dnf;
+                this.type = type;
+        }
+
+        @Override
+        public String name() {
+                return dnf.name();
+        }
+
+        @Override
+        public int arity() {
+                return dnf.arity() - 1;
+        }
+
+        @Override
+        public Class<T> valueType() {
+                return type;
+        }
+
+        @Override
+        public T defaultValue() {
+                return null;
+        }
+
+        @Override
+        public Dnf getDnf() {
+                return dnf;
+        }
+
+        public AssignedValue<T> call(List<NodeVariable> arguments) {
+                return targetVariable -> {
+                        var argumentsWithTarget = new ArrayList<Variable>(arguments.size() + 1);
+                        argumentsWithTarget.addAll(arguments);
+                        argumentsWithTarget.add(targetVariable);
+                        return dnf.call(CallPolarity.POSITIVE, argumentsWithTarget);
+                };
+        }
+
+        public AssignedValue<T> call(NodeVariable... arguments) {
+                return call(List.of(arguments));
+        }
+
+        public <R> AssignedValue<R> aggregate(Aggregator<R, T> aggregator, List<NodeVariable> arguments) {
+                return targetVariable -> {
+                        var placeholderVariable = Variable.of(type);
+                        var argumentsWithPlaceholder = new ArrayList<Variable>(arguments.size() + 1);
+                        argumentsWithPlaceholder.addAll(arguments);
+                        argumentsWithPlaceholder.add(placeholderVariable);
+                        return dnf.aggregate(placeholderVariable, aggregator, argumentsWithPlaceholder).toLiteral(targetVariable);
+                };
+        }
+
+        public <R> AssignedValue<R> aggregate(Aggregator<R, T> aggregator, NodeVariable... arguments) {
+                return aggregate(aggregator, List.of(arguments));
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                FunctionalQuery<?> that = (FunctionalQuery<?>) o;
+                return dnf.equals(that.dnf) && type.equals(that.type);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(dnf, type);
+        }
+
+        @Override
+        public String toString() {
+                return dnf.toString();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQueryBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQueryBuilder.java
new file mode 100644
index 00000000..ca2bc006
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQueryBuilder.java
@@ -0,0 +1,46 @@
+package tools.refinery.store.query.dnf;
+
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.Collection;
+import java.util.Set;
+
+public final class FunctionalQueryBuilder<T> {
+        private final DnfBuilder dnfBuilder;
+        private final Class<T> type;
+
+        FunctionalQueryBuilder(DnfBuilder dnfBuilder, Class<T> type) {
+                this.dnfBuilder = dnfBuilder;
+                this.type = type;
+        }
+
+        public FunctionalQueryBuilder<T> functionalDependencies(Collection<FunctionalDependency<Variable>> functionalDependencies) {
+                dnfBuilder.functionalDependencies(functionalDependencies);
+                return this;
+        }
+
+        public FunctionalQueryBuilder<T> functionalDependency(FunctionalDependency<Variable> functionalDependency) {
+                dnfBuilder.functionalDependency(functionalDependency);
+                return this;
+        }
+
+        public FunctionalQueryBuilder<T> functionalDependency(Set<? extends Variable> forEach, Set<? extends Variable> unique) {
+                dnfBuilder.functionalDependency(forEach, unique);
+                return this;
+        }
+
+        public FunctionalQueryBuilder<T> clause(Literal... literals) {
+                dnfBuilder.clause(literals);
+                return this;
+        }
+
+        public FunctionalQueryBuilder<T> clause(Collection<? extends Literal> literals) {
+                dnfBuilder.clause(literals);
+                return this;
+        }
+
+        public FunctionalQuery<T> build() {
+                return dnfBuilder.build().asFunction(type);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Query.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Query.java
new file mode 100644
index 00000000..32e33052
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Query.java
@@ -0,0 +1,16 @@
+package tools.refinery.store.query.dnf;
+
+public sealed interface Query<T> extends AnyQuery permits RelationalQuery, FunctionalQuery {
+        @Override
+        Class<T> valueType();
+
+        T defaultValue();
+
+        static QueryBuilder builder() {
+                return new QueryBuilder();
+        }
+
+        static QueryBuilder builder(String name) {
+                return new QueryBuilder(name);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/QueryBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/QueryBuilder.java
new file mode 100644
index 00000000..ed253cc9
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/QueryBuilder.java
@@ -0,0 +1,71 @@
+package tools.refinery.store.query.dnf;
+
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.NodeVariable;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.Collection;
+import java.util.List;
+import java.util.Set;
+
+public final class QueryBuilder {
+        private final DnfBuilder dnfBuilder;
+
+        QueryBuilder(String name) {
+                dnfBuilder = Dnf.builder(name);
+        }
+
+        QueryBuilder() {
+                dnfBuilder = Dnf.builder();
+        }
+
+        public QueryBuilder parameter(NodeVariable variable) {
+                dnfBuilder.parameter(variable);
+                return this;
+        }
+
+        public QueryBuilder parameters(NodeVariable... variables) {
+                dnfBuilder.parameters(variables);
+                return this;
+        }
+
+        public QueryBuilder parameters(List<NodeVariable> variables) {
+                dnfBuilder.parameters(variables);
+                return this;
+        }
+
+        public <T> FunctionalQueryBuilder<T> output(DataVariable<T> outputVariable) {
+                dnfBuilder.output(outputVariable);
+                return new FunctionalQueryBuilder<>(dnfBuilder, outputVariable.getType());
+        }
+
+        public QueryBuilder functionalDependencies(Collection<FunctionalDependency<Variable>> functionalDependencies) {
+                dnfBuilder.functionalDependencies(functionalDependencies);
+                return this;
+        }
+
+        public QueryBuilder functionalDependency(FunctionalDependency<Variable> functionalDependency) {
+                dnfBuilder.functionalDependency(functionalDependency);
+                return this;
+        }
+
+        public QueryBuilder functionalDependency(Set<? extends Variable> forEach, Set<? extends Variable> unique) {
+                dnfBuilder.functionalDependency(forEach, unique);
+                return this;
+        }
+
+        public QueryBuilder clause(Literal... literals) {
+                dnfBuilder.clause(literals);
+                return this;
+        }
+
+        public QueryBuilder clause(Collection<? extends Literal> literals) {
+                dnfBuilder.clause(literals);
+                return this;
+        }
+
+        public RelationalQuery build() {
+                return dnfBuilder.build().asRelation();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/RelationalQuery.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/RelationalQuery.java
new file mode 100644
index 00000000..5307e509
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/RelationalQuery.java
@@ -0,0 +1,93 @@
+package tools.refinery.store.query.dnf;
+
+import tools.refinery.store.query.literal.CallLiteral;
+import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.term.AssignedValue;
+import tools.refinery.store.query.term.NodeSort;
+import tools.refinery.store.query.term.NodeVariable;
+
+import java.util.Collections;
+import java.util.List;
+import java.util.Objects;
+
+public final class RelationalQuery implements Query<Boolean> {
+        private final Dnf dnf;
+
+        RelationalQuery(Dnf dnf) {
+                for (var parameter : dnf.getParameters()) {
+                        if (!(parameter instanceof NodeVariable)) {
+                                throw new IllegalArgumentException("Expected parameter %s of %s to be of sort %s, but got %s instead"
+                                                .formatted(parameter, dnf, NodeSort.INSTANCE, parameter.getSort()));
+                        }
+                }
+                this.dnf = dnf;
+        }
+
+        @Override
+        public String name() {
+                return dnf.name();
+        }
+
+        @Override
+        public int arity() {
+                return dnf.arity();
+        }
+
+        @Override
+        public Class<Boolean> valueType() {
+                return Boolean.class;
+        }
+
+        @Override
+        public Boolean defaultValue() {
+                return false;
+        }
+
+        @Override
+        public Dnf getDnf() {
+                return dnf;
+        }
+
+        public CallLiteral call(CallPolarity polarity, List<NodeVariable> arguments) {
+                return dnf.call(polarity, Collections.unmodifiableList(arguments));
+        }
+
+        public CallLiteral call(CallPolarity polarity, NodeVariable... arguments) {
+                return dnf.call(polarity, arguments);
+        }
+
+        public CallLiteral call(NodeVariable... arguments) {
+                return dnf.call(arguments);
+        }
+
+        public CallLiteral callTransitive(NodeVariable left, NodeVariable right) {
+                return dnf.callTransitive(left, right);
+        }
+
+        public AssignedValue<Integer> count(List<NodeVariable> arguments) {
+                return dnf.count(Collections.unmodifiableList(arguments));
+        }
+
+        public AssignedValue<Integer> count(NodeVariable... arguments) {
+                return dnf.count(arguments);
+        }
+
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                RelationalQuery that = (RelationalQuery) o;
+                return dnf.equals(that.dnf);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(dnf);
+        }
+
+        @Override
+        public String toString() {
+                return dnf.toString();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java
new file mode 100644
index 00000000..c3bc3ea3
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java
@@ -0,0 +1,31 @@
+package tools.refinery.store.query.equality;
+
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.util.CycleDetectingMapper;
+
+import java.util.List;
+
+public class DeepDnfEqualityChecker implements DnfEqualityChecker {
+        private final CycleDetectingMapper<Pair, Boolean> mapper = new CycleDetectingMapper<>(Pair::toString,
+                        this::doCheckEqual);
+
+        @Override
+        public boolean dnfEqual(Dnf left, Dnf right) {
+                return mapper.map(new Pair(left, right));
+        }
+
+        protected boolean doCheckEqual(Pair pair) {
+                return pair.left.equalsWithSubstitution(this, pair.right);
+        }
+
+        protected List<Pair> getInProgress() {
+                return mapper.getInProgress();
+        }
+
+        protected record Pair(Dnf left, Dnf right) {
+                @Override
+                public String toString() {
+                        return "(%s, %s)".formatted(left.name(), right.name());
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java
new file mode 100644
index 00000000..6b1f2076
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java
@@ -0,0 +1,8 @@
+package tools.refinery.store.query.equality;
+
+import tools.refinery.store.query.dnf.Dnf;
+
+@FunctionalInterface
+public interface DnfEqualityChecker {
+        boolean dnfEqual(Dnf left, Dnf right);
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java
new file mode 100644
index 00000000..07d261ea
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java
@@ -0,0 +1,48 @@
+package tools.refinery.store.query.equality;
+
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+public class LiteralEqualityHelper {
+        private final DnfEqualityChecker dnfEqualityChecker;
+        private final Map<Variable, Variable> leftToRight;
+        private final Map<Variable, Variable> rightToLeft;
+
+        public LiteralEqualityHelper(DnfEqualityChecker dnfEqualityChecker, List<Variable> leftParameters,
+                                                                 List<Variable> rightParameters) {
+                this.dnfEqualityChecker = dnfEqualityChecker;
+                var arity = leftParameters.size();
+                if (arity != rightParameters.size()) {
+                        throw new IllegalArgumentException("Parameter lists have unequal length");
+                }
+                leftToRight = new HashMap<>(arity);
+                rightToLeft = new HashMap<>(arity);
+                for (int i = 0; i < arity; i++) {
+                        if (!variableEqual(leftParameters.get(i), rightParameters.get(i))) {
+                                throw new IllegalArgumentException("Parameter lists cannot be unified: duplicate parameter " + i);
+                        }
+                }
+        }
+
+        public boolean dnfEqual(Dnf left, Dnf right) {
+                return dnfEqualityChecker.dnfEqual(left, right);
+        }
+
+        public boolean variableEqual(Variable left, Variable right) {
+                if (checkMapping(leftToRight, left, right) && checkMapping(rightToLeft, right, left)) {
+                        leftToRight.put(left, right);
+                        rightToLeft.put(right, left);
+                        return true;
+                }
+                return false;
+        }
+
+        private static boolean checkMapping(Map<Variable, Variable> map, Variable key, Variable expectedValue) {
+                var currentValue = map.get(key);
+                return currentValue == null || currentValue.equals(expectedValue);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java
new file mode 100644
index 00000000..657ca26b
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java
@@ -0,0 +1,80 @@
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.List;
+import java.util.Objects;
+
+public abstract class AbstractCallLiteral implements Literal {
+        private final Constraint target;
+        private final List<Variable> arguments;
+
+        protected AbstractCallLiteral(Constraint target, List<Variable> arguments) {
+                int arity = target.arity();
+                if (arguments.size() != arity) {
+                        throw new IllegalArgumentException("%s needs %d arguments, but got %s".formatted(target.name(),
+                                        target.arity(), arguments.size()));
+                }
+                this.target = target;
+                this.arguments = arguments;
+                var sorts = target.getSorts();
+                for (int i = 0; i < arity; i++) {
+                        var argument = arguments.get(i);
+                        var sort = sorts.get(i);
+                        if (!sort.isInstance(argument)) {
+                                throw new IllegalArgumentException("Required argument %d of %s to be of sort %s, but got %s instead"
+                                                .formatted(i, target, sort, argument.getSort()));
+                        }
+                }
+        }
+
+        public Constraint getTarget() {
+                return target;
+        }
+
+        public List<Variable> getArguments() {
+                return arguments;
+        }
+
+        @Override
+        public Literal substitute(Substitution substitution) {
+                var substitutedArguments = arguments.stream().map(substitution::getSubstitute).toList();
+                return doSubstitute(substitution, substitutedArguments);
+        }
+
+        protected abstract Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments);
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (other == null || getClass() != other.getClass()) {
+                        return false;
+                }
+                var otherCallLiteral = (AbstractCallLiteral) other;
+                var arity = arguments.size();
+                if (arity != otherCallLiteral.arguments.size()) {
+                        return false;
+                }
+                for (int i = 0; i < arity; i++) {
+                        if (!helper.variableEqual(arguments.get(i), otherCallLiteral.arguments.get(i))) {
+                                return false;
+                        }
+                }
+                return target.equals(helper, otherCallLiteral.target);
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                AbstractCallLiteral that = (AbstractCallLiteral) o;
+                return target.equals(that.target) && arguments.equals(that.arguments);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(target, arguments);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java
new file mode 100644
index 00000000..df64839c
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java
@@ -0,0 +1,113 @@
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Aggregator;
+import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.List;
+import java.util.Objects;
+import java.util.Set;
+
+public class AggregationLiteral<R, T> extends AbstractCallLiteral {
+        private final DataVariable<R> resultVariable;
+        private final DataVariable<T> inputVariable;
+        private final Aggregator<R, T> aggregator;
+
+        public AggregationLiteral(DataVariable<R> resultVariable, Aggregator<R, T> aggregator,
+                                                          DataVariable<T> inputVariable, Constraint target, List<Variable> arguments) {
+                super(target, arguments);
+                if (!inputVariable.getType().equals(aggregator.getInputType())) {
+                        throw new IllegalArgumentException("Input variable %s must of type %s, got %s instead".formatted(
+                                        inputVariable, aggregator.getInputType().getName(), inputVariable.getType().getName()));
+                }
+                if (!resultVariable.getType().equals(aggregator.getResultType())) {
+                        throw new IllegalArgumentException("Result variable %s must of type %s, got %s instead".formatted(
+                                        resultVariable, aggregator.getResultType().getName(), resultVariable.getType().getName()));
+                }
+                if (!arguments.contains(inputVariable)) {
+                        throw new IllegalArgumentException("Input variable %s must appear in the argument list".formatted(
+                                        inputVariable));
+                }
+                if (arguments.contains(resultVariable)) {
+                        throw new IllegalArgumentException("Result variable %s must not appear in the argument list".formatted(
+                                        resultVariable));
+                }
+                this.resultVariable = resultVariable;
+                this.inputVariable = inputVariable;
+                this.aggregator = aggregator;
+        }
+
+        public DataVariable<R> getResultVariable() {
+                return resultVariable;
+        }
+
+        public DataVariable<T> getInputVariable() {
+                return inputVariable;
+        }
+
+        public Aggregator<R, T> getAggregator() {
+                return aggregator;
+        }
+
+        @Override
+        public Set<Variable> getBoundVariables() {
+                return Set.of(resultVariable);
+        }
+
+        @Override
+        protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) {
+                return new AggregationLiteral<>(substitution.getTypeSafeSubstitute(resultVariable), aggregator,
+                                substitution.getTypeSafeSubstitute(inputVariable), getTarget(), substitutedArguments);
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherAggregationLiteral = (AggregationLiteral<?, ?>) other;
+                return helper.variableEqual(resultVariable, otherAggregationLiteral.resultVariable) &&
+                                aggregator.equals(otherAggregationLiteral.aggregator) &&
+                                helper.variableEqual(inputVariable, otherAggregationLiteral.inputVariable);
+        }
+
+        @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;
+                AggregationLiteral<?, ?> that = (AggregationLiteral<?, ?>) o;
+                return resultVariable.equals(that.resultVariable) && inputVariable.equals(that.inputVariable) &&
+                                aggregator.equals(that.aggregator);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), resultVariable, inputVariable, aggregator);
+        }
+
+        @Override
+        public String toString() {
+                var builder = new StringBuilder();
+                builder.append(resultVariable);
+                builder.append(" is ");
+                builder.append(getTarget().toReferenceString());
+                builder.append("(");
+                var argumentIterator = getArguments().iterator();
+                if (argumentIterator.hasNext()) {
+                        var argument = argumentIterator.next();
+                        if (inputVariable.equals(argument)) {
+                                builder.append("@Aggregate(\"").append(aggregator).append("\") ");
+                        }
+                        builder.append(argument);
+                        while (argumentIterator.hasNext()) {
+                                builder.append(", ").append(argumentIterator.next());
+                        }
+                }
+                builder.append(")");
+                return builder.toString();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java
new file mode 100644
index 00000000..52ac42d7
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java
@@ -0,0 +1,44 @@
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.Set;
+
+public record AssignLiteral<T>(DataVariable<T> variable, Term<T> term) implements Literal {
+        public AssignLiteral {
+                if (!term.getType().equals(variable.getType())) {
+                        throw new IllegalArgumentException("Term %s must be of type %s, got %s instead".formatted(
+                                        term, variable.getType().getName(), term.getType().getName()));
+                }
+        }
+
+        @Override
+        public Set<Variable> getBoundVariables() {
+                return Set.of(variable);
+        }
+
+        @Override
+        public Literal substitute(Substitution substitution) {
+                return new AssignLiteral<>(substitution.getTypeSafeSubstitute(variable), term.substitute(substitution));
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (other == null || getClass() != other.getClass()) {
+                        return false;
+                }
+                var otherLetLiteral = (AssignLiteral<?>) other;
+                return helper.variableEqual(variable, otherLetLiteral.variable) && term.equalsWithSubstitution(helper,
+                                otherLetLiteral.term);
+        }
+
+
+        @Override
+        public String toString() {
+                return "%s is (%s)".formatted(variable, term);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java
new file mode 100644
index 00000000..0b4267b4
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java
@@ -0,0 +1,53 @@
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.term.bool.BoolConstantTerm;
+
+import java.util.Set;
+
+public record AssumeLiteral(Term<Boolean> term) implements Literal {
+        public AssumeLiteral {
+                if (!term.getType().equals(Boolean.class)) {
+                        throw new IllegalArgumentException("Term %s must be of type %s, got %s instead".formatted(
+                                        term, Boolean.class.getName(), term.getType().getName()));
+                }
+        }
+
+        @Override
+        public Set<Variable> getBoundVariables() {
+                return Set.of();
+        }
+
+        @Override
+        public Literal substitute(Substitution substitution) {
+                return new AssumeLiteral(term.substitute(substitution));
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (other == null || getClass() != other.getClass()) {
+                        return false;
+                }
+                var otherAssumeLiteral = (AssumeLiteral) other;
+                return term.equalsWithSubstitution(helper, otherAssumeLiteral.term);
+        }
+
+        @Override
+        public LiteralReduction getReduction() {
+                if (BoolConstantTerm.TRUE.equals(term)) {
+                        return LiteralReduction.ALWAYS_TRUE;
+                } else if (BoolConstantTerm.FALSE.equals(term)) {
+                        return LiteralReduction.ALWAYS_FALSE;
+                } else {
+                        return LiteralReduction.NOT_REDUCIBLE;
+                }
+        }
+
+        @Override
+        public String toString() {
+                return "(%s)".formatted(term);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
new file mode 100644
index 00000000..38be61a4
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
@@ -0,0 +1,53 @@
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+
+import java.util.Set;
+
+public enum BooleanLiteral implements CanNegate<BooleanLiteral> {
+        TRUE(true),
+        FALSE(false);
+
+        private final boolean value;
+
+        BooleanLiteral(boolean value) {
+                this.value = value;
+        }
+
+        @Override
+        public Set<Variable> getBoundVariables() {
+                return Set.of();
+        }
+
+        @Override
+        public Literal substitute(Substitution substitution) {
+                // No variables to substitute.
+                return this;
+        }
+
+        @Override
+        public LiteralReduction getReduction() {
+                return value ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE;
+        }
+
+        @Override
+        public BooleanLiteral negate() {
+                return fromBoolean(!value);
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                return equals(other);
+        }
+
+        @Override
+        public String toString() {
+                return Boolean.toString(value);
+        }
+
+        public static BooleanLiteral fromBoolean(boolean value) {
+                return value ? TRUE : FALSE;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
new file mode 100644
index 00000000..78fae7f5
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
@@ -0,0 +1,102 @@
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.NodeSort;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.List;
+import java.util.Objects;
+import java.util.Set;
+
+public final class CallLiteral extends AbstractCallLiteral implements CanNegate<CallLiteral> {
+        private final CallPolarity polarity;
+
+        public CallLiteral(CallPolarity polarity, Constraint target, List<Variable> arguments) {
+                super(target, arguments);
+                if (polarity.isTransitive()) {
+                        if (target.arity() != 2) {
+                                throw new IllegalArgumentException("Transitive closures can only take binary relations");
+                        }
+                        var sorts = target.getSorts();
+                        if (!sorts.get(0).equals(NodeSort.INSTANCE) || !sorts.get(1).equals(NodeSort.INSTANCE)) {
+                                throw new IllegalArgumentException("Transitive closures can only be computed over nodes");
+                        }
+                }
+                this.polarity = polarity;
+        }
+
+        public CallPolarity getPolarity() {
+                return polarity;
+        }
+
+        @Override
+        public Set<Variable> getBoundVariables() {
+                return polarity.isPositive() ? Set.copyOf(getArguments()) : Set.of();
+        }
+
+        @Override
+        protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) {
+                return new CallLiteral(polarity, getTarget(), substitutedArguments);
+        }
+
+        @Override
+        public LiteralReduction getReduction() {
+                var reduction = getTarget().getReduction();
+                return polarity.isPositive() ? reduction : reduction.negate();
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherCallLiteral = (CallLiteral) other;
+                return polarity.equals(otherCallLiteral.polarity);
+        }
+
+        @Override
+        public CallLiteral negate() {
+                return new CallLiteral(polarity.negate(), getTarget(), getArguments());
+        }
+
+        @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;
+                CallLiteral that = (CallLiteral) o;
+                return polarity == that.polarity;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), polarity);
+        }
+
+        @Override
+        public String toString() {
+                var builder = new StringBuilder();
+                if (!polarity.isPositive()) {
+                        builder.append("!(");
+                }
+                builder.append(getTarget().toReferenceString());
+                if (polarity.isTransitive()) {
+                        builder.append("+");
+                }
+                builder.append("(");
+                var argumentIterator = getArguments().iterator();
+                if (argumentIterator.hasNext()) {
+                        builder.append(argumentIterator.next());
+                        while (argumentIterator.hasNext()) {
+                                builder.append(", ").append(argumentIterator.next());
+                        }
+                }
+                builder.append(")");
+                if (!polarity.isPositive()) {
+                        builder.append(")");
+                }
+                return builder.toString();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallPolarity.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallPolarity.java
new file mode 100644
index 00000000..84b4b771
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallPolarity.java
@@ -0,0 +1,32 @@
+package tools.refinery.store.query.literal;
+
+public enum CallPolarity {
+        POSITIVE(true, false),
+        NEGATIVE(false, false),
+        TRANSITIVE(true, true);
+
+        private final boolean positive;
+
+        private final boolean transitive;
+
+        CallPolarity(boolean positive, boolean transitive) {
+                this.positive = positive;
+                this.transitive = transitive;
+        }
+
+        public boolean isPositive() {
+                return positive;
+        }
+
+        public boolean isTransitive() {
+                return transitive;
+        }
+
+        public CallPolarity negate() {
+                return switch (this) {
+                        case POSITIVE -> NEGATIVE;
+                        case NEGATIVE -> POSITIVE;
+                        case TRANSITIVE -> throw new IllegalArgumentException("Transitive polarity cannot be negated");
+                };
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CanNegate.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CanNegate.java
new file mode 100644
index 00000000..3e159c43
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CanNegate.java
@@ -0,0 +1,5 @@
+package tools.refinery.store.query.literal;
+
+public interface CanNegate<T extends CanNegate<T>> extends Literal {
+        T negate();
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
new file mode 100644
index 00000000..93fa3df0
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
@@ -0,0 +1,34 @@
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.NodeVariable;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.Set;
+
+public record ConstantLiteral(NodeVariable variable, int nodeId) implements Literal {
+        @Override
+        public Set<Variable> getBoundVariables() {
+                return Set.of(variable);
+        }
+
+        @Override
+        public ConstantLiteral substitute(Substitution substitution) {
+                return new ConstantLiteral(substitution.getTypeSafeSubstitute(variable), nodeId);
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (other.getClass() != getClass()) {
+                        return false;
+                }
+                var otherConstantLiteral = (ConstantLiteral) other;
+                return helper.variableEqual(variable, otherConstantLiteral.variable) && nodeId == otherConstantLiteral.nodeId;
+        }
+
+        @Override
+        public String toString() {
+                return "%s === @Constant %d".formatted(variable, nodeId);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
new file mode 100644
index 00000000..32e7ba3a
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
@@ -0,0 +1,83 @@
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.Constraint;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.List;
+import java.util.Objects;
+import java.util.Set;
+
+public class CountLiteral extends AbstractCallLiteral {
+        private final DataVariable<Integer> resultVariable;
+
+        public CountLiteral(DataVariable<Integer> resultVariable, Constraint target, List<Variable> arguments) {
+                super(target, arguments);
+                if (!resultVariable.getType().equals(Integer.class)) {
+                        throw new IllegalArgumentException("Count result variable %s must be of type %s, got %s instead".formatted(
+                                        resultVariable, Integer.class.getName(), resultVariable.getType().getName()));
+                }
+                if (arguments.contains(resultVariable)) {
+                        throw new IllegalArgumentException("Count result variable %s must not appear in the argument list"
+                                        .formatted(resultVariable));
+                }
+                this.resultVariable = resultVariable;
+        }
+
+        public DataVariable<Integer> getResultVariable() {
+                return resultVariable;
+        }
+
+        @Override
+        public Set<Variable> getBoundVariables() {
+                return Set.of(resultVariable);
+        }
+
+        @Override
+        protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) {
+                return new CountLiteral(substitution.getTypeSafeSubstitute(resultVariable), getTarget(), substitutedArguments);
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherCountLiteral = (CountLiteral) other;
+                return helper.variableEqual(resultVariable, otherCountLiteral.resultVariable);
+        }
+
+        @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;
+                CountLiteral that = (CountLiteral) o;
+                return resultVariable.equals(that.resultVariable);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), resultVariable);
+        }
+
+        @Override
+        public String toString() {
+                var builder = new StringBuilder();
+                builder.append(resultVariable);
+                builder.append(" is count ");
+                builder.append(getTarget().toReferenceString());
+                builder.append("(");
+                var argumentIterator = getArguments().iterator();
+                if (argumentIterator.hasNext()) {
+                        builder.append(argumentIterator.next());
+                        while (argumentIterator.hasNext()) {
+                                builder.append(", ").append(argumentIterator.next());
+                        }
+                }
+                builder.append(")");
+                return builder.toString();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
new file mode 100644
index 00000000..4dc86b98
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
@@ -0,0 +1,52 @@
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.term.NodeVariable;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+
+import java.util.Set;
+
+public record EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right)
+                implements CanNegate<EquivalenceLiteral> {
+        @Override
+        public Set<Variable> getBoundVariables() {
+                // If one side of a {@code positive} equivalence is bound, it may bind its other side, but we under-approximate
+                // this behavior by not binding any of the sides by default.
+                return Set.of();
+        }
+
+        @Override
+        public EquivalenceLiteral negate() {
+                return new EquivalenceLiteral(!positive, left, right);
+        }
+
+        @Override
+        public EquivalenceLiteral substitute(Substitution substitution) {
+                return new EquivalenceLiteral(positive, substitution.getTypeSafeSubstitute(left),
+                                substitution.getTypeSafeSubstitute(right));
+        }
+
+        @Override
+        public LiteralReduction getReduction() {
+                if (left.equals(right)) {
+                        return positive ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE;
+                }
+                return LiteralReduction.NOT_REDUCIBLE;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (other.getClass() != getClass()) {
+                        return false;
+                }
+                var otherEquivalenceLiteral = (EquivalenceLiteral) other;
+                return helper.variableEqual(left, otherEquivalenceLiteral.left) && helper.variableEqual(right,
+                                otherEquivalenceLiteral.right);
+        }
+
+        @Override
+        public String toString() {
+                return "%s %s %s".formatted(left, positive ? "===" : "!==", right);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
new file mode 100644
index 00000000..6347410e
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
@@ -0,0 +1,20 @@
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+
+import java.util.Set;
+
+public interface Literal {
+        Set<Variable> getBoundVariables();
+
+        Literal substitute(Substitution substitution);
+
+        default LiteralReduction getReduction() {
+                return LiteralReduction.NOT_REDUCIBLE;
+        }
+
+        @SuppressWarnings("BooleanMethodIsAlwaysInverted")
+        boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other);
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java
new file mode 100644
index 00000000..146089f6
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/LiteralReduction.java
@@ -0,0 +1,26 @@
+package tools.refinery.store.query.literal;
+
+public enum LiteralReduction {
+        /**
+         * Signifies that a literal should be preserved in the clause.
+         */
+        NOT_REDUCIBLE,
+
+        /**
+         * Signifies that the literal may be omitted from the cause (if the model being queried is nonempty).
+         */
+        ALWAYS_TRUE,
+
+        /**
+         * Signifies that the clause with the literal may be omitted entirely.
+         */
+        ALWAYS_FALSE;
+
+        public LiteralReduction negate() {
+                return switch (this) {
+                        case NOT_REDUCIBLE -> NOT_REDUCIBLE;
+                        case ALWAYS_TRUE -> ALWAYS_FALSE;
+                        case ALWAYS_FALSE -> ALWAYS_TRUE;
+                };
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literals.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literals.java
new file mode 100644
index 00000000..89039352
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literals.java
@@ -0,0 +1,17 @@
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.term.Term;
+
+public final class Literals {
+        private Literals() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static <T extends CanNegate<T>> T not(CanNegate<T> literal) {
+                return literal.negate();
+        }
+
+        public static AssumeLiteral assume(Term<Boolean> term) {
+                return new AssumeLiteral(term);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/CompositeSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/CompositeSubstitution.java
new file mode 100644
index 00000000..f8064ca2
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/CompositeSubstitution.java
@@ -0,0 +1,10 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.term.Variable;
+
+public record CompositeSubstitution(Substitution first, Substitution second) implements Substitution {
+        @Override
+        public Variable getSubstitute(Variable variable) {
+                return second.getSubstitute(first.getSubstitute(variable));
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java
new file mode 100644
index 00000000..c7754619
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java
@@ -0,0 +1,13 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.term.Variable;
+
+import java.util.Map;
+
+public record MapBasedSubstitution(Map<Variable, Variable> map, Substitution fallback) implements Substitution {
+        @Override
+        public Variable getSubstitute(Variable variable) {
+                var value = map.get(variable);
+                return value == null ? fallback.getSubstitute(variable) : value;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java
new file mode 100644
index 00000000..7847e582
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java
@@ -0,0 +1,15 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.term.Variable;
+
+import java.util.HashMap;
+import java.util.Map;
+
+public class RenewingSubstitution implements Substitution {
+        private final Map<Variable, Variable> alreadyRenewed = new HashMap<>();
+
+        @Override
+        public Variable getSubstitute(Variable variable) {
+                return alreadyRenewed.computeIfAbsent(variable, Variable::renew);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java
new file mode 100644
index 00000000..eed414d9
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java
@@ -0,0 +1,18 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.term.Variable;
+
+public enum StatelessSubstitution implements Substitution {
+        FAILING {
+                @Override
+                public Variable getSubstitute(Variable variable) {
+                        throw new IllegalArgumentException("No substitute for " + variable);
+                }
+        },
+        IDENTITY {
+                @Override
+                public Variable getSubstitute(Variable variable) {
+                        return variable;
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java
new file mode 100644
index 00000000..99f84b9e
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java
@@ -0,0 +1,29 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.term.AnyDataVariable;
+import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.NodeVariable;
+import tools.refinery.store.query.term.Variable;
+
+@FunctionalInterface
+public interface Substitution {
+        Variable getSubstitute(Variable variable);
+
+        default NodeVariable getTypeSafeSubstitute(NodeVariable variable) {
+                var substitute = getSubstitute(variable);
+                return substitute.asNodeVariable();
+        }
+
+        default AnyDataVariable getTypeSafeSubstitute(AnyDataVariable variable) {
+                return getTypeSafeSubstitute((DataVariable<?>) variable);
+        }
+
+        default <T> DataVariable<T> getTypeSafeSubstitute(DataVariable<T> variable) {
+                var substitute = getSubstitute(variable);
+                return substitute.asDataVariable(variable.getType());
+        }
+
+        default Substitution andThen(Substitution second) {
+                return new CompositeSubstitution(this, second);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java
new file mode 100644
index 00000000..5d4654da
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java
@@ -0,0 +1,33 @@
+package tools.refinery.store.query.substitution;
+
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.Map;
+
+public final class Substitutions {
+        private Substitutions() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiate directly");
+        }
+
+        public static Substitution total(Map<Variable, Variable> map) {
+                return new MapBasedSubstitution(map, StatelessSubstitution.FAILING);
+        }
+
+        public static Substitution partial(Map<Variable, Variable> map) {
+                return new MapBasedSubstitution(map, StatelessSubstitution.IDENTITY);
+        }
+
+        public static Substitution renewing(Map<Variable, Variable> map) {
+                return new MapBasedSubstitution(map, renewing());
+        }
+
+        public static Substitution renewing() {
+                return new RenewingSubstitution();
+        }
+
+        public static Substitution compose(@Nullable Substitution first, @NotNull Substitution second) {
+                return first == null ? second : first.andThen(second);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Aggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Aggregator.java
new file mode 100644
index 00000000..47421a94
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Aggregator.java
@@ -0,0 +1,13 @@
+package tools.refinery.store.query.term;
+
+import java.util.stream.Stream;
+
+public interface Aggregator<R, T> {
+        Class<R> getResultType();
+
+        Class<T> getInputType();
+
+        R aggregateStream(Stream<T> stream);
+
+        R getEmptyResult();
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java
new file mode 100644
index 00000000..ecfefcf9
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java
@@ -0,0 +1,33 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+
+import java.util.Set;
+
+public abstract sealed class AnyDataVariable extends Variable implements AnyTerm permits DataVariable {
+        protected AnyDataVariable(String name) {
+                super(name);
+        }
+
+        @Override
+        public NodeVariable asNodeVariable() {
+                throw new IllegalStateException("%s is a data variable".formatted(this));
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                return other instanceof AnyDataVariable dataVariable && helper.variableEqual(this, dataVariable);
+        }
+
+        @Override
+        public Set<AnyDataVariable> getInputVariables() {
+                return Set.of(this);
+        }
+
+        @Override
+        public abstract AnyDataVariable renew(@Nullable String name);
+
+        @Override
+        public abstract AnyDataVariable renew();
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyTerm.java
new file mode 100644
index 00000000..8f998d45
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyTerm.java
@@ -0,0 +1,16 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+
+import java.util.Set;
+
+public sealed interface AnyTerm permits AnyDataVariable, Term {
+        Class<?> getType();
+
+        AnyTerm substitute(Substitution substitution);
+
+        boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other);
+
+        Set<AnyDataVariable> getInputVariables();
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryOperator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryOperator.java
new file mode 100644
index 00000000..8706a046
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryOperator.java
@@ -0,0 +1,26 @@
+package tools.refinery.store.query.term;
+
+public enum ArithmeticBinaryOperator {
+        ADD("+", true),
+        SUB("-", true),
+        MUL("*", true),
+        DIV("/", true),
+        POW("**", true),
+        MIN("min", false),
+        MAX("max", false);
+
+        private final String text;
+        private final boolean infix;
+
+        ArithmeticBinaryOperator(String text, boolean infix) {
+                this.text = text;
+                this.infix = infix;
+        }
+
+        public String formatString(String left, String right) {
+                if (infix) {
+                        return "(%s) %s (%s)".formatted(left, text, right);
+                }
+                return "%s(%s, %s)".formatted(text, left, right);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryTerm.java
new file mode 100644
index 00000000..887a1e6e
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryTerm.java
@@ -0,0 +1,56 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+
+import java.util.Objects;
+
+public abstract class ArithmeticBinaryTerm<T> extends BinaryTerm<T, T, T> {
+        private final ArithmeticBinaryOperator operator;
+
+        protected ArithmeticBinaryTerm(ArithmeticBinaryOperator operator, Term<T> left, Term<T> right) {
+                super(left, right);
+                this.operator = operator;
+        }
+
+        @Override
+        public Class<T> getLeftType() {
+                return getType();
+        }
+
+        @Override
+        public Class<T> getRightType() {
+                return getType();
+        }
+
+        public ArithmeticBinaryOperator getOperator() {
+                return operator;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherArithmeticBinaryTerm = (ArithmeticBinaryTerm<?>) other;
+                return operator == otherArithmeticBinaryTerm.operator;
+        }
+
+        @Override
+        public String toString() {
+                return operator.formatString(getLeft().toString(), getRight().toString());
+        }
+
+        @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;
+                ArithmeticBinaryTerm<?> that = (ArithmeticBinaryTerm<?>) o;
+                return operator == that.operator;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), operator);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryOperator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryOperator.java
new file mode 100644
index 00000000..6a7c25db
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryOperator.java
@@ -0,0 +1,16 @@
+package tools.refinery.store.query.term;
+
+public enum ArithmeticUnaryOperator {
+        PLUS("+"),
+        MINUS("-");
+
+        private final String prefix;
+
+        ArithmeticUnaryOperator(String prefix) {
+                this.prefix = prefix;
+        }
+
+        public String formatString(String body) {
+                return "%s(%s)".formatted(prefix, body);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryTerm.java
new file mode 100644
index 00000000..b78239c7
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryTerm.java
@@ -0,0 +1,51 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+
+import java.util.Objects;
+
+public abstract class ArithmeticUnaryTerm<T> extends UnaryTerm<T, T> {
+        private final ArithmeticUnaryOperator operator;
+
+        protected ArithmeticUnaryTerm(ArithmeticUnaryOperator operator, Term<T> body) {
+                super(body);
+                this.operator = operator;
+        }
+
+        @Override
+        public Class<T> getBodyType() {
+                return getType();
+        }
+
+        public ArithmeticUnaryOperator getOperator() {
+                return operator;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherArithmeticUnaryTerm = (ArithmeticUnaryTerm<?>) other;
+                return operator == otherArithmeticUnaryTerm.operator;
+        }
+
+        @Override
+        public String toString() {
+                return operator.formatString(getBody().toString());
+        }
+
+        @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;
+                ArithmeticUnaryTerm<?> that = (ArithmeticUnaryTerm<?>) o;
+                return operator == that.operator;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), operator);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AssignedValue.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AssignedValue.java
new file mode 100644
index 00000000..465e690f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AssignedValue.java
@@ -0,0 +1,8 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.literal.Literal;
+
+@FunctionalInterface
+public interface AssignedValue<T> {
+        Literal toLiteral(DataVariable<T> targetVariable);
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/BinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/BinaryTerm.java
new file mode 100644
index 00000000..34f48ccc
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/BinaryTerm.java
@@ -0,0 +1,93 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.valuation.Valuation;
+
+import java.util.Collections;
+import java.util.HashSet;
+import java.util.Objects;
+import java.util.Set;
+
+public abstract class BinaryTerm<R, T1, T2> implements Term<R> {
+        private final Term<T1> left;
+        private final Term<T2> right;
+
+        protected BinaryTerm(Term<T1> left, Term<T2> right) {
+                if (!left.getType().equals(getLeftType())) {
+                        throw new IllegalArgumentException("Expected left %s to be of type %s, got %s instead".formatted(left,
+                                        getLeftType().getName(), left.getType().getName()));
+                }
+                if (!right.getType().equals(getRightType())) {
+                        throw new IllegalArgumentException("Expected right %s to be of type %s, got %s instead".formatted(right,
+                                        getRightType().getName(), right.getType().getName()));
+                }
+                this.left = left;
+                this.right = right;
+        }
+
+        public abstract Class<T1> getLeftType();
+
+        public abstract Class<T2> getRightType();
+
+        public Term<T1> getLeft() {
+                return left;
+        }
+
+        public Term<T2> getRight() {
+                return right;
+        }
+
+        @Override
+        public R evaluate(Valuation valuation) {
+                var leftValue = left.evaluate(valuation);
+                if (leftValue == null) {
+                        return null;
+                }
+                var rightValue = right.evaluate(valuation);
+                if (rightValue == null) {
+                        return null;
+                }
+                return doEvaluate(leftValue, rightValue);
+        }
+
+        protected abstract R doEvaluate(T1 leftValue, T2 rightValue);
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                if (getClass() != other.getClass()) {
+                        return false;
+                }
+                var otherBinaryTerm = (BinaryTerm<?, ?, ?>) other;
+                return left.equalsWithSubstitution(helper, otherBinaryTerm.left) && right.equalsWithSubstitution(helper,
+                                otherBinaryTerm.right);
+        }
+
+        @Override
+        public Term<R> substitute(Substitution substitution) {
+                return doSubstitute(substitution, left.substitute(substitution), right.substitute(substitution));
+        }
+
+        public abstract Term<R> doSubstitute(Substitution substitution, Term<T1> substitutedLeft,
+                                                                                 Term<T2> substitutedRight);
+
+        @Override
+        public Set<AnyDataVariable> getInputVariables() {
+                var inputVariables = new HashSet<>(left.getInputVariables());
+                inputVariables.addAll(right.getInputVariables());
+                return Collections.unmodifiableSet(inputVariables);
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                BinaryTerm<?, ?, ?> that = (BinaryTerm<?, ?, ?>) o;
+                return left.equals(that.left) && right.equals(that.right);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(getClass(), left, right);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonOperator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonOperator.java
new file mode 100644
index 00000000..44dcce10
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonOperator.java
@@ -0,0 +1,20 @@
+package tools.refinery.store.query.term;
+
+public enum ComparisonOperator {
+        EQ("=="),
+        NOT_EQ("!="),
+        LESS("<"),
+        LESS_EQ("<="),
+        GREATER(">"),
+        GREATER_EQ(">=");
+
+        private final String text;
+
+        ComparisonOperator(String text) {
+                this.text = text;
+        }
+
+        public String formatString(String left, String right) {
+                return "(%s) %s (%s)".formatted(left, text, right);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonTerm.java
new file mode 100644
index 00000000..320d42df
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonTerm.java
@@ -0,0 +1,63 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+
+import java.util.Objects;
+
+public abstract class ComparisonTerm<T> extends BinaryTerm<Boolean, T, T> {
+        private final ComparisonOperator operator;
+
+        protected ComparisonTerm(ComparisonOperator operator, Term<T> left, Term<T> right) {
+                super(left, right);
+                this.operator = operator;
+        }
+
+        @Override
+        public Class<Boolean> getType() {
+                return Boolean.class;
+        }
+
+        public abstract Class<T> getOperandType();
+
+        @Override
+        public Class<T> getLeftType() {
+                return getOperandType();
+        }
+
+        @Override
+        public Class<T> getRightType() {
+                return getOperandType();
+        }
+
+        public ComparisonOperator getOperator() {
+                return operator;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherComparisonTerm = (ComparisonTerm<?>) other;
+                return operator == otherComparisonTerm.operator;
+        }
+
+        @Override
+        public String toString() {
+                return operator.formatString(getLeft().toString(), getRight().toString());
+        }
+
+        @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;
+                ComparisonTerm<?> that = (ComparisonTerm<?>) o;
+                return operator == that.operator;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), operator);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ConstantTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ConstantTerm.java
new file mode 100644
index 00000000..2185fe37
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ConstantTerm.java
@@ -0,0 +1,52 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.valuation.Valuation;
+
+import java.util.Set;
+
+public record ConstantTerm<T>(Class<T> type, T value) implements Term<T> {
+        public ConstantTerm {
+                if (value == null) {
+                        throw new IllegalArgumentException("value should not be null");
+                }
+                if (!type.isInstance(value)) {
+                        throw new IllegalArgumentException("value %s is not an instance of %s".formatted(value, type.getName()));
+                }
+        }
+
+        @Override
+        public Class<T> getType() {
+                return type;
+        }
+
+        public T getValue() {
+                return value;
+        }
+
+        @Override
+        public T evaluate(Valuation valuation) {
+                return getValue();
+        }
+
+        @Override
+        public Term<T> substitute(Substitution substitution) {
+                return this;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                return equals(other);
+        }
+
+        @Override
+        public Set<AnyDataVariable> getInputVariables() {
+                return Set.of();
+        }
+
+        @Override
+        public String toString() {
+                return getValue().toString();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataSort.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataSort.java
new file mode 100644
index 00000000..4fb44492
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataSort.java
@@ -0,0 +1,29 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+
+public record DataSort<T>(Class<T> type) implements Sort {
+        public static final DataSort<Integer> INT = new DataSort<>(Integer.class);
+
+        public static final DataSort<Boolean> BOOL = new DataSort<>(Boolean.class);
+
+        @Override
+        public boolean isInstance(Variable variable) {
+                return variable instanceof DataVariable<?> dataVariable && type.equals(dataVariable.getType());
+        }
+
+        @Override
+        public DataVariable<T> newInstance(@Nullable String name) {
+                return Variable.of(name, type);
+        }
+
+        @Override
+        public DataVariable<T> newInstance() {
+                return newInstance(null);
+        }
+
+        @Override
+        public String toString() {
+                return type.getName();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java
new file mode 100644
index 00000000..af070ca7
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java
@@ -0,0 +1,87 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.valuation.Valuation;
+
+import java.util.Objects;
+
+public final class DataVariable<T> extends AnyDataVariable implements Term<T> {
+        private final Class<T> type;
+
+        DataVariable(String name, Class<T> type) {
+                super(name);
+                this.type = type;
+        }
+
+        @Override
+        public DataSort<T> getSort() {
+                return new DataSort<>(getType());
+        }
+
+        @Override
+        public Class<T> getType() {
+                return type;
+        }
+
+        @Override
+        public DataVariable<T> renew(@Nullable String name) {
+                return new DataVariable<>(name, type);
+        }
+
+        @Override
+        public DataVariable<T> renew() {
+                return renew(getExplicitName());
+        }
+
+        @Override
+        public NodeVariable asNodeVariable() {
+                throw new IllegalStateException("%s is a data variable".formatted(this));
+        }
+
+        @Override
+        public <U> DataVariable<U> asDataVariable(Class<U> newType) {
+                if (!getType().equals(newType)) {
+                        throw new IllegalStateException("%s is not of type %s but of type %s".formatted(this, newType.getName(),
+                                        getType().getName()));
+                }
+                @SuppressWarnings("unchecked")
+                var result = (DataVariable<U>) this;
+                return result;
+        }
+
+        @Override
+        public T evaluate(Valuation valuation) {
+                return valuation.getValue(this);
+        }
+
+        @Override
+        public Term<T> substitute(Substitution substitution) {
+                return substitution.getTypeSafeSubstitute(this);
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                return other instanceof DataVariable<?> dataVariable && helper.variableEqual(this, dataVariable);
+        }
+
+        public Literal assign(AssignedValue<T> value) {
+                return value.toLiteral(this);
+        }
+
+        @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;
+                DataVariable<?> that = (DataVariable<?>) o;
+                return type.equals(that.type);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), type);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ExtremeValueAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ExtremeValueAggregator.java
new file mode 100644
index 00000000..57ff597c
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ExtremeValueAggregator.java
@@ -0,0 +1,103 @@
+package tools.refinery.store.query.term;
+
+import java.util.Comparator;
+import java.util.Objects;
+import java.util.SortedMap;
+import java.util.TreeMap;
+
+public class ExtremeValueAggregator<T> implements StatefulAggregator<T, T> {
+        private final Class<T> type;
+        private final T emptyResult;
+        private final Comparator<T> comparator;
+
+        public ExtremeValueAggregator(Class<T> type, T emptyResult) {
+                this(type, emptyResult, null);
+        }
+
+        public ExtremeValueAggregator(Class<T> type, T emptyResult, Comparator<T> comparator) {
+                this.type = type;
+                this.emptyResult = emptyResult;
+                this.comparator = comparator;
+        }
+
+        @Override
+        public Class<T> getResultType() {
+                return getInputType();
+        }
+
+        @Override
+        public Class<T> getInputType() {
+                return type;
+        }
+
+        @Override
+        public StatefulAggregate<T, T> createEmptyAggregate() {
+                return new Aggregate();
+        }
+
+        @Override
+        public T getEmptyResult() {
+                return emptyResult;
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                ExtremeValueAggregator<?> that = (ExtremeValueAggregator<?>) o;
+                return type.equals(that.type) && Objects.equals(emptyResult, that.emptyResult) && Objects.equals(comparator,
+                                that.comparator);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(type, emptyResult, comparator);
+        }
+
+        private class Aggregate implements StatefulAggregate<T, T> {
+                private final SortedMap<T, Integer> values;
+
+                private Aggregate() {
+                        values = new TreeMap<>(comparator);
+                }
+
+                private Aggregate(Aggregate other) {
+                        values = new TreeMap<>(other.values);
+                }
+
+                @Override
+                public void add(T value) {
+                        values.compute(value, (ignoredValue, currentCount) -> currentCount == null ? 1 : currentCount + 1);
+                }
+
+                @Override
+                public void remove(T value) {
+                        values.compute(value, (theValue, currentCount) -> {
+                                if (currentCount == null || currentCount <= 0) {
+                                        throw new IllegalStateException("Invalid count %d for value %s".formatted(currentCount, theValue));
+                                }
+                                return currentCount.equals(1) ? null : currentCount - 1;
+                        });
+                }
+
+                @Override
+                public T getResult() {
+                        return isEmpty() ? emptyResult : values.firstKey();
+                }
+
+                @Override
+                public boolean isEmpty() {
+                        return values.isEmpty();
+                }
+
+                @Override
+                public StatefulAggregate<T, T> deepCopy() {
+                        return new Aggregate(this);
+                }
+
+                @Override
+                public boolean contains(T value) {
+                        return StatefulAggregate.super.contains(value);
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeSort.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeSort.java
new file mode 100644
index 00000000..1a4b2d4b
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeSort.java
@@ -0,0 +1,30 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+
+public final class NodeSort implements Sort {
+        public static final NodeSort INSTANCE = new NodeSort();
+
+        private NodeSort() {
+        }
+
+        @Override
+        public boolean isInstance(Variable variable) {
+                return variable instanceof NodeVariable;
+        }
+
+        @Override
+        public NodeVariable newInstance(@Nullable String name) {
+                return new NodeVariable(name);
+        }
+
+        @Override
+        public NodeVariable newInstance() {
+                return newInstance(null);
+        }
+
+        @Override
+        public String toString() {
+                return "<node>";
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java
new file mode 100644
index 00000000..7419aaad
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java
@@ -0,0 +1,48 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.query.literal.ConstantLiteral;
+import tools.refinery.store.query.literal.EquivalenceLiteral;
+
+public final class NodeVariable extends Variable {
+        NodeVariable(@Nullable String name) {
+                super(name);
+        }
+
+        @Override
+        public NodeSort getSort() {
+                return NodeSort.INSTANCE;
+        }
+
+        @Override
+        public NodeVariable renew(@Nullable String name) {
+                return Variable.of(name);
+        }
+
+        @Override
+        public NodeVariable renew() {
+                return renew(getExplicitName());
+        }
+
+        @Override
+        public NodeVariable asNodeVariable() {
+                return this;
+        }
+
+        @Override
+        public <T> DataVariable<T> asDataVariable(Class<T> type) {
+                throw new IllegalStateException("%s is a node variable".formatted(this));
+        }
+
+        public ConstantLiteral isConstant(int value) {
+                return new ConstantLiteral(this, value);
+        }
+
+        public EquivalenceLiteral isEquivalent(NodeVariable other) {
+                return new EquivalenceLiteral(true, this, other);
+        }
+
+        public EquivalenceLiteral notEquivalent(NodeVariable other) {
+                return new EquivalenceLiteral(false, this, other);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/OpaqueTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/OpaqueTerm.java
new file mode 100644
index 00000000..8faa9c75
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/OpaqueTerm.java
@@ -0,0 +1,80 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.substitution.Substitutions;
+import tools.refinery.store.query.valuation.Valuation;
+
+import java.util.Objects;
+import java.util.Set;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+public final class OpaqueTerm<T> implements Term<T> {
+        private final Class<T> type;
+        private final Function<? super Valuation, ? extends T> evaluator;
+        private final Set<AnyDataVariable> variables;
+        private final Substitution substitution;
+
+        public OpaqueTerm(Class<T> type, Function<? super Valuation, ? extends T> evaluator,
+                                          Set<? extends AnyDataVariable> variables) {
+                this(type, evaluator, variables, null);
+        }
+
+        private OpaqueTerm(Class<T> type, Function<? super Valuation, ? extends T> evaluator,
+                                           Set<? extends AnyDataVariable> variables, Substitution substitution) {
+                this.type = type;
+                this.evaluator = evaluator;
+                this.variables = Set.copyOf(variables);
+                this.substitution = substitution;
+        }
+
+        @Override
+        public Class<T> getType() {
+                return type;
+        }
+
+        @Override
+        public Set<AnyDataVariable> getInputVariables() {
+                return variables;
+        }
+
+        @Override
+        public T evaluate(Valuation valuation) {
+                return evaluator.apply(valuation.substitute(substitution));
+        }
+
+        @Override
+        public Term<T> substitute(Substitution newSubstitution) {
+                var substitutedVariables = variables.stream()
+                                .map(newSubstitution::getTypeSafeSubstitute)
+                                .collect(Collectors.toUnmodifiableSet());
+                return new OpaqueTerm<>(type, evaluator, substitutedVariables,
+                                Substitutions.compose(substitution, newSubstitution));
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                // Cannot inspect the opaque evaluator for deep equality.
+                return equals(other);
+        }
+
+        @Override
+        public String toString() {
+                return "<opaque>";
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                OpaqueTerm<?> that = (OpaqueTerm<?>) o;
+                return type.equals(that.type) && evaluator.equals(that.evaluator) && Objects.equals(substitution,
+                                that.substitution);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(type, evaluator, substitution);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Sort.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Sort.java
new file mode 100644
index 00000000..622bcfce
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Sort.java
@@ -0,0 +1,11 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+
+public sealed interface Sort permits DataSort, NodeSort {
+        boolean isInstance(Variable variable);
+
+        Variable newInstance(@Nullable String name);
+
+        Variable newInstance();
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatefulAggregate.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatefulAggregate.java
new file mode 100644
index 00000000..7ce91305
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatefulAggregate.java
@@ -0,0 +1,17 @@
+package tools.refinery.store.query.term;
+
+public interface StatefulAggregate<R, T> {
+        void add(T value);
+
+        void remove(T value);
+
+        R getResult();
+
+        boolean isEmpty();
+
+        StatefulAggregate<R, T> deepCopy();
+
+        default boolean contains(T value) {
+                throw new UnsupportedOperationException();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatefulAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatefulAggregator.java
new file mode 100644
index 00000000..c215a511
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatefulAggregator.java
@@ -0,0 +1,23 @@
+package tools.refinery.store.query.term;
+
+import java.util.stream.Stream;
+
+public interface StatefulAggregator<R, T> extends Aggregator<R, T> {
+        StatefulAggregate<R, T> createEmptyAggregate();
+
+        @Override
+        default R aggregateStream(Stream<T> stream) {
+                var accumulator = createEmptyAggregate();
+                var iterator = stream.iterator();
+                while (iterator.hasNext()) {
+                        var value = iterator.next();
+                        accumulator.add(value);
+                }
+                return accumulator.getResult();
+        }
+
+        @Override
+        default R getEmptyResult() {
+                return createEmptyAggregate().getResult();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatelessAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatelessAggregator.java
new file mode 100644
index 00000000..74dbd335
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/StatelessAggregator.java
@@ -0,0 +1,20 @@
+package tools.refinery.store.query.term;
+
+import java.util.stream.Stream;
+
+public interface StatelessAggregator<R, T> extends Aggregator<R, T> {
+        R add(R current, T value);
+
+        R remove(R current, T value);
+
+        @Override
+        default R aggregateStream(Stream<T> stream) {
+                var accumulator = getEmptyResult();
+                var iterator = stream.iterator();
+                while (iterator.hasNext()) {
+                        var value = iterator.next();
+                        accumulator = add(accumulator, value);
+                }
+                return accumulator;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Term.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Term.java
new file mode 100644
index 00000000..95434db2
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Term.java
@@ -0,0 +1,21 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.literal.AssignLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.valuation.Valuation;
+
+public non-sealed interface Term<T> extends AnyTerm, AssignedValue<T> {
+        @Override
+        Class<T> getType();
+
+        T evaluate(Valuation valuation);
+
+        @Override
+        Term<T> substitute(Substitution substitution);
+
+        @Override
+        default Literal toLiteral(DataVariable<T> targetVariable) {
+                return new AssignLiteral<>(targetVariable, this);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/UnaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/UnaryTerm.java
new file mode 100644
index 00000000..4083111a
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/UnaryTerm.java
@@ -0,0 +1,68 @@
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.valuation.Valuation;
+
+import java.util.Objects;
+import java.util.Set;
+
+public abstract class UnaryTerm<R, T> implements Term<R> {
+        private final Term<T> body;
+
+        protected UnaryTerm(Term<T> body) {
+                if (!body.getType().equals(getBodyType())) {
+                        throw new IllegalArgumentException("Expected body %s to be of type %s, got %s instead".formatted(body,
+                                        getBodyType().getName(), body.getType().getName()));
+                }
+                this.body = body;
+        }
+
+        public abstract Class<T> getBodyType();
+
+        public Term<T> getBody() {
+                return body;
+        }
+
+        @Override
+        public R evaluate(Valuation valuation) {
+                var bodyValue = body.evaluate(valuation);
+                return bodyValue == null ? null : doEvaluate(bodyValue);
+        }
+
+        protected abstract R doEvaluate(T bodyValue);
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                if (getClass() != other.getClass()) {
+                        return false;
+                }
+                var otherUnaryTerm = (UnaryTerm<?, ?>) other;
+                return body.equalsWithSubstitution(helper, otherUnaryTerm.body);
+        }
+
+        @Override
+        public Term<R> substitute(Substitution substitution) {
+                return doSubstitute(substitution, body.substitute(substitution));
+        }
+
+        protected abstract Term<R> doSubstitute(Substitution substitution, Term<T> substitutedBody);
+
+        @Override
+        public Set<AnyDataVariable> getInputVariables() {
+                return body.getInputVariables();
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                UnaryTerm<?, ?> unaryTerm = (UnaryTerm<?, ?>) o;
+                return body.equals(unaryTerm.body);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(getClass(), body);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java
new file mode 100644
index 00000000..957e10f8
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java
@@ -0,0 +1,76 @@
+package tools.refinery.store.query.term;
+
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.query.dnf.DnfUtils;
+
+import java.util.Objects;
+
+public abstract sealed class Variable permits AnyDataVariable, NodeVariable {
+        private final String explicitName;
+        private final String uniqueName;
+
+        protected Variable(String name) {
+                this.explicitName = name;
+                uniqueName = DnfUtils.generateUniqueName(name);
+        }
+
+        public abstract Sort getSort();
+
+        public String getName() {
+                return explicitName == null ? uniqueName : explicitName;
+        }
+
+        protected String getExplicitName() {
+                return explicitName;
+        }
+
+        public boolean isExplicitlyNamed() {
+                return explicitName != null;
+        }
+
+        public String getUniqueName() {
+                return uniqueName;
+        }
+
+        public abstract Variable renew(@Nullable String name);
+
+        public abstract Variable renew();
+
+        public abstract NodeVariable asNodeVariable();
+
+        public abstract <T> DataVariable<T> asDataVariable(Class<T> type);
+
+        @Override
+        public String toString() {
+                return getName();
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                Variable variable = (Variable) o;
+                return Objects.equals(uniqueName, variable.uniqueName);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(uniqueName);
+        }
+
+        public static NodeVariable of(@Nullable String name) {
+                return new NodeVariable(name);
+        }
+
+        public static NodeVariable of() {
+                return of((String) null);
+        }
+
+        public static <T> DataVariable<T> of(@Nullable String name, Class<T> type) {
+                return new DataVariable<>(name, type);
+        }
+
+        public static <T> DataVariable<T> of(Class<T> type) {
+                return of(null, type);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolConstantTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolConstantTerm.java
new file mode 100644
index 00000000..5079f1ce
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolConstantTerm.java
@@ -0,0 +1,16 @@
+package tools.refinery.store.query.term.bool;
+
+import tools.refinery.store.query.term.ConstantTerm;
+
+public final class BoolConstantTerm {
+        public static final ConstantTerm<Boolean> TRUE = new ConstantTerm<>(Boolean.class, true);
+        public static final ConstantTerm<Boolean> FALSE = new ConstantTerm<>(Boolean.class, false);
+
+        private BoolConstantTerm() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static ConstantTerm<Boolean> valueOf(boolean boolValue) {
+                return boolValue ? TRUE : FALSE;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolLogicBinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolLogicBinaryTerm.java
new file mode 100644
index 00000000..d85f864d
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolLogicBinaryTerm.java
@@ -0,0 +1,78 @@
+package tools.refinery.store.query.term.bool;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.*;
+
+import java.util.Objects;
+
+public class BoolLogicBinaryTerm extends BinaryTerm<Boolean, Boolean, Boolean> {
+        private final LogicBinaryOperator operator;
+
+        protected BoolLogicBinaryTerm(LogicBinaryOperator operator, Term<Boolean> left, Term<Boolean> right) {
+                super(left, right);
+                this.operator = operator;
+        }
+
+        @Override
+        public Class<Boolean> getType() {
+                return Boolean.class;
+        }
+
+        @Override
+        public Class<Boolean> getLeftType() {
+                return getType();
+        }
+
+        @Override
+        public Class<Boolean> getRightType() {
+                return getType();
+        }
+
+        public LogicBinaryOperator getOperator() {
+                return operator;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherBoolLogicBinaryTerm = (BoolLogicBinaryTerm) other;
+                return operator == otherBoolLogicBinaryTerm.operator;
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<Boolean> substitutedLeft,
+                                                                          Term<Boolean> substitutedRight) {
+                return new BoolLogicBinaryTerm(getOperator(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Boolean doEvaluate(Boolean leftValue, Boolean rightValue) {
+                return switch (getOperator()) {
+                        case AND -> leftValue && rightValue;
+                        case OR -> leftValue || rightValue;
+                        case XOR -> leftValue ^ rightValue;
+                };
+        }
+
+        @Override
+        public String toString() {
+                return operator.formatString(getLeft().toString(), getRight().toString());
+        }
+
+        @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;
+                BoolLogicBinaryTerm that = (BoolLogicBinaryTerm) o;
+                return operator == that.operator;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), operator);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolNotTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolNotTerm.java
new file mode 100644
index 00000000..855139b5
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolNotTerm.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.query.term.bool;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.UnaryTerm;
+
+public class BoolNotTerm extends UnaryTerm<Boolean, Boolean> {
+        protected BoolNotTerm(Term<Boolean> body) {
+                super(body);
+        }
+
+        @Override
+        public Class<Boolean> getType() {
+                return Boolean.class;
+        }
+
+        @Override
+        public Class<Boolean> getBodyType() {
+                return getType();
+        }
+
+        @Override
+        protected Term<Boolean> doSubstitute(Substitution substitution, Term<Boolean> substitutedBody) {
+                return new BoolNotTerm(substitutedBody);
+        }
+
+        @Override
+        protected Boolean doEvaluate(Boolean bodyValue) {
+                return !bodyValue;
+        }
+
+        @Override
+        public String toString() {
+                return "!(%s)".formatted(getBody());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolTerms.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolTerms.java
new file mode 100644
index 00000000..3d6c8d9d
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolTerms.java
@@ -0,0 +1,30 @@
+package tools.refinery.store.query.term.bool;
+
+import tools.refinery.store.query.term.ConstantTerm;
+import tools.refinery.store.query.term.Term;
+
+public final class BoolTerms {
+        private BoolTerms() {
+                throw new IllegalArgumentException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static ConstantTerm<Boolean> constant(boolean value) {
+                return BoolConstantTerm.valueOf(value);
+        }
+
+        public static BoolNotTerm not(Term<Boolean> body) {
+                return new BoolNotTerm(body);
+        }
+
+        public static BoolLogicBinaryTerm and(Term<Boolean> left, Term<Boolean> right) {
+                return new BoolLogicBinaryTerm(LogicBinaryOperator.AND, left, right);
+        }
+
+        public static BoolLogicBinaryTerm or(Term<Boolean> left, Term<Boolean> right) {
+                return new BoolLogicBinaryTerm(LogicBinaryOperator.OR, left, right);
+        }
+
+        public static BoolLogicBinaryTerm xor(Term<Boolean> left, Term<Boolean> right) {
+                return new BoolLogicBinaryTerm(LogicBinaryOperator.XOR, left, right);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/LogicBinaryOperator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/LogicBinaryOperator.java
new file mode 100644
index 00000000..ca9ac66e
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/LogicBinaryOperator.java
@@ -0,0 +1,17 @@
+package tools.refinery.store.query.term.bool;
+
+public enum LogicBinaryOperator {
+        AND("&&"),
+        OR("||"),
+        XOR("^^");
+
+        private final String text;
+
+        LogicBinaryOperator(String text) {
+                this.text = text;
+        }
+
+        public String formatString(String left, String right) {
+                return "(%s) %s (%s)".formatted(left, text, right);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticBinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticBinaryTerm.java
new file mode 100644
index 00000000..32e41718
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticBinaryTerm.java
@@ -0,0 +1,48 @@
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.ArithmeticBinaryOperator;
+import tools.refinery.store.query.term.ArithmeticBinaryTerm;
+import tools.refinery.store.query.term.Term;
+
+public class IntArithmeticBinaryTerm extends ArithmeticBinaryTerm<Integer> {
+        public IntArithmeticBinaryTerm(ArithmeticBinaryOperator operator, Term<Integer> left, Term<Integer> right) {
+                super(operator, left, right);
+        }
+
+        @Override
+        public Class<Integer> getType() {
+                return Integer.class;
+        }
+
+        @Override
+        public Term<Integer> doSubstitute(Substitution substitution, Term<Integer> substitutedLeft,
+                                                                          Term<Integer> substitutedRight) {
+                return new IntArithmeticBinaryTerm(getOperator(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Integer doEvaluate(Integer leftValue, Integer rightValue) {
+                return switch (getOperator()) {
+                        case ADD -> leftValue + rightValue;
+                        case SUB -> leftValue - rightValue;
+                        case MUL -> leftValue * rightValue;
+                        case DIV -> rightValue == 0 ? null : leftValue / rightValue;
+                        case POW -> rightValue < 0 ? null : power(leftValue, rightValue);
+                        case MIN -> Math.min(leftValue, rightValue);
+                        case MAX -> Math.max(leftValue, rightValue);
+                };
+        }
+
+        private static int power(int base, int exponent) {
+                int accum = 1;
+                while (exponent > 0) {
+                        if (exponent % 2 == 1) {
+                                accum = accum * base;
+                        }
+                        base = base * base;
+                        exponent = exponent / 2;
+                }
+                return accum;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticUnaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticUnaryTerm.java
new file mode 100644
index 00000000..1e769259
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticUnaryTerm.java
@@ -0,0 +1,30 @@
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.ArithmeticUnaryOperator;
+import tools.refinery.store.query.term.ArithmeticUnaryTerm;
+
+public class IntArithmeticUnaryTerm extends ArithmeticUnaryTerm<Integer> {
+        public IntArithmeticUnaryTerm(ArithmeticUnaryOperator operation, Term<Integer> body) {
+                super(operation, body);
+        }
+
+        @Override
+        public Class<Integer> getType() {
+                return Integer.class;
+        }
+
+        @Override
+        protected Term<Integer> doSubstitute(Substitution substitution, Term<Integer> substitutedBody) {
+                return new IntArithmeticUnaryTerm(getOperator(), substitutedBody);
+        }
+
+        @Override
+        protected Integer doEvaluate(Integer bodyValue) {
+                return switch(getOperator()) {
+                        case PLUS -> bodyValue;
+                        case MINUS -> -bodyValue;
+                };
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntComparisonTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntComparisonTerm.java
new file mode 100644
index 00000000..322d2b80
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntComparisonTerm.java
@@ -0,0 +1,34 @@
+package tools.refinery.store.query.term.int_;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.ComparisonOperator;
+import tools.refinery.store.query.term.ComparisonTerm;
+import tools.refinery.store.query.term.Term;
+
+public class IntComparisonTerm extends ComparisonTerm<Integer> {
+        public IntComparisonTerm(ComparisonOperator operator, Term<Integer> left, Term<Integer> right) {
+                super(operator, left, right);
+        }
+
+        @Override
+        public Class<Integer> getOperandType() {
+                return Integer.class;
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<Integer> substitutedLeft,
+                                                                          Term<Integer> substitutedRight) {
+                return new IntComparisonTerm(getOperator(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Boolean doEvaluate(Integer leftValue, Integer rightValue) {
+                return switch (getOperator()) {
+                        case EQ -> leftValue.equals(rightValue);
+                        case NOT_EQ -> !leftValue.equals(rightValue);
+                        case LESS -> leftValue < rightValue;
+                        case LESS_EQ -> leftValue <= rightValue;
+                        case GREATER -> leftValue > rightValue;
+                        case GREATER_EQ -> leftValue >= rightValue;
+                };
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntExtremeValueAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntExtremeValueAggregator.java
new file mode 100644
index 00000000..d5a6add0
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntExtremeValueAggregator.java
@@ -0,0 +1,17 @@
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.term.ExtremeValueAggregator;
+
+import java.util.Comparator;
+
+public final class IntExtremeValueAggregator {
+        public static final ExtremeValueAggregator<Integer> MINIMUM = new ExtremeValueAggregator<>(Integer.class,
+                        Integer.MAX_VALUE);
+
+        public static final ExtremeValueAggregator<Integer> MAXIMUM = new ExtremeValueAggregator<>(Integer.class,
+                        Integer.MIN_VALUE, Comparator.reverseOrder());
+
+        private IntExtremeValueAggregator() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntSumAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntSumAggregator.java
new file mode 100644
index 00000000..65024f52
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntSumAggregator.java
@@ -0,0 +1,35 @@
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.term.StatelessAggregator;
+
+public final class IntSumAggregator implements StatelessAggregator<Integer, Integer> {
+        public static final IntSumAggregator INSTANCE = new IntSumAggregator();
+
+        private IntSumAggregator() {
+        }
+
+        @Override
+        public Class<Integer> getResultType() {
+                return Integer.class;
+        }
+
+        @Override
+        public Class<Integer> getInputType() {
+                return Integer.class;
+        }
+
+        @Override
+        public Integer getEmptyResult() {
+                return 0;
+        }
+
+        @Override
+        public Integer add(Integer current, Integer value) {
+                return current + value;
+        }
+
+        @Override
+        public Integer remove(Integer current, Integer value) {
+                return current - value;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntTerms.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntTerms.java
new file mode 100644
index 00000000..86594deb
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntTerms.java
@@ -0,0 +1,81 @@
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.term.*;
+
+public final class IntTerms {
+        public static final Aggregator<Integer, Integer> INT_SUM = IntSumAggregator.INSTANCE;
+        public static final Aggregator<Integer, Integer> INT_MIN = IntExtremeValueAggregator.MINIMUM;
+        public static final Aggregator<Integer, Integer> INT_MAX = IntExtremeValueAggregator.MAXIMUM;
+
+        private IntTerms() {
+                throw new IllegalArgumentException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static ConstantTerm<Integer> constant(int value) {
+                return new ConstantTerm<>(Integer.class, value);
+        }
+
+        public static IntArithmeticUnaryTerm plus(Term<Integer> body) {
+                return new IntArithmeticUnaryTerm(ArithmeticUnaryOperator.PLUS, body);
+        }
+
+        public static IntArithmeticUnaryTerm minus(Term<Integer> body) {
+                return new IntArithmeticUnaryTerm(ArithmeticUnaryOperator.MINUS, body);
+        }
+
+        public static IntArithmeticBinaryTerm add(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.ADD, left, right);
+        }
+
+        public static IntArithmeticBinaryTerm sub(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.SUB, left, right);
+        }
+
+        public static IntArithmeticBinaryTerm mul(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.MUL, left, right);
+        }
+
+        public static IntArithmeticBinaryTerm div(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.DIV, left, right);
+        }
+
+        public static IntArithmeticBinaryTerm pow(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.POW, left, right);
+        }
+
+        public static IntArithmeticBinaryTerm min(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.MIN, left, right);
+        }
+
+        public static IntArithmeticBinaryTerm max(Term<Integer> left, Term<Integer> right) {
+                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.MAX, left, right);
+        }
+
+        public static IntComparisonTerm eq(Term<Integer> left, Term<Integer> right) {
+                return new IntComparisonTerm(ComparisonOperator.EQ, left, right);
+        }
+
+        public static IntComparisonTerm notEq(Term<Integer> left, Term<Integer> right) {
+                return new IntComparisonTerm(ComparisonOperator.NOT_EQ, left, right);
+        }
+
+        public static IntComparisonTerm less(Term<Integer> left, Term<Integer> right) {
+                return new IntComparisonTerm(ComparisonOperator.LESS, left, right);
+        }
+
+        public static IntComparisonTerm lessEq(Term<Integer> left, Term<Integer> right) {
+                return new IntComparisonTerm(ComparisonOperator.LESS_EQ, left, right);
+        }
+
+        public static IntComparisonTerm greater(Term<Integer> left, Term<Integer> right) {
+                return new IntComparisonTerm(ComparisonOperator.GREATER, left, right);
+        }
+
+        public static IntComparisonTerm greaterEq(Term<Integer> left, Term<Integer> right) {
+                return new IntComparisonTerm(ComparisonOperator.GREATER_EQ, left, right);
+        }
+
+        public static RealToIntTerm asInt(Term<Double> body) {
+                return new RealToIntTerm(body);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/RealToIntTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/RealToIntTerm.java
new file mode 100644
index 00000000..53875ddc
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/RealToIntTerm.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.UnaryTerm;
+
+public class RealToIntTerm extends UnaryTerm<Integer, Double> {
+        protected RealToIntTerm(Term<Double> body) {
+                super(body);
+        }
+
+        @Override
+        public Class<Integer> getType() {
+                return Integer.class;
+        }
+
+        @Override
+        public Class<Double> getBodyType() {
+                return Double.class;
+        }
+
+        @Override
+        protected Integer doEvaluate(Double bodyValue) {
+                return bodyValue.intValue();
+        }
+
+        @Override
+        protected Term<Integer> doSubstitute(Substitution substitution, Term<Double> substitutedBody) {
+                return new RealToIntTerm(substitutedBody);
+        }
+
+        @Override
+        public String toString() {
+                return "(%s) as int".formatted(getBody());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/IntToRealTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/IntToRealTerm.java
new file mode 100644
index 00000000..55590824
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/IntToRealTerm.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.UnaryTerm;
+
+public class IntToRealTerm extends UnaryTerm<Double, Integer> {
+        protected IntToRealTerm(Term<Integer> body) {
+                super(body);
+        }
+
+        @Override
+        public Class<Double> getType() {
+                return Double.class;
+        }
+
+        @Override
+        public Class<Integer> getBodyType() {
+                return Integer.class;
+        }
+
+        @Override
+        protected Term<Double> doSubstitute(Substitution substitution, Term<Integer> substitutedBody) {
+                return new IntToRealTerm(substitutedBody);
+        }
+
+        @Override
+        protected Double doEvaluate(Integer bodyValue) {
+                return bodyValue.doubleValue();
+        }
+
+        @Override
+        public String toString() {
+                return "(%s) as real".formatted(getBody());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticBinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticBinaryTerm.java
new file mode 100644
index 00000000..57bcbe5e
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticBinaryTerm.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.ArithmeticBinaryOperator;
+import tools.refinery.store.query.term.ArithmeticBinaryTerm;
+import tools.refinery.store.query.term.Term;
+
+public class RealArithmeticBinaryTerm extends ArithmeticBinaryTerm<Double> {
+        public RealArithmeticBinaryTerm(ArithmeticBinaryOperator operator, Term<Double> left, Term<Double> right) {
+                super(operator, left, right);
+        }
+
+        @Override
+        public Class<Double> getType() {
+                return Double.class;
+        }
+
+        @Override
+        public Term<Double> doSubstitute(Substitution substitution, Term<Double> substitutedLeft,
+                                                                         Term<Double> substitutedRight) {
+                return new RealArithmeticBinaryTerm(getOperator(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Double doEvaluate(Double leftValue, Double rightValue) {
+                return switch (getOperator()) {
+                        case ADD -> leftValue + rightValue;
+                        case SUB -> leftValue - rightValue;
+                        case MUL -> leftValue * rightValue;
+                        case DIV -> leftValue / rightValue;
+                        case POW -> Math.pow(leftValue, rightValue);
+                        case MIN -> Math.min(leftValue, rightValue);
+                        case MAX -> Math.max(leftValue, rightValue);
+                };
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticUnaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticUnaryTerm.java
new file mode 100644
index 00000000..632e68bf
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticUnaryTerm.java
@@ -0,0 +1,30 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.ArithmeticUnaryOperator;
+import tools.refinery.store.query.term.ArithmeticUnaryTerm;
+import tools.refinery.store.query.term.Term;
+
+public class RealArithmeticUnaryTerm extends ArithmeticUnaryTerm<Double> {
+        public RealArithmeticUnaryTerm(ArithmeticUnaryOperator operation, Term<Double> body) {
+                super(operation, body);
+        }
+
+        @Override
+        public Class<Double> getType() {
+                return Double.class;
+        }
+
+        @Override
+        protected Term<Double> doSubstitute(Substitution substitution, Term<Double> substitutedBody) {
+                return new RealArithmeticUnaryTerm(getOperator(), substitutedBody);
+        }
+
+        @Override
+        protected Double doEvaluate(Double bodyValue) {
+                return switch(getOperator()) {
+                        case PLUS -> bodyValue;
+                        case MINUS -> -bodyValue;
+                };
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealComparisonTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealComparisonTerm.java
new file mode 100644
index 00000000..75d97adb
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealComparisonTerm.java
@@ -0,0 +1,35 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.ComparisonOperator;
+import tools.refinery.store.query.term.ComparisonTerm;
+import tools.refinery.store.query.term.Term;
+
+public class RealComparisonTerm extends ComparisonTerm<Double> {
+        public RealComparisonTerm(ComparisonOperator operator, Term<Double> left, Term<Double> right) {
+                super(operator, left, right);
+        }
+
+        @Override
+        public Class<Double> getOperandType() {
+                return Double.class;
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<Double> substitutedLeft,
+                                                                          Term<Double> substitutedRight) {
+                return new RealComparisonTerm(getOperator(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Boolean doEvaluate(Double leftValue, Double rightValue) {
+                return switch (getOperator()) {
+                        case EQ -> leftValue.equals(rightValue);
+                        case NOT_EQ -> !leftValue.equals(rightValue);
+                        case LESS -> leftValue < rightValue;
+                        case LESS_EQ -> leftValue <= rightValue;
+                        case GREATER -> leftValue > rightValue;
+                        case GREATER_EQ -> leftValue >= rightValue;
+                };
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealExtremeValueAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealExtremeValueAggregator.java
new file mode 100644
index 00000000..23384530
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealExtremeValueAggregator.java
@@ -0,0 +1,17 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.term.ExtremeValueAggregator;
+
+import java.util.Comparator;
+
+public final class RealExtremeValueAggregator {
+        public static final ExtremeValueAggregator<Double> MINIMUM = new ExtremeValueAggregator<>(Double.class,
+                        Double.POSITIVE_INFINITY);
+
+        public static final ExtremeValueAggregator<Double> MAXIMUM = new ExtremeValueAggregator<>(Double.class,
+                        Double.NEGATIVE_INFINITY, Comparator.reverseOrder());
+
+        private RealExtremeValueAggregator() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealSumAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealSumAggregator.java
new file mode 100644
index 00000000..d5888664
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealSumAggregator.java
@@ -0,0 +1,85 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.term.StatefulAggregate;
+import tools.refinery.store.query.term.StatefulAggregator;
+
+import java.util.Map;
+import java.util.TreeMap;
+
+public final class RealSumAggregator implements StatefulAggregator<Double, Double> {
+        public static final RealSumAggregator INSTANCE = new RealSumAggregator();
+
+        private RealSumAggregator() {
+        }
+
+        @Override
+        public Class<Double> getResultType() {
+                return null;
+        }
+
+        @Override
+        public Class<Double> getInputType() {
+                return null;
+        }
+
+        @Override
+        public StatefulAggregate<Double, Double> createEmptyAggregate() {
+                return new Aggregate();
+        }
+
+        @Override
+        public Double getEmptyResult() {
+                return 0d;
+        }
+
+        private static class Aggregate implements StatefulAggregate<Double, Double> {
+                private final Map<Double, Integer> values;
+
+                public Aggregate() {
+                        values = new TreeMap<>();
+                }
+
+                private Aggregate(Aggregate other) {
+                        values = new TreeMap<>(other.values);
+                }
+
+                @Override
+                public void add(Double value) {
+                        values.compute(value, (ignoredValue, currentCount) -> currentCount == null ? 1 : currentCount + 1);
+                }
+
+                @Override
+                public void remove(Double value) {
+                        values.compute(value, (theValue, currentCount) -> {
+                                if (currentCount == null || currentCount <= 0) {
+                                        throw new IllegalStateException("Invalid count %d for value %f".formatted(currentCount, theValue));
+                                }
+                                return currentCount.equals(1) ? null : currentCount - 1;
+                        });
+                }
+
+                @Override
+                public Double getResult() {
+                        return values.entrySet()
+                                        .stream()
+                                        .mapToDouble(entry -> entry.getKey() * entry.getValue())
+                                        .reduce(Double::sum)
+                                        .orElse(0d);
+                }
+
+                @Override
+                public boolean isEmpty() {
+                        return values.isEmpty();
+                }
+
+                @Override
+                public StatefulAggregate<Double, Double> deepCopy() {
+                        return new Aggregate(this);
+                }
+
+                @Override
+                public boolean contains(Double value) {
+                        return values.containsKey(value);
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealTerms.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealTerms.java
new file mode 100644
index 00000000..a8117842
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealTerms.java
@@ -0,0 +1,81 @@
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.term.*;
+
+public final class RealTerms {
+        public static final Aggregator<Double, Double> REAL_SUM = RealSumAggregator.INSTANCE;
+        public static final Aggregator<Double, Double> REAL_MIN = RealExtremeValueAggregator.MINIMUM;
+        public static final Aggregator<Double, Double> REAL_MAX = RealExtremeValueAggregator.MAXIMUM;
+
+        private RealTerms() {
+                throw new IllegalArgumentException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static ConstantTerm<Double> constant(double value) {
+                return new ConstantTerm<>(Double.class, value);
+        }
+
+        public static RealArithmeticUnaryTerm plus(Term<Double> body) {
+                return new RealArithmeticUnaryTerm(ArithmeticUnaryOperator.PLUS, body);
+        }
+
+        public static RealArithmeticUnaryTerm minus(Term<Double> body) {
+                return new RealArithmeticUnaryTerm(ArithmeticUnaryOperator.MINUS, body);
+        }
+
+        public static RealArithmeticBinaryTerm add(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.ADD, left, right);
+        }
+
+        public static RealArithmeticBinaryTerm sub(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.SUB, left, right);
+        }
+
+        public static RealArithmeticBinaryTerm mul(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.MUL, left, right);
+        }
+
+        public static RealArithmeticBinaryTerm div(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.DIV, left, right);
+        }
+
+        public static RealArithmeticBinaryTerm pow(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.POW, left, right);
+        }
+
+        public static RealArithmeticBinaryTerm min(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.MIN, left, right);
+        }
+
+        public static RealArithmeticBinaryTerm max(Term<Double> left, Term<Double> right) {
+                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.MAX, left, right);
+        }
+
+        public static RealComparisonTerm eq(Term<Double> left, Term<Double> right) {
+                return new RealComparisonTerm(ComparisonOperator.EQ, left, right);
+        }
+
+        public static RealComparisonTerm notEq(Term<Double> left, Term<Double> right) {
+                return new RealComparisonTerm(ComparisonOperator.NOT_EQ, left, right);
+        }
+
+        public static RealComparisonTerm less(Term<Double> left, Term<Double> right) {
+                return new RealComparisonTerm(ComparisonOperator.LESS, left, right);
+        }
+
+        public static RealComparisonTerm lessEq(Term<Double> left, Term<Double> right) {
+                return new RealComparisonTerm(ComparisonOperator.LESS_EQ, left, right);
+        }
+
+        public static RealComparisonTerm greater(Term<Double> left, Term<Double> right) {
+                return new RealComparisonTerm(ComparisonOperator.GREATER, left, right);
+        }
+
+        public static RealComparisonTerm greaterEq(Term<Double> left, Term<Double> right) {
+                return new RealComparisonTerm(ComparisonOperator.GREATER_EQ, left, right);
+        }
+
+        public static IntToRealTerm asReal(Term<Integer> body) {
+                return new IntToRealTerm(body);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/RestrictedValuation.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/RestrictedValuation.java
new file mode 100644
index 00000000..fb512d88
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/RestrictedValuation.java
@@ -0,0 +1,16 @@
+package tools.refinery.store.query.valuation;
+
+import tools.refinery.store.query.term.AnyDataVariable;
+import tools.refinery.store.query.term.DataVariable;
+
+import java.util.Set;
+
+public record RestrictedValuation(Valuation valuation, Set<AnyDataVariable> allowedVariables) implements Valuation {
+        @Override
+        public <T> T getValue(DataVariable<T> variable) {
+                if (!allowedVariables.contains(variable)) {
+                        throw new IllegalArgumentException("Variable %s is not in scope".formatted(variable));
+                }
+                return valuation.getValue(variable);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/SubstitutedValuation.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/SubstitutedValuation.java
new file mode 100644
index 00000000..8e79663c
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/SubstitutedValuation.java
@@ -0,0 +1,11 @@
+package tools.refinery.store.query.valuation;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.DataVariable;
+
+public record SubstitutedValuation(Valuation originalValuation, Substitution substitution) implements Valuation {
+        @Override
+        public <T> T getValue(DataVariable<T> variable) {
+                return originalValuation.getValue(substitution.getTypeSafeSubstitute(variable));
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/Valuation.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/Valuation.java
new file mode 100644
index 00000000..3ba9a6b8
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/Valuation.java
@@ -0,0 +1,23 @@
+package tools.refinery.store.query.valuation;
+
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.AnyDataVariable;
+import tools.refinery.store.query.term.DataVariable;
+
+import java.util.Set;
+
+public interface Valuation {
+        <T> T getValue(DataVariable<T> variable);
+
+        default Valuation substitute(@Nullable Substitution substitution) {
+                if (substitution == null) {
+                        return this;
+                }
+                return new SubstitutedValuation(this, substitution);
+        }
+
+        default Valuation restrict(Set<? extends AnyDataVariable> allowedVariables) {
+                return new RestrictedValuation(this, Set.copyOf(allowedVariables));
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java
new file mode 100644
index 00000000..6ae410f2
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java
@@ -0,0 +1,26 @@
+package tools.refinery.store.query.view;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.dnf.FunctionalDependency;
+import tools.refinery.store.representation.AnySymbol;
+import tools.refinery.store.query.Constraint;
+
+import java.util.Set;
+
+public sealed interface AnyRelationView extends Constraint permits RelationView {
+        AnySymbol getSymbol();
+
+        String getViewName();
+
+        default Set<FunctionalDependency<Integer>> getFunctionalDependencies() {
+                return Set.of();
+        }
+
+        default Set<RelationViewImplication> getImpliedRelationViews() {
+                return Set.of();
+        }
+
+        boolean get(Model model, Object[] tuple);
+
+        Iterable<Object[]> getAll(Model model);
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java
new file mode 100644
index 00000000..64c601bb
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FilteredRelationView.java
@@ -0,0 +1,49 @@
+package tools.refinery.store.query.view;
+
+import tools.refinery.store.tuple.Tuple;
+import tools.refinery.store.representation.Symbol;
+
+import java.util.Objects;
+import java.util.function.BiPredicate;
+import java.util.function.Predicate;
+
+public class FilteredRelationView<T> extends TuplePreservingRelationView<T> {
+        private final BiPredicate<Tuple, T> predicate;
+
+        public FilteredRelationView(Symbol<T> symbol, String name, BiPredicate<Tuple, T> predicate) {
+                super(symbol, name);
+                this.predicate = predicate;
+        }
+
+        public FilteredRelationView(Symbol<T> symbol, BiPredicate<Tuple, T> predicate) {
+                super(symbol);
+                this.predicate = predicate;
+        }
+
+        public FilteredRelationView(Symbol<T> symbol, String name, Predicate<T> predicate) {
+                this(symbol, name, (k, v) -> predicate.test(v));
+        }
+
+        public FilteredRelationView(Symbol<T> symbol, Predicate<T> predicate) {
+                this(symbol, (k, v) -> predicate.test(v));
+        }
+
+        @Override
+        public boolean filter(Tuple key, T value) {
+                return this.predicate.test(key, value);
+        }
+
+        @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;
+                FilteredRelationView<?> that = (FilteredRelationView<?>) o;
+                return Objects.equals(predicate, that.predicate);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), predicate);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/ForbiddenRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/ForbiddenRelationView.java
new file mode 100644
index 00000000..050b9496
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/ForbiddenRelationView.java
@@ -0,0 +1,16 @@
+package tools.refinery.store.query.view;
+
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+public class ForbiddenRelationView extends TuplePreservingRelationView<TruthValue> {
+        public ForbiddenRelationView(Symbol<TruthValue> symbol) {
+                super(symbol, "forbidden");
+        }
+
+        @Override
+        public boolean filter(Tuple key, TruthValue value) {
+                return !value.may();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java
new file mode 100644
index 00000000..7ec9e7ac
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionalRelationView.java
@@ -0,0 +1,105 @@
+package tools.refinery.store.query.view;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.dnf.FunctionalDependency;
+import tools.refinery.store.query.term.DataSort;
+import tools.refinery.store.query.term.NodeSort;
+import tools.refinery.store.query.term.Sort;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+import tools.refinery.store.tuple.Tuple1;
+
+import java.util.List;
+import java.util.Objects;
+import java.util.Set;
+import java.util.stream.Collectors;
+import java.util.stream.IntStream;
+
+public final class FunctionalRelationView<T> extends RelationView<T> {
+        private final T defaultValue;
+
+        public FunctionalRelationView(Symbol<T> symbol, String name) {
+                super(symbol, name);
+                defaultValue = symbol.defaultValue();
+        }
+
+        public FunctionalRelationView(Symbol<T> symbol) {
+                super(symbol);
+                defaultValue = symbol.defaultValue();
+        }
+
+        @Override
+        public Set<FunctionalDependency<Integer>> getFunctionalDependencies() {
+                var arity = getSymbol().arity();
+                var forEach = IntStream.range(0, arity).boxed().collect(Collectors.toUnmodifiableSet());
+                var unique = Set.of(arity);
+                return Set.of(new FunctionalDependency<>(forEach, unique));
+        }
+
+        @Override
+        public Set<RelationViewImplication> getImpliedRelationViews() {
+                var symbol = getSymbol();
+                var impliedIndices = IntStream.range(0, symbol.arity()).boxed().toList();
+                var keyOnlyRelationView = new KeyOnlyRelationView<>(symbol);
+                return Set.of(new RelationViewImplication(this, keyOnlyRelationView, impliedIndices));
+        }
+
+        @Override
+        public boolean filter(Tuple key, T value) {
+                return !Objects.equals(defaultValue, value);
+        }
+
+        @Override
+        public Object[] forwardMap(Tuple key, T value) {
+                int size = key.getSize();
+                Object[] result = new Object[size + 1];
+                for (int i = 0; i < size; i++) {
+                        result[i] = Tuple.of(key.get(i));
+                }
+                result[key.getSize()] = value;
+                return result;
+        }
+
+        @Override
+        public boolean get(Model model, Object[] tuple) {
+                int[] content = new int[tuple.length - 1];
+                for (int i = 0; i < tuple.length - 1; i++) {
+                        content[i] = ((Tuple1) tuple[i]).value0();
+                }
+                Tuple key = Tuple.of(content);
+                @SuppressWarnings("unchecked")
+                T valueInTuple = (T) tuple[tuple.length - 1];
+                T valueInMap = model.getInterpretation(getSymbol()).get(key);
+                return valueInTuple.equals(valueInMap);
+        }
+
+        @Override
+        public int arity() {
+                return getSymbol().arity() + 1;
+        }
+
+        @Override
+        public List<Sort> getSorts() {
+                var sorts = new Sort[arity()];
+                int valueIndex = sorts.length - 1;
+                for (int i = 0; i < valueIndex; i++) {
+                        sorts[i] = NodeSort.INSTANCE;
+                }
+                sorts[valueIndex] = new DataSort<>(getSymbol().valueType());
+                return List.of(sorts);
+        }
+
+        @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;
+                FunctionalRelationView<?> that = (FunctionalRelationView<?>) o;
+                return Objects.equals(defaultValue, that.defaultValue);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), defaultValue);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java
new file mode 100644
index 00000000..e1b2e45b
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/KeyOnlyRelationView.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.query.view;
+
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.Objects;
+
+public final class KeyOnlyRelationView<T> extends TuplePreservingRelationView<T> {
+        public static final String VIEW_NAME = "key";
+
+        private final T defaultValue;
+
+        public KeyOnlyRelationView(Symbol<T> symbol) {
+                super(symbol, VIEW_NAME);
+                defaultValue = symbol.defaultValue();
+        }
+
+        @Override
+        public boolean filter(Tuple key, T value) {
+                return !Objects.equals(value, defaultValue);
+        }
+
+        @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;
+                KeyOnlyRelationView<?> that = (KeyOnlyRelationView<?>) o;
+                return Objects.equals(defaultValue, that.defaultValue);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), defaultValue);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/MayRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/MayRelationView.java
new file mode 100644
index 00000000..a2a84b3c
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/MayRelationView.java
@@ -0,0 +1,16 @@
+package tools.refinery.store.query.view;
+
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+public class MayRelationView extends TuplePreservingRelationView<TruthValue> {
+        public MayRelationView(Symbol<TruthValue> symbol) {
+                super(symbol, "may");
+        }
+
+        @Override
+        public boolean filter(Tuple key, TruthValue value) {
+                return value.may();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/MustRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/MustRelationView.java
new file mode 100644
index 00000000..72ac0ca3
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/MustRelationView.java
@@ -0,0 +1,16 @@
+package tools.refinery.store.query.view;
+
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.representation.TruthValue;
+import tools.refinery.store.tuple.Tuple;
+
+public class MustRelationView extends TuplePreservingRelationView<TruthValue> {
+        public MustRelationView(Symbol<TruthValue> symbol) {
+                super(symbol, "must");
+        }
+
+        @Override
+        public boolean filter(Tuple key, TruthValue value) {
+                return value.must();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java
new file mode 100644
index 00000000..d7164b3b
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java
@@ -0,0 +1,77 @@
+package tools.refinery.store.query.view;
+
+import tools.refinery.store.map.CursorAsIterator;
+import tools.refinery.store.model.Model;
+import tools.refinery.store.representation.Symbol;
+import tools.refinery.store.tuple.Tuple;
+
+import java.util.Objects;
+import java.util.UUID;
+
+/**
+ * Represents a view of a {@link Symbol} that can be queried.
+ *
+ * @param <T>
+ * @author Oszkar Semerath
+ */
+public abstract non-sealed class RelationView<T> implements AnyRelationView {
+        private final Symbol<T> symbol;
+
+        private final String viewName;
+
+        protected RelationView(Symbol<T> symbol, String viewName) {
+                this.symbol = symbol;
+                this.viewName = viewName;
+        }
+
+        protected RelationView(Symbol<T> representation) {
+                this(representation, UUID.randomUUID().toString());
+        }
+
+        @Override
+        public Symbol<T> getSymbol() {
+                return symbol;
+        }
+
+        @Override
+        public String getViewName() {
+                return viewName;
+        }
+
+        @Override
+        public String name() {
+                return symbol.name() + "#" + viewName;
+        }
+
+        public abstract boolean filter(Tuple key, T value);
+
+        public abstract Object[] forwardMap(Tuple key, T value);
+
+        @Override
+        public Iterable<Object[]> getAll(Model model) {
+                return (() -> new CursorAsIterator<>(model.getInterpretation(symbol).getAll(), this::forwardMap, this::filter));
+        }
+
+        @Override
+        public String toString() {
+                return name();
+        }
+
+        @Override
+        public String toReferenceString() {
+                return "@RelationView(\"%s\") %s".formatted(viewName, symbol.name());
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                RelationView<?> that = (RelationView<?>) o;
+                return Objects.equals(symbol, that.symbol) && Objects.equals(viewName, that.viewName);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(symbol, viewName);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java
new file mode 100644
index 00000000..2ba1fcc4
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationViewImplication.java
@@ -0,0 +1,19 @@
+package tools.refinery.store.query.view;
+
+import java.util.List;
+
+public record RelationViewImplication(AnyRelationView implyingRelationView, AnyRelationView impliedRelationView,
+                                                                          List<Integer> impliedIndices) {
+        public RelationViewImplication {
+                if (impliedIndices.size() != impliedRelationView.arity()) {
+                        throw new IllegalArgumentException("Expected %d implied indices for %s, but %d are provided"
+                                        .formatted(impliedRelationView.arity(), impliedRelationView, impliedIndices.size()));
+                }
+                for (var index : impliedIndices) {
+                        if (impliedRelationView.invalidIndex(index)) {
+                                throw new IllegalArgumentException("%d is not a valid index for %s".formatted(index,
+                                                implyingRelationView));
+                        }
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java
new file mode 100644
index 00000000..234b3a9a
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingRelationView.java
@@ -0,0 +1,57 @@
+package tools.refinery.store.query.view;
+
+import tools.refinery.store.model.Model;
+import tools.refinery.store.query.term.NodeSort;
+import tools.refinery.store.query.term.Sort;
+import tools.refinery.store.tuple.Tuple;
+import tools.refinery.store.tuple.Tuple1;
+import tools.refinery.store.representation.Symbol;
+
+import java.util.Arrays;
+import java.util.List;
+
+public abstract class TuplePreservingRelationView<T> extends RelationView<T> {
+        protected TuplePreservingRelationView(Symbol<T> symbol, String name) {
+                super(symbol, name);
+        }
+
+        protected TuplePreservingRelationView(Symbol<T> symbol) {
+                super(symbol);
+        }
+
+        public Object[] forwardMap(Tuple key) {
+                Object[] result = new Object[key.getSize()];
+                for (int i = 0; i < key.getSize(); i++) {
+                        result[i] = Tuple.of(key.get(i));
+                }
+                return result;
+        }
+
+        @Override
+        public Object[] forwardMap(Tuple key, T value) {
+                return forwardMap(key);
+        }
+
+        @Override
+        public boolean get(Model model, Object[] tuple) {
+                int[] content = new int[tuple.length];
+                for (int i = 0; i < tuple.length; i++) {
+                        content[i] = ((Tuple1) tuple[i]).value0();
+                }
+                Tuple key = Tuple.of(content);
+                T value = model.getInterpretation(getSymbol()).get(key);
+                return filter(key, value);
+        }
+
+        @Override
+        public int arity() {
+                return this.getSymbol().arity();
+        }
+
+        @Override
+        public List<Sort> getSorts() {
+                var sorts = new Sort[arity()];
+                Arrays.fill(sorts, NodeSort.INSTANCE);
+                return List.of(sorts);
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java
new file mode 100644
index 00000000..ceb46d6f
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java
@@ -0,0 +1,220 @@
+package tools.refinery.store.query;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.literal.BooleanLiteral;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.view.KeyOnlyRelationView;
+import tools.refinery.store.representation.Symbol;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static tools.refinery.store.query.literal.Literals.not;
+import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo;
+
+class DnfBuilderTest {
+        @Test
+        void eliminateTrueTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(BooleanLiteral.TRUE, friendView.call(p, q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateFalseTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(friendView.call(q, p), BooleanLiteral.FALSE)
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysTrueTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(BooleanLiteral.TRUE)
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause().build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysFalseTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q), BooleanLiteral.FALSE)
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateTrueDnfTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var trueDnf = Dnf.builder().parameter(p).clause().build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(trueDnf.call(q), friendView.call(p, q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateFalseDnfTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var falseDnf = Dnf.builder().parameter(p).build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(friendView.call(q, p), falseDnf.call(q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysTrueDnfTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var trueDnf = Dnf.builder().parameter(p).clause().build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(trueDnf.call(q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause().build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysFalseDnfTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var falseDnf = Dnf.builder().parameter(p).build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q), falseDnf.call(q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateNotFalseDnfTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var falseDnf = Dnf.builder().parameter(p).build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(not(falseDnf.call(q)), friendView.call(p, q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateNotTrueDnfTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var trueDnf = Dnf.builder().parameter(p).clause().build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(friendView.call(q, p), not(trueDnf.call(q)))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysNotFalseDnfTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var falseDnf = Dnf.builder().parameter(p).build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(not(falseDnf.call(q)))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause().build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysNotTrueDnfTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var trueDnf = Dnf.builder().parameter(p).clause().build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q), not(trueDnf.call(q)))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToDefinitionStringTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToDefinitionStringTest.java
new file mode 100644
index 00000000..9b469bb0
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToDefinitionStringTest.java
@@ -0,0 +1,174 @@
+package tools.refinery.store.query;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.view.KeyOnlyRelationView;
+import tools.refinery.store.representation.Symbol;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+import static tools.refinery.store.query.literal.Literals.not;
+
+class DnfToDefinitionStringTest {
+        @Test
+        void noClausesTest() {
+                var p = Variable.of("p");
+                var dnf = Dnf.builder("Example").parameter(p).build();
+
+                assertThat(dnf.toDefinitionString(), is("""
+                                pred Example(p) <->
+                                    <no clauses>.
+                                """));
+        }
+
+        @Test
+        void noParametersTest() {
+                var dnf = Dnf.builder("Example").build();
+
+                assertThat(dnf.toDefinitionString(), is("""
+                                pred Example() <->
+                                    <no clauses>.
+                                """));
+        }
+
+        @Test
+        void emptyClauseTest() {
+                var p = Variable.of("p");
+                var dnf = Dnf.builder("Example").parameter(p).clause().build();
+
+                assertThat(dnf.toDefinitionString(), is("""
+                                pred Example(p) <->
+                                    <empty>.
+                                """));
+        }
+
+        @Test
+        void relationViewPositiveTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example").parameter(p).clause(friendView.call(p, q)).build();
+
+                assertThat(dnf.toDefinitionString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") friend(p, q).
+                                """));
+        }
+
+        @Test
+        void relationViewNegativeTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example").parameter(p).clause(not(friendView.call(p, q))).build();
+
+                assertThat(dnf.toDefinitionString(), is("""
+                                pred Example(p) <->
+                                    !(@RelationView("key") friend(p, q)).
+                                """));
+        }
+
+        @Test
+        void relationViewTransitiveTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example").parameter(p).clause(friendView.callTransitive(p, q)).build();
+
+                assertThat(dnf.toDefinitionString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") friend+(p, q).
+                                """));
+        }
+
+        @Test
+        void multipleParametersTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example").parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(dnf.toDefinitionString(), is("""
+                                pred Example(p, q) <->
+                                    @RelationView("key") friend(p, q).
+                                """));
+        }
+
+        @Test
+        void multipleLiteralsTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var person = new Symbol<>("person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example")
+                                .parameter(p)
+                                .clause(
+                                                personView.call(p),
+                                                personView.call(q),
+                                                friendView.call(p, q)
+                                )
+                                .build();
+
+                assertThat(dnf.toDefinitionString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") person(p),
+                                    @RelationView("key") person(q),
+                                    @RelationView("key") friend(p, q).
+                                """));
+        }
+
+        @Test
+        void multipleClausesTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example")
+                                .parameter(p)
+                                .clause(friendView.call(p, q))
+                                .clause(friendView.call(q, p))
+                                .build();
+
+                assertThat(dnf.toDefinitionString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") friend(p, q)
+                                ;
+                                    @RelationView("key") friend(q, p).
+                                """));
+        }
+
+        @Test
+        void dnfTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var r = Variable.of("r");
+                var s = Variable.of("s");
+                var person = new Symbol<>("person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var called  = Dnf.builder("Called").parameters(r, s).clause(friendView.call(r, s)).build();
+                var dnf = Dnf.builder("Example")
+                                .parameter(p)
+                                .clause(
+                                                personView.call(p),
+                                                personView.call(q),
+                                                not(called.call(p, q))
+                                )
+                                .build();
+
+                assertThat(dnf.toDefinitionString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") person(p),
+                                    @RelationView("key") person(q),
+                                    !(@Dnf Called(p, q)).
+                                """));
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/tests/StructurallyEqualToTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/tests/StructurallyEqualToTest.java
new file mode 100644
index 00000000..a61e2b65
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/tests/StructurallyEqualToTest.java
@@ -0,0 +1,77 @@
+package tools.refinery.store.query.tests;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.view.KeyOnlyRelationView;
+import tools.refinery.store.representation.Symbol;
+
+import static org.hamcrest.CoreMatchers.containsString;
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.junit.jupiter.api.Assertions.assertThrows;
+import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo;
+
+class StructurallyEqualToTest {
+        @Test
+        void flatEqualsTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+
+                var expected = Dnf.builder("Expected").parameters(q).clause(personView.call(q)).build();
+                var actual = Dnf.builder("Actual").parameters(p).clause(personView.call(p)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void flatNotEqualsTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+
+                var expected = Dnf.builder("Expected").parameters(q).clause(personView.call(q)).build();
+                var actual = Dnf.builder("Actual").parameters(p).clause(personView.call(q)).build();
+
+                var assertion = structurallyEqualTo(expected);
+                assertThrows(AssertionError.class, () -> assertThat(actual, assertion));
+        }
+
+        @Test
+        void deepEqualsTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+
+                var expected = Dnf.builder("Expected").parameters(q).clause(
+                                Dnf.builder("Expected2").parameters(p).clause(personView.call(p)).build().call(q)
+                ).build();
+                var actual = Dnf.builder("Actual").parameters(q).clause(
+                                Dnf.builder("Actual2").parameters(p).clause(personView.call(p)).build().call(q)
+                ).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void deepNotEqualsTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+
+                var expected = Dnf.builder("Expected").parameters(q).clause(
+                                Dnf.builder("Expected2").parameters(p).clause(personView.call(p)).build().call(q)
+                ).build();
+                var actual = Dnf.builder("Actual").parameters(q).clause(
+                                Dnf.builder("Actual2").parameters(p).clause(personView.call(q)).build().call(q)
+                ).build();
+
+                var assertion = structurallyEqualTo(expected);
+                var error = assertThrows(AssertionError.class, () -> assertThat(actual, assertion));
+                assertThat(error.getMessage(), containsString(" called from Expected/1 "));
+        }
+}
diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java
new file mode 100644
index 00000000..685957c9
--- /dev/null
+++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java
@@ -0,0 +1,43 @@
+package tools.refinery.store.query.tests;
+
+import org.hamcrest.Description;
+import tools.refinery.store.query.equality.DeepDnfEqualityChecker;
+
+class MismatchDescribingDnfEqualityChecker extends DeepDnfEqualityChecker {
+        private final Description description;
+        private boolean described;
+
+        MismatchDescribingDnfEqualityChecker(Description description) {
+                this.description = description;
+        }
+
+        public boolean isDescribed() {
+                return described;
+        }
+
+        @Override
+        protected boolean doCheckEqual(Pair pair) {
+                boolean result = super.doCheckEqual(pair);
+                if (!result && !described) {
+                        describeMismatch(pair);
+                        // Only describe the first found (innermost) mismatch.
+                        described = true;
+                }
+                return result;
+        }
+
+        private void describeMismatch(Pair pair) {
+                var inProgress = getInProgress();
+                int size = inProgress.size();
+                if (size <= 1) {
+                        description.appendText("was ").appendText(pair.left().toDefinitionString());
+                        return;
+                }
+                var last = inProgress.get(size - 1);
+                description.appendText("expected ").appendText(last.right().toDefinitionString());
+                for (int i = size - 2; i >= 0; i--) {
+                        description.appendText(" called from ").appendText(inProgress.get(i).left().toString());
+                }
+                description.appendText(" was not structurally equal to ").appendText(last.right().toDefinitionString());
+        }
+}
diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/QueryMatchers.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/QueryMatchers.java
new file mode 100644
index 00000000..bf1c1b74
--- /dev/null
+++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/QueryMatchers.java
@@ -0,0 +1,14 @@
+package tools.refinery.store.query.tests;
+
+import org.hamcrest.Matcher;
+import tools.refinery.store.query.dnf.Dnf;
+
+public final class QueryMatchers {
+        private QueryMatchers() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static Matcher<Dnf> structurallyEqualTo(Dnf expected) {
+                return new StructurallyEqualTo(expected);
+        }
+}
diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/StructurallyEqualTo.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/StructurallyEqualTo.java
new file mode 100644
index 00000000..a9a78f88
--- /dev/null
+++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/StructurallyEqualTo.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.query.tests;
+
+import org.hamcrest.Description;
+import org.hamcrest.TypeSafeMatcher;
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.equality.DeepDnfEqualityChecker;
+
+public class StructurallyEqualTo extends TypeSafeMatcher<Dnf> {
+        private final Dnf expected;
+
+        public StructurallyEqualTo(Dnf expected) {
+                this.expected = expected;
+        }
+
+        @Override
+        protected boolean matchesSafely(Dnf item) {
+                var checker = new DeepDnfEqualityChecker();
+                return checker.dnfEqual(expected, item);
+        }
+
+        @Override
+        protected void describeMismatchSafely(Dnf item, Description mismatchDescription) {
+                var describingChecker = new MismatchDescribingDnfEqualityChecker(mismatchDescription);
+                if (describingChecker.dnfEqual(expected, item)) {
+                        throw new IllegalStateException("Mismatched Dnf was matching on repeated comparison");
+                }
+                if (!describingChecker.isDescribed()) {
+                        super.describeMismatchSafely(item, mismatchDescription);
+                }
+        }
+
+        @Override
+        public void describeTo(Description description) {
+                description.appendText("structurally equal to ").appendText(expected.toDefinitionString());
+        }
+}