feat: terms and improved query evaluation

* Implement data terms for computations in queries.
* Function-like queries with computed results.
* Improved query evaluation, including positive and negative diagonal
  cosntraints.
* Preliminary local search support.
* Changes to the DNF representation for count and aggregation support.

feat: terms wip

feat: query terms wip

feat: query evaluation, diagonal constraints, local search wip

fix reasoning compilation wip

98 files changed, 3001 insertions, 343 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
index 9ff6df26..9af73bdd 100644
--- 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
@@ -2,21 +2,33 @@ 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 class EmptyResultSet implements ResultSet {
+public record EmptyResultSet<T>(ModelQueryAdapter adapter, Query<T> query) implements ResultSet<T> {
         @Override
-        public boolean hasResult(TupleLike parameters) {
-                return false;
+        public ModelQueryAdapter getAdapter() {
+                return adapter;
         }
 
         @Override
-        public Cursor<TupleLike, Boolean> allResults() {
+        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 countResults() {
+        public int size() {
                 return 0;
         }
 }
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
index f7762444..2e30fec4 100644
--- 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
@@ -1,11 +1,17 @@
 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();
 
-        ResultSet getResultSet(Dnf query);
+        default AnyResultSet getResultSet(AnyQuery query) {
+                return getResultSet((Query<?>) query);
+        }
+
+        <T> ResultSet<T> getResultSet(Query<T> query);
 
         boolean hasPendingChanges();
 
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
index b3cfb4b4..4fdc9210 100644
--- 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
@@ -2,21 +2,23 @@ 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(Dnf... queries) {
+        default ModelQueryBuilder queries(AnyQuery... queries) {
                 return queries(List.of(queries));
         }
 
-        default ModelQueryBuilder queries(Collection<Dnf> queries) {
+        default ModelQueryBuilder queries(Collection<? extends AnyQuery> queries) {
                 queries.forEach(this::query);
                 return this;
         }
 
-        ModelQueryBuilder query(Dnf query);
+        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
index 091d6d06..514e582b 100644
--- 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
@@ -1,15 +1,16 @@
 package tools.refinery.store.query;
 
-import tools.refinery.store.query.view.AnyRelationView;
 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<Dnf> getQueries();
+        Collection<AnyQuery> getQueries();
 
         @Override
         ModelQueryAdapter createModelAdapter(Model model);
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/RelationLike.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/RelationLike.java
deleted file mode 100644
index 8c784d8b..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/RelationLike.java
+++ /dev/null
@@ -1,11 +0,0 @@
-package tools.refinery.store.query;
-
-public interface RelationLike {
-        String name();
-
-        int arity();
-
-        default boolean invalidIndex(int i) {
-                return i < 0 || i >= arity();
-        }
-}
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
index d2b8c9dd..3f6bc06f 100644
--- 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
@@ -1,16 +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 interface ResultSet {
-        default boolean hasResult() {
-                return countResults() > 0;
-        }
+public non-sealed interface ResultSet<T> extends AnyResultSet {
+        Query<T> getQuery();
 
-        boolean hasResult(TupleLike parameters);
+        T get(TupleLike parameters);
 
-        Cursor<TupleLike, Boolean> allResults();
-
-        int countResults();
+        Cursor<TupleLike, T> getAll();
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java
deleted file mode 100644
index d0e0dead..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java
+++ /dev/null
@@ -1,63 +0,0 @@
-package tools.refinery.store.query;
-
-import tools.refinery.store.query.literal.ConstantLiteral;
-import tools.refinery.store.query.literal.EquivalenceLiteral;
-
-import java.util.Objects;
-
-public class Variable {
-        private final String name;
-        private final String uniqueName;
-
-        public Variable() {
-                this(null);
-        }
-
-        public Variable(String name) {
-                super();
-                this.name = name;
-                this.uniqueName = DnfUtils.generateUniqueName(name);
-
-        }
-        public String getName() {
-                return name == null ? uniqueName : name;
-        }
-
-        public boolean isExplicitlyNamed() {
-                return name != null;
-        }
-
-        public String getUniqueName() {
-                return uniqueName;
-        }
-
-        public ConstantLiteral isConstant(int value) {
-                return new ConstantLiteral(this, value);
-        }
-
-        public EquivalenceLiteral isEquivalent(Variable other) {
-                return new EquivalenceLiteral(true, this, other);
-        }
-
-        public EquivalenceLiteral notEquivalent(Variable other) {
-                return new EquivalenceLiteral(false, this, other);
-        }
-
-        @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);
-        }
-}
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.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java
index b6744b50..1b7759c7 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java
@@ -1,14 +1,18 @@
-package tools.refinery.store.query;
+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.literal.CallPolarity;
-import tools.refinery.store.query.literal.DnfCallLiteral;
+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.*;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
 
-public final class Dnf implements RelationLike {
+public final class Dnf implements Constraint {
         private static final String INDENTATION = "    ";
 
         private final String name;
@@ -69,6 +73,11 @@ public final class Dnf implements RelationLike {
                 return parameters;
         }
 
+        @Override
+        public List<Sort> getSorts() {
+                return parameters.stream().map(Variable::getSort).toList();
+        }
+
         public List<FunctionalDependency<Variable>> getFunctionalDependencies() {
                 return functionalDependencies;
         }
@@ -82,6 +91,15 @@ public final class Dnf implements RelationLike {
                 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;
@@ -94,22 +112,6 @@ public final class Dnf implements RelationLike {
                 return LiteralReduction.NOT_REDUCIBLE;
         }
 
-        public DnfCallLiteral call(CallPolarity polarity, List<Variable> arguments) {
-                return new DnfCallLiteral(polarity, this, arguments);
-        }
-
-        public DnfCallLiteral call(CallPolarity polarity, Variable... arguments) {
-                return call(polarity, List.of(arguments));
-        }
-
-        public DnfCallLiteral call(Variable... arguments) {
-                return call(CallPolarity.POSITIVE, arguments);
-        }
-
-        public DnfCallLiteral callTransitive(Variable left, Variable right) {
-                return call(CallPolarity.TRANSITIVE, List.of(left, right));
-        }
-
         public boolean equalsWithSubstitution(DnfEqualityChecker callEqualityChecker, Dnf other) {
                 if (arity() != other.arity()) {
                         return false;
@@ -128,7 +130,24 @@ public final class Dnf implements RelationLike {
         }
 
         @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();
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java
index ca47e979..aad5a85f 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java
@@ -1,11 +1,13 @@
-package tools.refinery.store.query;
+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 class DnfBuilder {
+public final class DnfBuilder {
         private final String name;
 
         private final List<Variable> parameters = new ArrayList<>();
@@ -19,6 +21,9 @@ public class DnfBuilder {
         }
 
         public DnfBuilder parameter(Variable variable) {
+                if (parameters.contains(variable)) {
+                        throw new IllegalArgumentException("Duplicate parameter: " + variable);
+                }
                 parameters.add(variable);
                 return this;
         }
@@ -27,7 +32,7 @@ public class DnfBuilder {
                 return parameters(List.of(variables));
         }
 
-        public DnfBuilder parameters(Collection<Variable> variables) {
+        public DnfBuilder parameters(Collection<? extends Variable> variables) {
                 parameters.addAll(variables);
                 return this;
         }
@@ -42,8 +47,8 @@ public class DnfBuilder {
                 return this;
         }
 
-        public DnfBuilder functionalDependency(Set<Variable> forEach, Set<Variable> unique) {
-                return functionalDependency(new FunctionalDependency<>(forEach, unique));
+        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) {
@@ -51,7 +56,7 @@ public class DnfBuilder {
                 return this;
         }
 
-        public DnfBuilder clause(Collection<Literal> literals) {
+        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) {
@@ -73,21 +78,6 @@ public class DnfBuilder {
                 return this;
         }
 
-        public DnfBuilder clause(DnfClause clause) {
-                return clause(clause.literals());
-        }
-
-        public DnfBuilder clauses(DnfClause... clauses) {
-                return clauses(List.of(clauses));
-        }
-
-        public DnfBuilder clauses(Collection<DnfClause> clauses) {
-                for (var clause : clauses) {
-                        this.clause(clause);
-                }
-                return this;
-        }
-
         public Dnf build() {
                 var postProcessedClauses = postProcessClauses();
                 return new Dnf(name, Collections.unmodifiableList(parameters),
@@ -95,6 +85,11 @@ public class DnfBuilder {
                                 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) {
@@ -103,8 +98,8 @@ public class DnfBuilder {
                                 return List.of(new DnfClause(Set.of(), List.of()));
                         }
                         var variables = new HashSet<Variable>();
-                        for (var constraint : literals) {
-                                constraint.collectAllVariables(variables);
+                        for (var literal : literals) {
+                                variables.addAll(literal.getBoundVariables());
                         }
                         parameters.forEach(variables::remove);
                         postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables),
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java
index c6e8b8c9..01830af1 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java
@@ -1,12 +1,13 @@
-package tools.refinery.store.query;
+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> quantifiedVariables, List<Literal> literals) {
+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()) {
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfUtils.java
index c7a2849c..9bcf944c 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfUtils.java
@@ -1,4 +1,4 @@
-package tools.refinery.store.query;
+package tools.refinery.store.query.dnf;
 
 import java.util.UUID;
 
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/FunctionalDependency.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalDependency.java
index 63a81713..f4cd109f 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/FunctionalDependency.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalDependency.java
@@ -1,4 +1,4 @@
-package tools.refinery.store.query;
+package tools.refinery.store.query.dnf;
 
 import java.util.HashSet;
 import java.util.Set;
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
index ebd7f5b0..c3bc3ea3 100644
--- 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
@@ -1,6 +1,6 @@
 package tools.refinery.store.query.equality;
 
-import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.dnf.Dnf;
 import tools.refinery.store.util.CycleDetectingMapper;
 
 import java.util.List;
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
index eb77de17..6b1f2076 100644
--- 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
@@ -1,6 +1,6 @@
 package tools.refinery.store.query.equality;
 
-import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.dnf.Dnf;
 
 @FunctionalInterface
 public interface DnfEqualityChecker {
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
index 23f1acc7..07d261ea 100644
--- 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
@@ -1,7 +1,7 @@
 package tools.refinery.store.query.equality;
 
-import tools.refinery.store.query.Dnf;
-import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.term.Variable;
 
 import java.util.HashMap;
 import java.util.List;
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
index 6d751be8..38be61a4 100644
--- 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
@@ -1,12 +1,12 @@
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.Variable;
+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 PolarLiteral<BooleanLiteral> {
+public enum BooleanLiteral implements CanNegate<BooleanLiteral> {
         TRUE(true),
         FALSE(false);
 
@@ -17,8 +17,8 @@ public enum BooleanLiteral implements PolarLiteral<BooleanLiteral> {
         }
 
         @Override
-        public void collectAllVariables(Set<Variable> variables) {
-                // No variables to collect.
+        public Set<Variable> getBoundVariables() {
+                return Set.of();
         }
 
         @Override
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
index 091b4e04..78fae7f5 100644
--- 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
@@ -1,109 +1,78 @@
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.RelationLike;
-import tools.refinery.store.query.Variable;
+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 abstract class CallLiteral<T extends RelationLike> implements Literal {
+public final class CallLiteral extends AbstractCallLiteral implements CanNegate<CallLiteral> {
         private final CallPolarity polarity;
-        private final T target;
-        private final List<Variable> arguments;
 
-        protected CallLiteral(CallPolarity polarity, T target, List<Variable> arguments) {
-                if (arguments.size() != target.arity()) {
-                        throw new IllegalArgumentException("%s needs %d arguments, but got %s".formatted(target.name(),
-                                        target.arity(), arguments.size()));
-                }
-                if (polarity.isTransitive() && target.arity() != 2) {
-                        throw new IllegalArgumentException("Transitive closures can only take binary relations");
+        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;
-                this.target = target;
-                this.arguments = arguments;
         }
 
         public CallPolarity getPolarity() {
                 return polarity;
         }
 
-        public abstract Class<T> getTargetType();
-
-        public T getTarget() {
-                return target;
-        }
-
-        public List<Variable> getArguments() {
-                return arguments;
-        }
-
         @Override
-        public void collectAllVariables(Set<Variable> variables) {
-                if (polarity.isPositive()) {
-                        variables.addAll(arguments);
-                }
+        public Set<Variable> getBoundVariables() {
+                return polarity.isPositive() ? Set.copyOf(getArguments()) : Set.of();
         }
 
-        protected List<Variable> substituteArguments(Substitution substitution) {
-                return arguments.stream().map(substitution::getSubstitute).toList();
+        @Override
+        protected Literal doSubstitute(Substitution substitution, List<Variable> substitutedArguments) {
+                return new CallLiteral(polarity, getTarget(), substitutedArguments);
         }
 
-        /**
-         * Compares the target of this call literal with another object.
-         *
-         * @param helper      Equality helper for comparing {@link Variable} and {@link tools.refinery.store.query.Dnf}
-         *                    instances.
-         * @param otherTarget The object to compare the target to.
-         * @return {@code true} if {@code otherTarget} is equal to the return value of {@link #getTarget()} according to
-         * {@code helper}, {@code false} otherwise.
-         */
-        protected boolean targetEquals(LiteralEqualityHelper helper, T otherTarget) {
-                return target.equals(otherTarget);
+        @Override
+        public LiteralReduction getReduction() {
+                var reduction = getTarget().getReduction();
+                return polarity.isPositive() ? reduction : reduction.negate();
         }
 
         @Override
         public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
-                if (other.getClass() != getClass()) {
+                if (!super.equalsWithSubstitution(helper, other)) {
                         return false;
                 }
-                var otherCallLiteral = (CallLiteral<?>) other;
-                if (getTargetType() != otherCallLiteral.getTargetType() || polarity != otherCallLiteral.polarity) {
-                        return false;
-                }
-                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;
-                        }
-                }
-                @SuppressWarnings("unchecked")
-                var otherTarget = (T) otherCallLiteral.target;
-                return targetEquals(helper, otherTarget);
+                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;
-                CallLiteral<?> callAtom = (CallLiteral<?>) o;
-                return polarity == callAtom.polarity && Objects.equals(target, callAtom.target) &&
-                                Objects.equals(arguments, callAtom.arguments);
+                if (!super.equals(o)) return false;
+                CallLiteral that = (CallLiteral) o;
+                return polarity == that.polarity;
         }
 
         @Override
         public int hashCode() {
-                return Objects.hash(polarity, target, arguments);
-        }
-
-        protected String targetToString() {
-                return "@%s %s".formatted(getTargetType().getSimpleName(), target.name());
+                return Objects.hash(super.hashCode(), polarity);
         }
 
         @Override
@@ -112,12 +81,12 @@ public abstract class CallLiteral<T extends RelationLike> implements Literal {
                 if (!polarity.isPositive()) {
                         builder.append("!(");
                 }
-                builder.append(targetToString());
+                builder.append(getTarget().toReferenceString());
                 if (polarity.isTransitive()) {
                         builder.append("+");
                 }
                 builder.append("(");
-                var argumentIterator = arguments.iterator();
+                var argumentIterator = getArguments().iterator();
                 if (argumentIterator.hasNext()) {
                         builder.append(argumentIterator.next());
                         while (argumentIterator.hasNext()) {
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
index d01c7d20..93fa3df0 100644
--- 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
@@ -1,20 +1,21 @@
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.Variable;
 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(Variable variable, int nodeId) implements Literal {
+public record ConstantLiteral(NodeVariable variable, int nodeId) implements Literal {
         @Override
-        public void collectAllVariables(Set<Variable> variables) {
-                variables.add(variable);
+        public Set<Variable> getBoundVariables() {
+                return Set.of(variable);
         }
 
         @Override
         public ConstantLiteral substitute(Substitution substitution) {
-                return new ConstantLiteral(substitution.getSubstitute(variable), nodeId);
+                return new ConstantLiteral(substitution.getTypeSafeSubstitute(variable), nodeId);
         }
 
         @Override
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/DnfCallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java
deleted file mode 100644
index 27917265..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java
+++ /dev/null
@@ -1,40 +0,0 @@
-package tools.refinery.store.query.literal;
-
-import tools.refinery.store.query.Dnf;
-import tools.refinery.store.query.Variable;
-import tools.refinery.store.query.equality.LiteralEqualityHelper;
-import tools.refinery.store.query.substitution.Substitution;
-
-import java.util.List;
-
-public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiteral<DnfCallLiteral> {
-        public DnfCallLiteral(CallPolarity polarity, Dnf target, List<Variable> arguments) {
-                super(polarity, target, arguments);
-        }
-
-        @Override
-        public Class<Dnf> getTargetType() {
-                return Dnf.class;
-        }
-
-        @Override
-        public DnfCallLiteral substitute(Substitution substitution) {
-                return new DnfCallLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
-        }
-
-        @Override
-        public DnfCallLiteral negate() {
-                return new DnfCallLiteral(getPolarity().negate(), getTarget(), getArguments());
-        }
-
-        @Override
-        public LiteralReduction getReduction() {
-                var dnfReduction = getTarget().getReduction();
-                return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate();
-        }
-
-        @Override
-        protected boolean targetEquals(LiteralEqualityHelper helper, Dnf otherTarget) {
-                return helper.dnfEqual(getTarget(), otherTarget);
-        }
-}
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
index 61c753c3..4dc86b98 100644
--- 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
@@ -1,17 +1,19 @@
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.Variable;
+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, Variable left, Variable right)
-                implements PolarLiteral<EquivalenceLiteral> {
+public record EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right)
+                implements CanNegate<EquivalenceLiteral> {
         @Override
-        public void collectAllVariables(Set<Variable> variables) {
-                variables.add(left);
-                variables.add(right);
+        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
@@ -21,7 +23,8 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right
 
         @Override
         public EquivalenceLiteral substitute(Substitution substitution) {
-                return new EquivalenceLiteral(positive, substitution.getSubstitute(left), substitution.getSubstitute(right));
+                return new EquivalenceLiteral(positive, substitution.getTypeSafeSubstitute(left),
+                                substitution.getTypeSafeSubstitute(right));
         }
 
         @Override
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
index ddd91775..6347410e 100644
--- 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
@@ -1,13 +1,13 @@
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.Variable;
+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 {
-        void collectAllVariables(Set<Variable> variables);
+        Set<Variable> getBoundVariables();
 
         Literal substitute(Substitution substitution);
 
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
index 2c7e893f..89039352 100644
--- 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
@@ -1,11 +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 PolarLiteral<T>> T not(PolarLiteral<T> literal) {
+        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/literal/PolarLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java
deleted file mode 100644
index 32523675..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/PolarLiteral.java
+++ /dev/null
@@ -1,5 +0,0 @@
-package tools.refinery.store.query.literal;
-
-public interface PolarLiteral<T extends PolarLiteral<T>> extends Literal {
-        T negate();
-}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java
deleted file mode 100644
index fb8b3332..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java
+++ /dev/null
@@ -1,35 +0,0 @@
-package tools.refinery.store.query.literal;
-
-import tools.refinery.store.query.Variable;
-import tools.refinery.store.query.substitution.Substitution;
-import tools.refinery.store.query.view.AnyRelationView;
-
-import java.util.List;
-
-public final class RelationViewLiteral extends CallLiteral<AnyRelationView>
-                implements PolarLiteral<RelationViewLiteral> {
-        public RelationViewLiteral(CallPolarity polarity, AnyRelationView target, List<Variable> arguments) {
-                super(polarity, target, arguments);
-        }
-
-        @Override
-        public Class<AnyRelationView> getTargetType() {
-                return AnyRelationView.class;
-        }
-
-        @Override
-        protected String targetToString() {
-                var target = getTarget();
-                return "@RelationView(\"%s\") %s".formatted(target.getViewName(), target.getSymbol().name());
-        }
-
-        @Override
-        public RelationViewLiteral substitute(Substitution substitution) {
-                return new RelationViewLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
-        }
-
-        @Override
-        public RelationViewLiteral negate() {
-                return new RelationViewLiteral(getPolarity().negate(), getTarget(), getArguments());
-        }
-}
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
index ffc65047..c7754619 100644
--- 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
@@ -1,6 +1,6 @@
 package tools.refinery.store.query.substitution;
 
-import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.term.Variable;
 
 import java.util.Map;
 
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
index 54d18a3f..7847e582 100644
--- 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
@@ -1,6 +1,6 @@
 package tools.refinery.store.query.substitution;
 
-import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.term.Variable;
 
 import java.util.HashMap;
 import java.util.Map;
@@ -10,10 +10,6 @@ public class RenewingSubstitution implements Substitution {
 
         @Override
         public Variable getSubstitute(Variable variable) {
-                return alreadyRenewed.computeIfAbsent(variable, RenewingSubstitution::renew);
-        }
-
-        private static Variable renew(Variable variable) {
-                return variable.isExplicitlyNamed() ? new Variable(variable.getName()) : new 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
index d33ad6fb..eed414d9 100644
--- 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
@@ -1,6 +1,6 @@
 package tools.refinery.store.query.substitution;
 
-import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.term.Variable;
 
 public enum StatelessSubstitution implements Substitution {
         FAILING {
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
index 9d086bf5..99f84b9e 100644
--- 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
@@ -1,8 +1,29 @@
 package tools.refinery.store.query.substitution;
 
-import tools.refinery.store.query.Variable;
+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
index 26cf1a20..5d4654da 100644
--- 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
@@ -1,6 +1,8 @@
 package tools.refinery.store.query.substitution;
 
-import tools.refinery.store.query.Variable;
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+import tools.refinery.store.query.term.Variable;
 
 import java.util.Map;
 
@@ -24,4 +26,8 @@ public final class Substitutions {
         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
index bc3ac1ea..6ae410f2 100644
--- 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
@@ -1,13 +1,13 @@
 package tools.refinery.store.query.view;
 
 import tools.refinery.store.model.Model;
-import tools.refinery.store.query.FunctionalDependency;
+import tools.refinery.store.query.dnf.FunctionalDependency;
 import tools.refinery.store.representation.AnySymbol;
-import tools.refinery.store.query.RelationLike;
+import tools.refinery.store.query.Constraint;
 
 import java.util.Set;
 
-public sealed interface AnyRelationView extends RelationLike permits RelationView {
+public sealed interface AnyRelationView extends Constraint permits RelationView {
         AnySymbol getSymbol();
 
         String getViewName();
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
index 3d278a8b..7ec9e7ac 100644
--- 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
@@ -1,22 +1,31 @@
 package tools.refinery.store.query.view;
 
 import tools.refinery.store.model.Model;
-import tools.refinery.store.query.FunctionalDependency;
+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
@@ -37,7 +46,7 @@ public final class FunctionalRelationView<T> extends RelationView<T> {
 
         @Override
         public boolean filter(Tuple key, T value) {
-                return true;
+                return !Objects.equals(defaultValue, value);
         }
 
         @Override
@@ -68,4 +77,29 @@ public final class FunctionalRelationView<T> extends RelationView<T> {
         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/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
index ea9fd5e2..d7164b3b 100644
--- 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
@@ -1,14 +1,10 @@
 package tools.refinery.store.query.view;
 
-import tools.refinery.store.query.Variable;
 import tools.refinery.store.map.CursorAsIterator;
 import tools.refinery.store.model.Model;
-import tools.refinery.store.query.literal.CallPolarity;
-import tools.refinery.store.query.literal.RelationViewLiteral;
 import tools.refinery.store.representation.Symbol;
 import tools.refinery.store.tuple.Tuple;
 
-import java.util.List;
 import java.util.Objects;
 import java.util.UUID;
 
@@ -56,20 +52,14 @@ public abstract non-sealed class RelationView<T> implements AnyRelationView {
                 return (() -> new CursorAsIterator<>(model.getInterpretation(symbol).getAll(), this::forwardMap, this::filter));
         }
 
-        public RelationViewLiteral call(CallPolarity polarity, List<Variable> arguments) {
-                return new RelationViewLiteral(polarity, this, arguments);
-        }
-
-        public RelationViewLiteral call(CallPolarity polarity, Variable... arguments) {
-                return call(polarity, List.of(arguments));
-        }
-
-        public RelationViewLiteral call(Variable... arguments) {
-                return call(CallPolarity.POSITIVE, arguments);
+        @Override
+        public String toString() {
+                return name();
         }
 
-        public RelationViewLiteral callTransitive(Variable left, Variable right) {
-                return call(CallPolarity.TRANSITIVE, List.of(left, right));
+        @Override
+        public String toReferenceString() {
+                return "@RelationView(\"%s\") %s".formatted(viewName, symbol.name());
         }
 
         @Override
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
index 8cc4986e..234b3a9a 100644
--- 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
@@ -1,10 +1,15 @@
 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);
@@ -38,7 +43,15 @@ public abstract class TuplePreservingRelationView<T> extends RelationView<T> {
                 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);
+        }
 }