refactor: query terms

* Separate different operators into different classes to make it easier to add
  functionality (e.g., simplification) later.
* Add UpperCardinality terms.
* Move UpperCardinality aggregator and tests into refinery-store-query.

87 files changed, 2507 insertions, 1187 deletions

diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/cardinality/UpperCardinalitySumAggregationOperator.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/cardinality/UpperCardinalitySumAggregationOperator.java
deleted file mode 100644
index bfd4c049..00000000
--- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/cardinality/UpperCardinalitySumAggregationOperator.java
+++ /dev/null
@@ -1,102 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.query.viatra.internal.cardinality;
-
-import org.eclipse.viatra.query.runtime.matchers.psystem.aggregations.BoundAggregator;
-import org.eclipse.viatra.query.runtime.matchers.psystem.aggregations.IMultisetAggregationOperator;
-import tools.refinery.store.representation.cardinality.FiniteUpperCardinality;
-import tools.refinery.store.representation.cardinality.UnboundedUpperCardinality;
-import tools.refinery.store.representation.cardinality.UpperCardinalities;
-import tools.refinery.store.representation.cardinality.UpperCardinality;
-
-import java.util.stream.Stream;
-
-public class UpperCardinalitySumAggregationOperator implements IMultisetAggregationOperator<UpperCardinality,
-                UpperCardinalitySumAggregationOperator.Accumulator, UpperCardinality> {
-        public static final UpperCardinalitySumAggregationOperator INSTANCE = new UpperCardinalitySumAggregationOperator();
-
-        public static final BoundAggregator BOUND_AGGREGATOR = new BoundAggregator(INSTANCE, UpperCardinality.class,
-                        UpperCardinality.class);
-
-        private UpperCardinalitySumAggregationOperator() {
-                // Singleton constructor.
-        }
-
-        @Override
-        public String getName() {
-                return "sum<UpperCardinality>";
-        }
-
-        @Override
-        public String getShortDescription() {
-                return "%s computes the sum of finite or unbounded upper cardinalities".formatted(getName());
-        }
-
-        @Override
-        public Accumulator createNeutral() {
-                return new Accumulator();
-        }
-
-        @Override
-        public boolean isNeutral(Accumulator result) {
-                return result.sumFiniteUpperBounds == 0 && result.countUnbounded == 0;
-        }
-
-        @Override
-        public Accumulator update(Accumulator oldResult, UpperCardinality updateValue, boolean isInsertion) {
-                if (updateValue instanceof FiniteUpperCardinality finiteUpperCardinality) {
-                        int finiteUpperBound = finiteUpperCardinality.finiteUpperBound();
-                        if (isInsertion) {
-                                oldResult.sumFiniteUpperBounds += finiteUpperBound;
-                        } else {
-                                oldResult.sumFiniteUpperBounds -= finiteUpperBound;
-                        }
-                } else if (updateValue instanceof UnboundedUpperCardinality) {
-                        if (isInsertion) {
-                                oldResult.countUnbounded += 1;
-                        } else {
-                                oldResult.countUnbounded -= 1;
-                        }
-                } else {
-                        throw new IllegalArgumentException("Unknown UpperCardinality: " + updateValue);
-                }
-                return oldResult;
-        }
-
-        @Override
-        public UpperCardinality getAggregate(Accumulator result) {
-                return result.countUnbounded > 0 ? UpperCardinalities.UNBOUNDED :
-                                UpperCardinalities.valueOf(result.sumFiniteUpperBounds);
-        }
-
-        @Override
-        public UpperCardinality aggregateStream(Stream<UpperCardinality> stream) {
-                var result = stream.collect(this::createNeutral, (accumulator, value) -> update(accumulator, value, true),
-                                (left, right) -> new Accumulator(left.sumFiniteUpperBounds + right.sumFiniteUpperBounds,
-                                                left.countUnbounded + right.countUnbounded));
-                return getAggregate(result);
-        }
-
-        @Override
-        public Accumulator clone(Accumulator original) {
-                return new Accumulator(original.sumFiniteUpperBounds, original.countUnbounded);
-        }
-
-        public static class Accumulator {
-                private int sumFiniteUpperBounds;
-
-                private int countUnbounded;
-
-                private Accumulator(int sumFiniteUpperBounds, int countUnbounded) {
-                        this.sumFiniteUpperBounds = sumFiniteUpperBounds;
-                        this.countUnbounded = countUnbounded;
-                }
-
-                private Accumulator() {
-                        this(0, 0);
-                }
-        }
-}
diff --git a/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/internal/cardinality/UpperCardinalitySumAggregationOperatorTest.java b/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/internal/cardinality/UpperCardinalitySumAggregationOperatorTest.java
deleted file mode 100644
index 677eeeac..00000000
--- a/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/internal/cardinality/UpperCardinalitySumAggregationOperatorTest.java
+++ /dev/null
@@ -1,92 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.query.viatra.internal.cardinality;
-
-import org.junit.jupiter.api.BeforeEach;
-import org.junit.jupiter.api.Test;
-import tools.refinery.store.representation.cardinality.UpperCardinalities;
-import tools.refinery.store.representation.cardinality.UpperCardinality;
-
-import static org.hamcrest.MatcherAssert.assertThat;
-import static org.hamcrest.Matchers.equalTo;
-
-class UpperCardinalitySumAggregationOperatorTest {
-        private UpperCardinalitySumAggregationOperator.Accumulator accumulator;
-
-        @BeforeEach
-        void beforeEach() {
-                accumulator = UpperCardinalitySumAggregationOperator.INSTANCE.createNeutral();
-        }
-
-        @Test
-        void emptyAggregationTest() {
-                assertResult(UpperCardinality.of(0));
-        }
-
-        @Test
-        void singleBoundedTest() {
-                insert(UpperCardinality.of(3));
-                assertResult(UpperCardinality.of(3));
-        }
-
-        @Test
-        void multipleBoundedTest() {
-                insert(UpperCardinality.of(2));
-                insert(UpperCardinality.of(3));
-                assertResult(UpperCardinality.of(5));
-        }
-
-        @Test
-        void singleUnboundedTest() {
-                insert(UpperCardinalities.UNBOUNDED);
-                assertResult(UpperCardinalities.UNBOUNDED);
-        }
-
-        @Test
-        void multipleUnboundedTest() {
-                insert(UpperCardinalities.UNBOUNDED);
-                insert(UpperCardinalities.UNBOUNDED);
-                assertResult(UpperCardinalities.UNBOUNDED);
-        }
-
-        @Test
-        void removeBoundedTest() {
-                insert(UpperCardinality.of(2));
-                insert(UpperCardinality.of(3));
-                remove(UpperCardinality.of(2));
-                assertResult(UpperCardinality.of(3));
-        }
-
-        @Test
-        void removeAllUnboundedTest() {
-                insert(UpperCardinalities.UNBOUNDED);
-                insert(UpperCardinality.of(3));
-                remove(UpperCardinalities.UNBOUNDED);
-                assertResult(UpperCardinality.of(3));
-        }
-
-        @Test
-        void removeSomeUnboundedTest() {
-                insert(UpperCardinalities.UNBOUNDED);
-                insert(UpperCardinalities.UNBOUNDED);
-                insert(UpperCardinality.of(3));
-                remove(UpperCardinalities.UNBOUNDED);
-                assertResult(UpperCardinalities.UNBOUNDED);
-        }
-
-        private void insert(UpperCardinality value) {
-                accumulator = UpperCardinalitySumAggregationOperator.INSTANCE.update(accumulator, value, true);
-        }
-
-        private void remove(UpperCardinality value) {
-                accumulator = UpperCardinalitySumAggregationOperator.INSTANCE.update(accumulator, value, false);
-        }
-
-        private void assertResult(UpperCardinality expected) {
-                var result = UpperCardinalitySumAggregationOperator.INSTANCE.getAggregate(accumulator);
-                assertThat(result, equalTo(expected));
-        }
-}
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
index 58d563da..59538831 100644
--- 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
@@ -7,9 +7,9 @@ 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.ConstantTerm;
 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;
 
@@ -42,13 +42,12 @@ public record AssumeLiteral(Term<Boolean> term) implements Literal {
 
         @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;
+                if (term instanceof ConstantTerm<Boolean> constantTerm) {
+                        // Return {@code ALWAYS_FALSE} for {@code false} or {@code null} literals.
+                        return Boolean.TRUE.equals(constantTerm.getValue()) ? LiteralReduction.ALWAYS_TRUE :
+                                        LiteralReduction.ALWAYS_FALSE;
                 }
+                return LiteralReduction.NOT_REDUCIBLE;
         }
 
         @Override
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
deleted file mode 100644
index d175130e..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/CompositeSubstitution.java
+++ /dev/null
@@ -1,15 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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/Substitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java
index 5714edf4..834fce12 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
@@ -5,7 +5,6 @@
  */
 package tools.refinery.store.query.substitution;
 
-import tools.refinery.store.query.term.AnyDataVariable;
 import tools.refinery.store.query.term.DataVariable;
 import tools.refinery.store.query.term.NodeVariable;
 import tools.refinery.store.query.term.Variable;
@@ -19,16 +18,12 @@ public interface Substitution {
                 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);
+        static SubstitutionBuilder builder() {
+                return new SubstitutionBuilder();
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/SubstitutionBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/SubstitutionBuilder.java
new file mode 100644
index 00000000..658a26e3
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/SubstitutionBuilder.java
@@ -0,0 +1,78 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.NodeVariable;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+@SuppressWarnings("UnusedReturnValue")
+public class SubstitutionBuilder {
+        private final Map<Variable, Variable> map = new HashMap<>();
+        private Substitution fallback;
+
+        SubstitutionBuilder() {
+                total();
+        }
+
+        public SubstitutionBuilder put(NodeVariable original, NodeVariable substitute) {
+                return putChecked(original, substitute);
+        }
+
+        public <T> SubstitutionBuilder put(DataVariable<T> original, DataVariable<T> substitute) {
+                return putChecked(original, substitute);
+        }
+
+        public SubstitutionBuilder putChecked(Variable original, Variable substitute) {
+                if (!original.getSort().equals(substitute.getSort())) {
+                        throw new IllegalArgumentException("Cannot substitute variable %s of sort %s with variable %s of sort %s"
+                                        .formatted(original, original.getSort(), substitute, substitute.getSort()));
+                }
+                if (map.containsKey(original)) {
+                        throw new IllegalArgumentException("Already has substitution for variable %s".formatted(original));
+                }
+                map.put(original, substitute);
+                return this;
+        }
+
+        public SubstitutionBuilder putManyChecked(List<Variable> originals, List<Variable> substitutes) {
+                int size = originals.size();
+                if (size != substitutes.size()) {
+                        throw new IllegalArgumentException("Cannot substitute %d variables %s with %d variables %s"
+                                        .formatted(size, originals, substitutes.size(), substitutes));
+                }
+                for (int i = 0; i < size; i++) {
+                        putChecked(originals.get(i), substitutes.get(i));
+                }
+                return this;
+        }
+
+        public SubstitutionBuilder fallback(Substitution newFallback) {
+                fallback = newFallback;
+                return this;
+        }
+
+        public SubstitutionBuilder total() {
+                return fallback(StatelessSubstitution.FAILING);
+        }
+
+        public SubstitutionBuilder partial() {
+                return fallback(StatelessSubstitution.IDENTITY);
+        }
+
+        public SubstitutionBuilder renewing() {
+                return fallback(new RenewingSubstitution());
+        }
+
+        public Substitution build() {
+                return map.isEmpty() ? fallback : new MapBasedSubstitution(Collections.unmodifiableMap(map), fallback);
+        }
+}
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
deleted file mode 100644
index c4791bf1..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java
+++ /dev/null
@@ -1,38 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-package tools.refinery.store.query.substitution;
-
-import org.jetbrains.annotations.NotNull;
-import org.jetbrains.annotations.Nullable;
-import tools.refinery.store.query.term.Variable;
-
-import java.util.Map;
-
-public final class Substitutions {
-        private Substitutions() {
-                throw new IllegalStateException("This is a static utility class and should not be instantiate directly");
-        }
-
-        public static Substitution total(Map<Variable, Variable> map) {
-                return new MapBasedSubstitution(map, StatelessSubstitution.FAILING);
-        }
-
-        public static Substitution partial(Map<Variable, Variable> map) {
-                return new MapBasedSubstitution(map, StatelessSubstitution.IDENTITY);
-        }
-
-        public static Substitution renewing(Map<Variable, Variable> map) {
-                return new MapBasedSubstitution(map, renewing());
-        }
-
-        public static Substitution renewing() {
-                return new RenewingSubstitution();
-        }
-
-        public static Substitution compose(@Nullable Substitution first, @NotNull Substitution second) {
-                return first == null ? second : first.andThen(second);
-        }
-}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AbstractTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AbstractTerm.java
new file mode 100644
index 00000000..d0ae3c12
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AbstractTerm.java
@@ -0,0 +1,41 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term;
+
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+
+import java.util.Objects;
+
+public abstract class AbstractTerm<T> implements Term<T> {
+        private final Class<T> type;
+
+        protected AbstractTerm(Class<T> type) {
+                this.type = type;
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
+                return getClass().equals(other.getClass()) && type.equals(other.getType());
+        }
+
+        @Override
+        public Class<T> getType() {
+                return type;
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                AbstractTerm<?> that = (AbstractTerm<?>) o;
+                return type.equals(that.type);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(getClass(), type);
+        }
+}
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
deleted file mode 100644
index 5ff7c65c..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryOperator.java
+++ /dev/null
@@ -1,31 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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
deleted file mode 100644
index e405df00..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticBinaryTerm.java
+++ /dev/null
@@ -1,61 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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
deleted file mode 100644
index d98134f3..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryOperator.java
+++ /dev/null
@@ -1,21 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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
deleted file mode 100644
index bdc87545..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ArithmeticUnaryTerm.java
+++ /dev/null
@@ -1,56 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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/BinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/BinaryTerm.java
index b2994d23..8ad17839 100644
--- 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
@@ -14,26 +14,35 @@ import java.util.HashSet;
 import java.util.Objects;
 import java.util.Set;
 
-public abstract class BinaryTerm<R, T1, T2> implements Term<R> {
+public abstract class BinaryTerm<R, T1, T2> extends AbstractTerm<R> {
+        private final Class<T1> leftType;
+        private final Class<T2> rightType;
         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()));
+        protected BinaryTerm(Class<R> type, Class<T1> leftType, Class<T2> rightType, Term<T1> left, Term<T2> right) {
+                super(type);
+                if (!left.getType().equals(leftType)) {
+                        throw new IllegalArgumentException("Expected left %s to be of type %s, got %s instead".formatted(
+                                        left, leftType.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()));
+                if (!right.getType().equals(rightType)) {
+                        throw new IllegalArgumentException("Expected right %s to be of type %s, got %s instead".formatted(
+                                        right, rightType.getName(), right.getType().getName()));
                 }
+                this.leftType = leftType;
+                this.rightType = rightType;
                 this.left = left;
                 this.right = right;
         }
 
-        public abstract Class<T1> getLeftType();
+        public Class<T1> getLeftType() {
+                return leftType;
+        }
 
-        public abstract Class<T2> getRightType();
+        public Class<T2> getRightType() {
+                return rightType;
+        }
 
         public Term<T1> getLeft() {
                 return left;
@@ -60,12 +69,14 @@ public abstract class BinaryTerm<R, T1, T2> implements Term<R> {
 
         @Override
         public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
-                if (getClass() != other.getClass()) {
+                if (!super.equalsWithSubstitution(helper, other)) {
                         return false;
                 }
                 var otherBinaryTerm = (BinaryTerm<?, ?, ?>) other;
-                return left.equalsWithSubstitution(helper, otherBinaryTerm.left) && right.equalsWithSubstitution(helper,
-                                otherBinaryTerm.right);
+                return leftType.equals(otherBinaryTerm.leftType) &&
+                                rightType.equals(otherBinaryTerm.rightType) &&
+                                left.equalsWithSubstitution(helper, otherBinaryTerm.left) &&
+                                right.equalsWithSubstitution(helper, otherBinaryTerm.right);
         }
 
         @Override
@@ -87,12 +98,16 @@ public abstract class BinaryTerm<R, T1, T2> implements Term<R> {
         public boolean equals(Object o) {
                 if (this == o) return true;
                 if (o == null || getClass() != o.getClass()) return false;
+                if (!super.equals(o)) return false;
                 BinaryTerm<?, ?, ?> that = (BinaryTerm<?, ?, ?>) o;
-                return left.equals(that.left) && right.equals(that.right);
+                return Objects.equals(leftType, that.leftType) &&
+                                Objects.equals(rightType, that.rightType) &&
+                                Objects.equals(left, that.left) &&
+                                Objects.equals(right, that.right);
         }
 
         @Override
         public int hashCode() {
-                return Objects.hash(getClass(), left, right);
+                return Objects.hash(super.hashCode(), leftType, rightType, 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
deleted file mode 100644
index d04ae22c..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonOperator.java
+++ /dev/null
@@ -1,25 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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
deleted file mode 100644
index 2c304aef..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ComparisonTerm.java
+++ /dev/null
@@ -1,68 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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
index b03f07fd..2f6c56d1 100644
--- 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
@@ -9,21 +9,18 @@ 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 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()));
-                }
-        }
+public final class ConstantTerm<T> extends AbstractTerm<T> {
+        private final T value;
 
-        @Override
-        public Class<T> getType() {
-                return type;
+        public ConstantTerm(Class<T> type, T value) {
+                super(type);
+                if (value != null && !type.isInstance(value)) {
+                        throw new IllegalArgumentException("Value %s is not an instance of %s".formatted(value, type.getName()));
+                }
+                this.value = value;
         }
 
         public T getValue() {
@@ -42,7 +39,11 @@ public record ConstantTerm<T>(Class<T> type, T value) implements Term<T> {
 
         @Override
         public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
-                return equals(other);
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                var otherConstantTerm = (ConstantTerm<?>) other;
+                return Objects.equals(value, otherConstantTerm.value);
         }
 
         @Override
@@ -52,6 +53,19 @@ public record ConstantTerm<T>(Class<T> type, T value) implements Term<T> {
 
         @Override
         public String toString() {
-                return getValue().toString();
+                return value.toString();
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                ConstantTerm<?> that = (ConstantTerm<?>) o;
+                return Objects.equals(value, that.value);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(value);
         }
 }
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
deleted file mode 100644
index 6626365f..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/OpaqueTerm.java
+++ /dev/null
@@ -1,85 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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/UnaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/UnaryTerm.java
index 069e0d95..a46ebe31 100644
--- 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
@@ -12,18 +12,23 @@ import tools.refinery.store.query.valuation.Valuation;
 import java.util.Objects;
 import java.util.Set;
 
-public abstract class UnaryTerm<R, T> implements Term<R> {
+public abstract class UnaryTerm<R, T> extends AbstractTerm<R> {
+        private final Class<T> bodyType;
         private final Term<T> body;
 
-        protected UnaryTerm(Term<T> body) {
-                if (!body.getType().equals(getBodyType())) {
+        protected UnaryTerm(Class<R> type, Class<T> bodyType, Term<T> body) {
+                super(type);
+                if (!body.getType().equals(bodyType)) {
                         throw new IllegalArgumentException("Expected body %s to be of type %s, got %s instead".formatted(body,
-                                        getBodyType().getName(), body.getType().getName()));
+                                        bodyType.getName(), body.getType().getName()));
                 }
+                this.bodyType = bodyType;
                 this.body = body;
         }
 
-        public abstract Class<T> getBodyType();
+        public Class<T> getBodyType() {
+                return bodyType;
+        }
 
         public Term<T> getBody() {
                 return body;
@@ -39,11 +44,11 @@ public abstract class UnaryTerm<R, T> implements Term<R> {
 
         @Override
         public boolean equalsWithSubstitution(LiteralEqualityHelper helper, AnyTerm other) {
-                if (getClass() != other.getClass()) {
+                if (!super.equalsWithSubstitution(helper, other)) {
                         return false;
                 }
                 var otherUnaryTerm = (UnaryTerm<?, ?>) other;
-                return body.equalsWithSubstitution(helper, otherUnaryTerm.body);
+                return bodyType.equals(otherUnaryTerm.bodyType) && body.equalsWithSubstitution(helper, otherUnaryTerm.body);
         }
 
         @Override
@@ -62,12 +67,13 @@ public abstract class UnaryTerm<R, T> implements Term<R> {
         public boolean equals(Object o) {
                 if (this == o) return true;
                 if (o == null || getClass() != o.getClass()) return false;
+                if (!super.equals(o)) return false;
                 UnaryTerm<?, ?> unaryTerm = (UnaryTerm<?, ?>) o;
-                return body.equals(unaryTerm.body);
+                return Objects.equals(bodyType, unaryTerm.bodyType) && Objects.equals(body, unaryTerm.body);
         }
 
         @Override
         public int hashCode() {
-                return Objects.hash(getClass(), body);
+                return Objects.hash(super.hashCode(), bodyType, body);
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolAndTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolAndTerm.java
new file mode 100644
index 00000000..f9e1c06f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolAndTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.bool;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class BoolAndTerm extends BoolBinaryTerm {
+        public BoolAndTerm(Term<Boolean> left, Term<Boolean> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<Boolean> substitutedLeft,
+                                                                          Term<Boolean> substitutedRight) {
+                return new BoolAndTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Boolean doEvaluate(Boolean leftValue, Boolean rightValue) {
+                return leftValue && rightValue;
+        }
+
+        @Override
+        public String toString() {
+                return "(%s && %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolBinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolBinaryTerm.java
new file mode 100644
index 00000000..a85aa63a
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolBinaryTerm.java
@@ -0,0 +1,15 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.bool;
+
+import tools.refinery.store.query.term.BinaryTerm;
+import tools.refinery.store.query.term.Term;
+
+public abstract class BoolBinaryTerm extends BinaryTerm<Boolean, Boolean, Boolean> {
+        protected BoolBinaryTerm(Term<Boolean> left, Term<Boolean> right) {
+                super(Boolean.class, Boolean.class, Boolean.class, left, right);
+        }
+}
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
deleted file mode 100644
index e5690ab6..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolConstantTerm.java
+++ /dev/null
@@ -1,21 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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
deleted file mode 100644
index 11e764c2..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolLogicBinaryTerm.java
+++ /dev/null
@@ -1,83 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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
index bb06cf8b..8d3382b3 100644
--- 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
@@ -11,17 +11,7 @@ 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();
+                super(Boolean.class, Boolean.class, body);
         }
 
         @Override
@@ -36,6 +26,6 @@ public class BoolNotTerm extends UnaryTerm<Boolean, Boolean> {
 
         @Override
         public String toString() {
-                return "!(%s)".formatted(getBody());
+                return "(!%s)".formatted(getBody());
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolOrTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolOrTerm.java
new file mode 100644
index 00000000..b5195d52
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolOrTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.bool;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class BoolOrTerm extends BoolBinaryTerm {
+        public BoolOrTerm(Term<Boolean> left, Term<Boolean> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<Boolean> substitutedLeft,
+                                                                          Term<Boolean> substitutedRight) {
+                return new BoolOrTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Boolean doEvaluate(Boolean leftValue, Boolean rightValue) {
+                return leftValue || rightValue;
+        }
+
+        @Override
+        public String toString() {
+                return "(%s || %s)".formatted(getLeft(), getRight());
+        }
+}
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
index 55825952..fa54f686 100644
--- 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
@@ -13,23 +13,23 @@ public final class 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 Term<Boolean> constant(Boolean value) {
+                return new ConstantTerm<>(Boolean.class, value);
         }
 
-        public static BoolNotTerm not(Term<Boolean> body) {
+        public static Term<Boolean> 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 Term<Boolean> and(Term<Boolean> left, Term<Boolean> right) {
+                return new BoolAndTerm(left, right);
         }
 
-        public static BoolLogicBinaryTerm or(Term<Boolean> left, Term<Boolean> right) {
-                return new BoolLogicBinaryTerm(LogicBinaryOperator.OR, left, right);
+        public static Term<Boolean> or(Term<Boolean> left, Term<Boolean> right) {
+                return new BoolOrTerm(left, right);
         }
 
-        public static BoolLogicBinaryTerm xor(Term<Boolean> left, Term<Boolean> right) {
-                return new BoolLogicBinaryTerm(LogicBinaryOperator.XOR, left, right);
+        public static Term<Boolean> xor(Term<Boolean> left, Term<Boolean> right) {
+                return new BoolXorTerm(left, right);
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolXorTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolXorTerm.java
new file mode 100644
index 00000000..7478b8a5
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/BoolXorTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.bool;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class BoolXorTerm extends BoolBinaryTerm {
+        public BoolXorTerm(Term<Boolean> left, Term<Boolean> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<Boolean> substitutedLeft,
+                                                                          Term<Boolean> substitutedRight) {
+                return new BoolXorTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Boolean doEvaluate(Boolean leftValue, Boolean rightValue) {
+                return leftValue ^ rightValue;
+        }
+
+        @Override
+        public String toString() {
+                return "(%s ^^ %s)".formatted(getLeft(), getRight());
+        }
+}
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
deleted file mode 100644
index 93a72f88..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/bool/LogicBinaryOperator.java
+++ /dev/null
@@ -1,22 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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/comparable/ComparisonTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/ComparisonTerm.java
new file mode 100644
index 00000000..5ca5a0a1
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/ComparisonTerm.java
@@ -0,0 +1,19 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.comparable;
+
+import tools.refinery.store.query.term.BinaryTerm;
+import tools.refinery.store.query.term.Term;
+
+public abstract class ComparisonTerm<T> extends BinaryTerm<Boolean, T, T> {
+        protected ComparisonTerm(Class<T> argumentType, Term<T> left, Term<T> right) {
+                super(Boolean.class, argumentType, argumentType, left, right);
+        }
+
+        public Class<T> getArgumentType() {
+                return getLeftType();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/EqTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/EqTerm.java
new file mode 100644
index 00000000..b8cf36f8
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/EqTerm.java
@@ -0,0 +1,30 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.comparable;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class EqTerm<T> extends ComparisonTerm<T> {
+        public EqTerm(Class<T> argumentType, Term<T> left, Term<T> right) {
+                super(argumentType, left, right);
+        }
+
+        @Override
+        protected Boolean doEvaluate(T leftValue, T rightValue) {
+                return leftValue.equals(rightValue);
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<T> substitutedLeft, Term<T> substitutedRight) {
+                return new EqTerm<>(getArgumentType(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        public String toString() {
+                return "(%s == %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/GreaterEqTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/GreaterEqTerm.java
new file mode 100644
index 00000000..b109eb1a
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/GreaterEqTerm.java
@@ -0,0 +1,30 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.comparable;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class GreaterEqTerm<T extends Comparable<T>> extends ComparisonTerm<T> {
+        public GreaterEqTerm(Class<T> argumentType, Term<T> left, Term<T> right) {
+                super(argumentType, left, right);
+        }
+
+        @Override
+        protected Boolean doEvaluate(T leftValue, T rightValue) {
+                return leftValue.compareTo(rightValue) >= 0;
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<T> substitutedLeft, Term<T> substitutedRight) {
+                return new GreaterEqTerm<>(getArgumentType(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        public String toString() {
+                return "(%s >= %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/GreaterTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/GreaterTerm.java
new file mode 100644
index 00000000..1b67f8b5
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/GreaterTerm.java
@@ -0,0 +1,30 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.comparable;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class GreaterTerm<T extends Comparable<T>> extends ComparisonTerm<T> {
+        public GreaterTerm(Class<T> argumentType, Term<T> left, Term<T> right) {
+                super(argumentType, left, right);
+        }
+
+        @Override
+        protected Boolean doEvaluate(T leftValue, T rightValue) {
+                return leftValue.compareTo(rightValue) > 0;
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<T> substitutedLeft, Term<T> substitutedRight) {
+                return new GreaterTerm<>(getArgumentType(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        public String toString() {
+                return "(%s > %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/LessEqTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/LessEqTerm.java
new file mode 100644
index 00000000..1b34535f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/LessEqTerm.java
@@ -0,0 +1,30 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.comparable;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class LessEqTerm<T extends Comparable<T>> extends ComparisonTerm<T> {
+        public LessEqTerm(Class<T> argumentType, Term<T> left, Term<T> right) {
+                super(argumentType, left, right);
+        }
+
+        @Override
+        protected Boolean doEvaluate(T leftValue, T rightValue) {
+                return leftValue.compareTo(rightValue) <= 0;
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<T> substitutedLeft, Term<T> substitutedRight) {
+                return new LessEqTerm<>(getArgumentType(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        public String toString() {
+                return "(%s <= %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/LessTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/LessTerm.java
new file mode 100644
index 00000000..44e70902
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/LessTerm.java
@@ -0,0 +1,30 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.comparable;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class LessTerm<T extends Comparable<T>> extends ComparisonTerm<T> {
+        public LessTerm(Class<T> argumentType, Term<T> left, Term<T> right) {
+                super(argumentType, left, right);
+        }
+
+        @Override
+        protected Boolean doEvaluate(T leftValue, T rightValue) {
+                return leftValue.compareTo(rightValue) < 0;
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<T> substitutedLeft, Term<T> substitutedRight) {
+                return new LessTerm<>(getArgumentType(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        public String toString() {
+                return "(%s < %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/NotEqTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/NotEqTerm.java
new file mode 100644
index 00000000..1f9734c4
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/comparable/NotEqTerm.java
@@ -0,0 +1,30 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.comparable;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class NotEqTerm<T> extends ComparisonTerm<T> {
+        public NotEqTerm(Class<T> argumentType, Term<T> left, Term<T> right) {
+                super(argumentType, left, right);
+        }
+
+        @Override
+        protected Boolean doEvaluate(T leftValue, T rightValue) {
+                return !leftValue.equals(rightValue);
+        }
+
+        @Override
+        public Term<Boolean> doSubstitute(Substitution substitution, Term<T> substitutedLeft, Term<T> substitutedRight) {
+                return new NotEqTerm<>(getArgumentType(), substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        public String toString() {
+                return "(%s != %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntAddTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntAddTerm.java
new file mode 100644
index 00000000..dbea3efc
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntAddTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class IntAddTerm extends IntBinaryTerm {
+        public IntAddTerm(Term<Integer> left, Term<Integer> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Integer> doSubstitute(Substitution substitution, Term<Integer> substitutedLeft,
+                                                                          Term<Integer> substitutedRight) {
+                return new IntAddTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Integer doEvaluate(Integer leftValue, Integer rightValue) {
+                return leftValue + rightValue;
+        }
+
+        @Override
+        public String toString() {
+                return "(%s + %s)".formatted(getLeft(), getRight());
+        }
+}
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
deleted file mode 100644
index 8a76ecbd..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticBinaryTerm.java
+++ /dev/null
@@ -1,53 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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
deleted file mode 100644
index 8522f2c1..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntArithmeticUnaryTerm.java
+++ /dev/null
@@ -1,35 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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_/IntBinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntBinaryTerm.java
new file mode 100644
index 00000000..27ced4e4
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntBinaryTerm.java
@@ -0,0 +1,15 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.term.BinaryTerm;
+import tools.refinery.store.query.term.Term;
+
+public abstract class IntBinaryTerm extends BinaryTerm<Integer, Integer, Integer> {
+        protected IntBinaryTerm(Term<Integer> left, Term<Integer> right) {
+                super(Integer.class, Integer.class, Integer.class, left, right);
+        }
+}
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
deleted file mode 100644
index 2ce2b2f3..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntComparisonTerm.java
+++ /dev/null
@@ -1,39 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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_/IntDivTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntDivTerm.java
new file mode 100644
index 00000000..2a35058c
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntDivTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class IntDivTerm extends IntBinaryTerm {
+        public IntDivTerm(Term<Integer> left, Term<Integer> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Integer> doSubstitute(Substitution substitution, Term<Integer> substitutedLeft,
+                                                                          Term<Integer> substitutedRight) {
+                return new IntDivTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Integer doEvaluate(Integer leftValue, Integer rightValue) {
+                return rightValue == 0 ? null : leftValue / rightValue;
+        }
+
+        @Override
+        public String toString() {
+                return "(%s / %s)".formatted(getLeft(), getRight());
+        }
+}
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
deleted file mode 100644
index 7982f45c..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntExtremeValueAggregator.java
+++ /dev/null
@@ -1,22 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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_/IntMaxTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntMaxTerm.java
new file mode 100644
index 00000000..f81fc509
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntMaxTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class IntMaxTerm extends IntBinaryTerm {
+        public IntMaxTerm(Term<Integer> left, Term<Integer> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Integer> doSubstitute(Substitution substitution, Term<Integer> substitutedLeft,
+                                                                          Term<Integer> substitutedRight) {
+                return new IntMaxTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Integer doEvaluate(Integer leftValue, Integer rightValue) {
+                return Math.max(rightValue, leftValue);
+        }
+
+        @Override
+        public String toString() {
+                return "max(%s, %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntMinTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntMinTerm.java
new file mode 100644
index 00000000..89182e26
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntMinTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class IntMinTerm extends IntBinaryTerm {
+        public IntMinTerm(Term<Integer> left, Term<Integer> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Integer> doSubstitute(Substitution substitution, Term<Integer> substitutedLeft,
+                                                                          Term<Integer> substitutedRight) {
+                return new IntMinTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Integer doEvaluate(Integer leftValue, Integer rightValue) {
+                return Math.min(rightValue, leftValue);
+        }
+
+        @Override
+        public String toString() {
+                return "min(%s, %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntMinusTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntMinusTerm.java
new file mode 100644
index 00000000..709aa5ba
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntMinusTerm.java
@@ -0,0 +1,30 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class IntMinusTerm extends IntUnaryTerm {
+        public IntMinusTerm(Term<Integer> body) {
+                super(body);
+        }
+
+        @Override
+        protected Term<Integer> doSubstitute(Substitution substitution, Term<Integer> substitutedBody) {
+                return new IntMinusTerm(substitutedBody);
+        }
+
+        @Override
+        protected Integer doEvaluate(Integer 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/int_/IntMulTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntMulTerm.java
new file mode 100644
index 00000000..89d4c5f4
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntMulTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class IntMulTerm extends IntBinaryTerm {
+        public IntMulTerm(Term<Integer> left, Term<Integer> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Integer> doSubstitute(Substitution substitution, Term<Integer> substitutedLeft,
+                                                                          Term<Integer> substitutedRight) {
+                return new IntMulTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Integer doEvaluate(Integer leftValue, Integer rightValue) {
+                return leftValue * rightValue;
+        }
+
+        @Override
+        public String toString() {
+                return "(%s * %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntPlusTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntPlusTerm.java
new file mode 100644
index 00000000..aef83bb4
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntPlusTerm.java
@@ -0,0 +1,30 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class IntPlusTerm extends IntUnaryTerm {
+        public IntPlusTerm(Term<Integer> body) {
+                super(body);
+        }
+
+        @Override
+        protected Term<Integer> doSubstitute(Substitution substitution, Term<Integer> substitutedBody) {
+                return new IntPlusTerm(substitutedBody);
+        }
+
+        @Override
+        protected Integer doEvaluate(Integer 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/int_/IntPowTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntPowTerm.java
new file mode 100644
index 00000000..d5af97a1
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntPowTerm.java
@@ -0,0 +1,43 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class IntPowTerm extends IntBinaryTerm {
+        public IntPowTerm(Term<Integer> left, Term<Integer> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Integer> doSubstitute(Substitution substitution, Term<Integer> substitutedLeft,
+                                                                          Term<Integer> substitutedRight) {
+                return new IntPowTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Integer doEvaluate(Integer leftValue, Integer rightValue) {
+                return rightValue < 0 ? null : power(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;
+        }
+
+        @Override
+        public String toString() {
+                return "(%s ** %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntSubTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntSubTerm.java
new file mode 100644
index 00000000..2c27afb1
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntSubTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class IntSubTerm extends IntBinaryTerm {
+        public IntSubTerm(Term<Integer> left, Term<Integer> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Integer> doSubstitute(Substitution substitution, Term<Integer> substitutedLeft,
+                                                                          Term<Integer> substitutedRight) {
+                return new IntSubTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Integer doEvaluate(Integer leftValue, Integer rightValue) {
+                return leftValue - rightValue;
+        }
+
+        @Override
+        public String toString() {
+                return "(%s - %s)".formatted(getLeft(), getRight());
+        }
+}
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
index 38f7f449..acb98b94 100644
--- 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
@@ -5,82 +5,90 @@
  */
 package tools.refinery.store.query.term.int_;
 
-import tools.refinery.store.query.term.*;
+import tools.refinery.store.query.term.Aggregator;
+import tools.refinery.store.query.term.ConstantTerm;
+import tools.refinery.store.query.term.ExtremeValueAggregator;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.comparable.*;
+
+import java.util.Comparator;
 
 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;
+        public static final Aggregator<Integer, Integer> INT_MIN = new ExtremeValueAggregator<>(Integer.class,
+                        Integer.MAX_VALUE);
+        public static final Aggregator<Integer, Integer> INT_MAX = new ExtremeValueAggregator<>(Integer.class,
+                        Integer.MIN_VALUE, Comparator.reverseOrder());
 
         private IntTerms() {
                 throw new IllegalArgumentException("This is a static utility class and should not be instantiated directly");
         }
 
-        public static ConstantTerm<Integer> constant(int value) {
+        public static Term<Integer> constant(Integer value) {
                 return new ConstantTerm<>(Integer.class, value);
         }
 
-        public static IntArithmeticUnaryTerm plus(Term<Integer> body) {
-                return new IntArithmeticUnaryTerm(ArithmeticUnaryOperator.PLUS, body);
+        public static Term<Integer> plus(Term<Integer> body) {
+                return new IntPlusTerm(body);
         }
 
-        public static IntArithmeticUnaryTerm minus(Term<Integer> body) {
-                return new IntArithmeticUnaryTerm(ArithmeticUnaryOperator.MINUS, body);
+        public static Term<Integer> minus(Term<Integer> body) {
+                return new IntMinusTerm(body);
         }
 
-        public static IntArithmeticBinaryTerm add(Term<Integer> left, Term<Integer> right) {
-                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.ADD, left, right);
+        public static Term<Integer> add(Term<Integer> left, Term<Integer> right) {
+                return new IntAddTerm(left, right);
         }
 
-        public static IntArithmeticBinaryTerm sub(Term<Integer> left, Term<Integer> right) {
-                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.SUB, left, right);
+        public static Term<Integer> sub(Term<Integer> left, Term<Integer> right) {
+                return new IntSubTerm(left, right);
         }
 
-        public static IntArithmeticBinaryTerm mul(Term<Integer> left, Term<Integer> right) {
-                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.MUL, left, right);
+        public static Term<Integer> mul(Term<Integer> left, Term<Integer> right) {
+                return new IntMulTerm(left, right);
         }
 
-        public static IntArithmeticBinaryTerm div(Term<Integer> left, Term<Integer> right) {
-                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.DIV, left, right);
+        public static Term<Integer> div(Term<Integer> left, Term<Integer> right) {
+                return new IntDivTerm(left, right);
         }
 
-        public static IntArithmeticBinaryTerm pow(Term<Integer> left, Term<Integer> right) {
-                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.POW, left, right);
+        public static Term<Integer> pow(Term<Integer> left, Term<Integer> right) {
+                return new IntPowTerm(left, right);
         }
 
-        public static IntArithmeticBinaryTerm min(Term<Integer> left, Term<Integer> right) {
-                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.MIN, left, right);
+        public static Term<Integer> min(Term<Integer> left, Term<Integer> right) {
+                return new IntMinTerm(left, right);
         }
 
-        public static IntArithmeticBinaryTerm max(Term<Integer> left, Term<Integer> right) {
-                return new IntArithmeticBinaryTerm(ArithmeticBinaryOperator.MAX, left, right);
+        public static Term<Integer> max(Term<Integer> left, Term<Integer> right) {
+                return new IntMaxTerm(left, right);
         }
 
-        public static IntComparisonTerm eq(Term<Integer> left, Term<Integer> right) {
-                return new IntComparisonTerm(ComparisonOperator.EQ, left, right);
+        public static Term<Boolean> eq(Term<Integer> left, Term<Integer> right) {
+                return new EqTerm<>(Integer.class, left, right);
         }
 
-        public static IntComparisonTerm notEq(Term<Integer> left, Term<Integer> right) {
-                return new IntComparisonTerm(ComparisonOperator.NOT_EQ, left, right);
+        public static Term<Boolean> notEq(Term<Integer> left, Term<Integer> right) {
+                return new NotEqTerm<>(Integer.class, left, right);
         }
 
-        public static IntComparisonTerm less(Term<Integer> left, Term<Integer> right) {
-                return new IntComparisonTerm(ComparisonOperator.LESS, left, right);
+        public static Term<Boolean> less(Term<Integer> left, Term<Integer> right) {
+                return new LessTerm<>(Integer.class, left, right);
         }
 
-        public static IntComparisonTerm lessEq(Term<Integer> left, Term<Integer> right) {
-                return new IntComparisonTerm(ComparisonOperator.LESS_EQ, left, right);
+        public static Term<Boolean> lessEq(Term<Integer> left, Term<Integer> right) {
+                return new LessEqTerm<>(Integer.class, left, right);
         }
 
-        public static IntComparisonTerm greater(Term<Integer> left, Term<Integer> right) {
-                return new IntComparisonTerm(ComparisonOperator.GREATER, left, right);
+        public static Term<Boolean> greater(Term<Integer> left, Term<Integer> right) {
+                return new GreaterTerm<>(Integer.class, left, right);
         }
 
-        public static IntComparisonTerm greaterEq(Term<Integer> left, Term<Integer> right) {
-                return new IntComparisonTerm(ComparisonOperator.GREATER_EQ, left, right);
+        public static Term<Boolean> greaterEq(Term<Integer> left, Term<Integer> right) {
+                return new GreaterEqTerm<>(Integer.class, left, right);
         }
 
-        public static RealToIntTerm asInt(Term<Double> body) {
+        public static Term<Integer> asInt(Term<Double> body) {
                 return new RealToIntTerm(body);
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntUnaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntUnaryTerm.java
new file mode 100644
index 00000000..49b4c647
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/int_/IntUnaryTerm.java
@@ -0,0 +1,15 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.int_;
+
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.UnaryTerm;
+
+public abstract class IntUnaryTerm extends UnaryTerm<Integer, Integer> {
+        protected IntUnaryTerm(Term<Integer> body) {
+                super(Integer.class, Integer.class, 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
index 399adf4a..7d383562 100644
--- 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
@@ -11,22 +11,12 @@ 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;
+                super(Integer.class, Double.class, body);
         }
 
         @Override
         protected Integer doEvaluate(Double bodyValue) {
-                return bodyValue.intValue();
+                return bodyValue.isNaN() ? null : bodyValue.intValue();
         }
 
         @Override
@@ -36,6 +26,6 @@ public class RealToIntTerm extends UnaryTerm<Integer, Double> {
 
         @Override
         public String toString() {
-                return "(%s) as int".formatted(getBody());
+                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
index 4f7d5687..2f53117a 100644
--- 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
@@ -11,17 +11,7 @@ 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;
+                super(Double.class, Integer.class, body);
         }
 
         @Override
@@ -36,6 +26,6 @@ public class IntToRealTerm extends UnaryTerm<Double, Integer> {
 
         @Override
         public String toString() {
-                return "(%s) as real".formatted(getBody());
+                return "(%s as real)".formatted(getBody());
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealAddTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealAddTerm.java
new file mode 100644
index 00000000..33fc9e41
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealAddTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class RealAddTerm extends RealBinaryTerm {
+        public RealAddTerm(Term<Double> left, Term<Double> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Double> doSubstitute(Substitution substitution, Term<Double> substitutedLeft,
+                                                                         Term<Double> substitutedRight) {
+                return new RealAddTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Double doEvaluate(Double leftValue, Double rightValue) {
+                return leftValue + rightValue;
+        }
+
+        @Override
+        public String toString() {
+                return "(%s + %s)".formatted(getLeft(), getRight());
+        }
+}
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
deleted file mode 100644
index 8d5c9242..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticBinaryTerm.java
+++ /dev/null
@@ -1,41 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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
deleted file mode 100644
index 9d233dfc..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealArithmeticUnaryTerm.java
+++ /dev/null
@@ -1,35 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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/RealBinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealBinaryTerm.java
new file mode 100644
index 00000000..000f3623
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealBinaryTerm.java
@@ -0,0 +1,15 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.term.BinaryTerm;
+import tools.refinery.store.query.term.Term;
+
+public abstract class RealBinaryTerm extends BinaryTerm<Double, Double, Double> {
+        protected RealBinaryTerm(Term<Double> left, Term<Double> right) {
+                super(Double.class, Double.class, Double.class, left, right);
+        }
+}
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
deleted file mode 100644
index 25c88f89..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealComparisonTerm.java
+++ /dev/null
@@ -1,40 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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/RealDivTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealDivTerm.java
new file mode 100644
index 00000000..1e55bf42
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealDivTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class RealDivTerm extends RealBinaryTerm {
+        public RealDivTerm(Term<Double> left, Term<Double> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Double> doSubstitute(Substitution substitution, Term<Double> substitutedLeft,
+                                                                         Term<Double> substitutedRight) {
+                return new RealDivTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Double doEvaluate(Double leftValue, Double rightValue) {
+                return leftValue / rightValue;
+        }
+
+        @Override
+        public String toString() {
+                return "(%s / %s)".formatted(getLeft(), getRight());
+        }
+}
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
deleted file mode 100644
index 526e643b..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealExtremeValueAggregator.java
+++ /dev/null
@@ -1,22 +0,0 @@
-/*
- * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
- *
- * SPDX-License-Identifier: EPL-2.0
- */
-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/RealMaxTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealMaxTerm.java
new file mode 100644
index 00000000..2a249496
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealMaxTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class RealMaxTerm extends RealBinaryTerm {
+        public RealMaxTerm(Term<Double> left, Term<Double> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Double> doSubstitute(Substitution substitution, Term<Double> substitutedLeft,
+                                                                         Term<Double> substitutedRight) {
+                return new RealMaxTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Double doEvaluate(Double leftValue, Double rightValue) {
+                return Math.max(leftValue, rightValue);
+        }
+
+        @Override
+        public String toString() {
+                return "max(%s, %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealMinTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealMinTerm.java
new file mode 100644
index 00000000..2eb4cc1e
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealMinTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class RealMinTerm extends RealBinaryTerm {
+        public RealMinTerm(Term<Double> left, Term<Double> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Double> doSubstitute(Substitution substitution, Term<Double> substitutedLeft,
+                                                                         Term<Double> substitutedRight) {
+                return new RealMinTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Double doEvaluate(Double leftValue, Double rightValue) {
+                return Math.min(leftValue, rightValue);
+        }
+
+        @Override
+        public String toString() {
+                return "min(%s, %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealMinusTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealMinusTerm.java
new file mode 100644
index 00000000..4afec7a1
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealMinusTerm.java
@@ -0,0 +1,30 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class RealMinusTerm extends RealUnaryTerm {
+        public RealMinusTerm(Term<Double> body) {
+                super(body);
+        }
+
+        @Override
+        protected Term<Double> doSubstitute(Substitution substitution, Term<Double> substitutedBody) {
+                return new RealMinusTerm(substitutedBody);
+        }
+
+        @Override
+        protected Double doEvaluate(Double 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/real/RealMulTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealMulTerm.java
new file mode 100644
index 00000000..ec95ac6f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealMulTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class RealMulTerm extends RealBinaryTerm {
+        public RealMulTerm(Term<Double> left, Term<Double> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Double> doSubstitute(Substitution substitution, Term<Double> substitutedLeft,
+                                                                         Term<Double> substitutedRight) {
+                return new RealMulTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Double doEvaluate(Double leftValue, Double rightValue) {
+                return leftValue * rightValue;
+        }
+
+        @Override
+        public String toString() {
+                return "(%s * %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealPlusTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealPlusTerm.java
new file mode 100644
index 00000000..64dd2e70
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealPlusTerm.java
@@ -0,0 +1,30 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class RealPlusTerm extends RealUnaryTerm {
+        public RealPlusTerm(Term<Double> body) {
+                super(body);
+        }
+
+        @Override
+        protected Term<Double> doSubstitute(Substitution substitution, Term<Double> substitutedBody) {
+                return new RealPlusTerm(substitutedBody);
+        }
+
+        @Override
+        protected Double doEvaluate(Double 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/real/RealPowTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealPowTerm.java
new file mode 100644
index 00000000..11c952ea
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealPowTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class RealPowTerm extends RealBinaryTerm {
+        public RealPowTerm(Term<Double> left, Term<Double> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Double> doSubstitute(Substitution substitution, Term<Double> substitutedLeft,
+                                                                         Term<Double> substitutedRight) {
+                return new RealPowTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Double doEvaluate(Double leftValue, Double rightValue) {
+                return Math.pow(leftValue, rightValue);
+        }
+
+        @Override
+        public String toString() {
+                return "(%s ** %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealSubTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealSubTerm.java
new file mode 100644
index 00000000..8cc701ed
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealSubTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+
+public class RealSubTerm extends RealBinaryTerm {
+        public RealSubTerm(Term<Double> left, Term<Double> right) {
+                super(left, right);
+        }
+
+        @Override
+        public Term<Double> doSubstitute(Substitution substitution, Term<Double> substitutedLeft,
+                                                                         Term<Double> substitutedRight) {
+                return new RealSubTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        protected Double doEvaluate(Double leftValue, Double rightValue) {
+                return leftValue - rightValue;
+        }
+
+        @Override
+        public String toString() {
+                return "(%s - %s)".formatted(getLeft(), getRight());
+        }
+}
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
index 1240d478..79220358 100644
--- 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
@@ -5,82 +5,90 @@
  */
 package tools.refinery.store.query.term.real;
 
-import tools.refinery.store.query.term.*;
+import tools.refinery.store.query.term.Aggregator;
+import tools.refinery.store.query.term.ConstantTerm;
+import tools.refinery.store.query.term.ExtremeValueAggregator;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.comparable.*;
+
+import java.util.Comparator;
 
 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;
+        public static final Aggregator<Double, Double> REAL_MIN = new ExtremeValueAggregator<>(Double.class,
+                        Double.POSITIVE_INFINITY);
+        public static final Aggregator<Double, Double> REAL_MAX = new ExtremeValueAggregator<>(Double.class,
+                        Double.NEGATIVE_INFINITY, Comparator.reverseOrder());
 
         private RealTerms() {
                 throw new IllegalArgumentException("This is a static utility class and should not be instantiated directly");
         }
 
-        public static ConstantTerm<Double> constant(double value) {
+        public static Term<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 Term<Double> plus(Term<Double> body) {
+                return new RealPlusTerm(body);
         }
 
-        public static RealArithmeticUnaryTerm minus(Term<Double> body) {
-                return new RealArithmeticUnaryTerm(ArithmeticUnaryOperator.MINUS, body);
+        public static Term<Double> minus(Term<Double> body) {
+                return new RealMinusTerm(body);
         }
 
-        public static RealArithmeticBinaryTerm add(Term<Double> left, Term<Double> right) {
-                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.ADD, left, right);
+        public static Term<Double> add(Term<Double> left, Term<Double> right) {
+                return new RealAddTerm(left, right);
         }
 
-        public static RealArithmeticBinaryTerm sub(Term<Double> left, Term<Double> right) {
-                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.SUB, left, right);
+        public static Term<Double> sub(Term<Double> left, Term<Double> right) {
+                return new RealSubTerm(left, right);
         }
 
-        public static RealArithmeticBinaryTerm mul(Term<Double> left, Term<Double> right) {
-                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.MUL, left, right);
+        public static Term<Double> mul(Term<Double> left, Term<Double> right) {
+                return new RealMulTerm(left, right);
         }
 
-        public static RealArithmeticBinaryTerm div(Term<Double> left, Term<Double> right) {
-                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.DIV, left, right);
+        public static Term<Double> div(Term<Double> left, Term<Double> right) {
+                return new RealDivTerm(left, right);
         }
 
-        public static RealArithmeticBinaryTerm pow(Term<Double> left, Term<Double> right) {
-                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.POW, left, right);
+        public static Term<Double> pow(Term<Double> left, Term<Double> right) {
+                return new RealPowTerm(left, right);
         }
 
-        public static RealArithmeticBinaryTerm min(Term<Double> left, Term<Double> right) {
-                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.MIN, left, right);
+        public static Term<Double> min(Term<Double> left, Term<Double> right) {
+                return new RealMinTerm(left, right);
         }
 
-        public static RealArithmeticBinaryTerm max(Term<Double> left, Term<Double> right) {
-                return new RealArithmeticBinaryTerm(ArithmeticBinaryOperator.MAX, left, right);
+        public static Term<Double> max(Term<Double> left, Term<Double> right) {
+                return new RealMaxTerm(left, right);
         }
 
-        public static RealComparisonTerm eq(Term<Double> left, Term<Double> right) {
-                return new RealComparisonTerm(ComparisonOperator.EQ, left, right);
+        public static Term<Boolean> eq(Term<Double> left, Term<Double> right) {
+                return new EqTerm<>(Double.class, left, right);
         }
 
-        public static RealComparisonTerm notEq(Term<Double> left, Term<Double> right) {
-                return new RealComparisonTerm(ComparisonOperator.NOT_EQ, left, right);
+        public static Term<Boolean> notEq(Term<Double> left, Term<Double> right) {
+                return new NotEqTerm<>(Double.class, left, right);
         }
 
-        public static RealComparisonTerm less(Term<Double> left, Term<Double> right) {
-                return new RealComparisonTerm(ComparisonOperator.LESS, left, right);
+        public static Term<Boolean> less(Term<Double> left, Term<Double> right) {
+                return new LessTerm<>(Double.class, left, right);
         }
 
-        public static RealComparisonTerm lessEq(Term<Double> left, Term<Double> right) {
-                return new RealComparisonTerm(ComparisonOperator.LESS_EQ, left, right);
+        public static Term<Boolean> lessEq(Term<Double> left, Term<Double> right) {
+                return new LessEqTerm<>(Double.class, left, right);
         }
 
-        public static RealComparisonTerm greater(Term<Double> left, Term<Double> right) {
-                return new RealComparisonTerm(ComparisonOperator.GREATER, left, right);
+        public static Term<Boolean> greater(Term<Double> left, Term<Double> right) {
+                return new GreaterTerm<>(Double.class, left, right);
         }
 
-        public static RealComparisonTerm greaterEq(Term<Double> left, Term<Double> right) {
-                return new RealComparisonTerm(ComparisonOperator.GREATER_EQ, left, right);
+        public static Term<Boolean> greaterEq(Term<Double> left, Term<Double> right) {
+                return new GreaterEqTerm<>(Double.class, left, right);
         }
 
-        public static IntToRealTerm asReal(Term<Integer> body) {
+        public static Term<Double> asReal(Term<Integer> body) {
                 return new IntToRealTerm(body);
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealUnaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealUnaryTerm.java
new file mode 100644
index 00000000..d41c4ed9
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/real/RealUnaryTerm.java
@@ -0,0 +1,15 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.real;
+
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.UnaryTerm;
+
+public abstract class RealUnaryTerm extends UnaryTerm<Double, Double> {
+        protected RealUnaryTerm(Term<Double> body) {
+                super(Double.class, Double.class, body);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityAddTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityAddTerm.java
new file mode 100644
index 00000000..68905f51
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityAddTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.uppercardinality;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+public class UpperCardinalityAddTerm extends UpperCardinalityBinaryTerm {
+        protected UpperCardinalityAddTerm(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                super(left, right);
+        }
+
+        @Override
+        protected UpperCardinality doEvaluate(UpperCardinality leftValue, UpperCardinality rightValue) {
+                return leftValue.add(rightValue);
+        }
+
+        @Override
+        public Term<UpperCardinality> doSubstitute(Substitution substitution, Term<UpperCardinality> substitutedLeft, Term<UpperCardinality> substitutedRight) {
+                return new UpperCardinalityAddTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        public String toString() {
+                return "(%s + %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityBinaryTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityBinaryTerm.java
new file mode 100644
index 00000000..0cf8fe44
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityBinaryTerm.java
@@ -0,0 +1,17 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.uppercardinality;
+
+import tools.refinery.store.query.term.BinaryTerm;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+public abstract class UpperCardinalityBinaryTerm extends BinaryTerm<UpperCardinality, UpperCardinality,
+                UpperCardinality> {
+        protected UpperCardinalityBinaryTerm(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                super(UpperCardinality.class, UpperCardinality.class, UpperCardinality.class, left, right);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityMaxTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityMaxTerm.java
new file mode 100644
index 00000000..ff75f64e
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityMaxTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.uppercardinality;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+public class UpperCardinalityMaxTerm extends UpperCardinalityBinaryTerm {
+        protected UpperCardinalityMaxTerm(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                super(left, right);
+        }
+
+        @Override
+        protected UpperCardinality doEvaluate(UpperCardinality leftValue, UpperCardinality rightValue) {
+                return leftValue.max(rightValue);
+        }
+
+        @Override
+        public Term<UpperCardinality> doSubstitute(Substitution substitution, Term<UpperCardinality> substitutedLeft, Term<UpperCardinality> substitutedRight) {
+                return new UpperCardinalityMaxTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        public String toString() {
+                return "max(%s, %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityMinTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityMinTerm.java
new file mode 100644
index 00000000..1e89e9f4
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityMinTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.uppercardinality;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+public class UpperCardinalityMinTerm extends UpperCardinalityBinaryTerm {
+        protected UpperCardinalityMinTerm(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                super(left, right);
+        }
+
+        @Override
+        protected UpperCardinality doEvaluate(UpperCardinality leftValue, UpperCardinality rightValue) {
+                return leftValue.min(rightValue);
+        }
+
+        @Override
+        public Term<UpperCardinality> doSubstitute(Substitution substitution, Term<UpperCardinality> substitutedLeft, Term<UpperCardinality> substitutedRight) {
+                return new UpperCardinalityMinTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        public String toString() {
+                return "min(%s, %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityMulTerm.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityMulTerm.java
new file mode 100644
index 00000000..3b4970f4
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityMulTerm.java
@@ -0,0 +1,31 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.uppercardinality;
+
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+public class UpperCardinalityMulTerm extends UpperCardinalityBinaryTerm {
+        protected UpperCardinalityMulTerm(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                super(left, right);
+        }
+
+        @Override
+        protected UpperCardinality doEvaluate(UpperCardinality leftValue, UpperCardinality rightValue) {
+                return leftValue.multiply(rightValue);
+        }
+
+        @Override
+        public Term<UpperCardinality> doSubstitute(Substitution substitution, Term<UpperCardinality> substitutedLeft, Term<UpperCardinality> substitutedRight) {
+                return new UpperCardinalityMulTerm(substitutedLeft, substitutedRight);
+        }
+
+        @Override
+        public String toString() {
+                return "(%s * %s)".formatted(getLeft(), getRight());
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregator.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregator.java
new file mode 100644
index 00000000..5bbd3081
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregator.java
@@ -0,0 +1,86 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.uppercardinality;
+
+import tools.refinery.store.query.term.StatefulAggregate;
+import tools.refinery.store.query.term.StatefulAggregator;
+import tools.refinery.store.representation.cardinality.FiniteUpperCardinality;
+import tools.refinery.store.representation.cardinality.UnboundedUpperCardinality;
+import tools.refinery.store.representation.cardinality.UpperCardinalities;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+public class UpperCardinalitySumAggregator implements StatefulAggregator<UpperCardinality, UpperCardinality> {
+        public static final UpperCardinalitySumAggregator INSTANCE = new UpperCardinalitySumAggregator();
+
+        private UpperCardinalitySumAggregator() {
+        }
+
+        @Override
+        public Class<UpperCardinality> getResultType() {
+                return UpperCardinality.class;
+        }
+
+        @Override
+        public Class<UpperCardinality> getInputType() {
+                return UpperCardinality.class;
+        }
+
+        @Override
+        public StatefulAggregate<UpperCardinality, UpperCardinality> createEmptyAggregate() {
+                return new Aggregate();
+        }
+
+        private static class Aggregate implements StatefulAggregate<UpperCardinality, UpperCardinality> {
+                private int sumFiniteUpperBounds;
+                private int countUnbounded;
+
+                public Aggregate() {
+                        this(0, 0);
+                }
+
+                private Aggregate(int sumFiniteUpperBounds, int countUnbounded) {
+                        this.sumFiniteUpperBounds = sumFiniteUpperBounds;
+                        this.countUnbounded = countUnbounded;
+                }
+
+                @Override
+                public void add(UpperCardinality value) {
+                        if (value instanceof FiniteUpperCardinality finiteUpperCardinality) {
+                                sumFiniteUpperBounds += finiteUpperCardinality.finiteUpperBound();
+                        } else if (value instanceof UnboundedUpperCardinality) {
+                                countUnbounded += 1;
+                        } else {
+                                throw new IllegalArgumentException("Unknown UpperCardinality: " + value);
+                        }
+                }
+
+                @Override
+                public void remove(UpperCardinality value) {
+                        if (value instanceof FiniteUpperCardinality finiteUpperCardinality) {
+                                sumFiniteUpperBounds -= finiteUpperCardinality.finiteUpperBound();
+                        } else if (value instanceof UnboundedUpperCardinality) {
+                                countUnbounded -= 1;
+                        } else {
+                                throw new IllegalArgumentException("Unknown UpperCardinality: " + value);
+                        }
+                }
+
+                @Override
+                public UpperCardinality getResult() {
+                        return countUnbounded > 0 ? UpperCardinalities.UNBOUNDED : UpperCardinalities.valueOf(sumFiniteUpperBounds);
+                }
+
+                @Override
+                public boolean isEmpty() {
+                        return sumFiniteUpperBounds == 0 && countUnbounded == 0;
+                }
+
+                @Override
+                public StatefulAggregate<UpperCardinality, UpperCardinality> deepCopy() {
+                        return new Aggregate(sumFiniteUpperBounds, countUnbounded);
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityTerms.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityTerms.java
new file mode 100644
index 00000000..13914f2d
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityTerms.java
@@ -0,0 +1,73 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.uppercardinality;
+
+import tools.refinery.store.query.term.Aggregator;
+import tools.refinery.store.query.term.ConstantTerm;
+import tools.refinery.store.query.term.ExtremeValueAggregator;
+import tools.refinery.store.query.term.Term;
+import tools.refinery.store.query.term.comparable.*;
+import tools.refinery.store.representation.cardinality.UpperCardinalities;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+import java.util.Comparator;
+
+public final class UpperCardinalityTerms {
+        public static final Aggregator<UpperCardinality, UpperCardinality> UPPER_CARDINALITY_SUM =
+                        UpperCardinalitySumAggregator.INSTANCE;
+        public static final Aggregator<UpperCardinality, UpperCardinality> UPPER_CARDINALITY_MIN =
+                        new ExtremeValueAggregator<>(UpperCardinality.class, UpperCardinalities.UNBOUNDED);
+        public static final Aggregator<UpperCardinality, UpperCardinality> UPPER_CARDINALITY_MAX =
+                        new ExtremeValueAggregator<>(UpperCardinality.class, UpperCardinalities.ZERO, Comparator.reverseOrder());
+
+        private UpperCardinalityTerms() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static Term<UpperCardinality> constant(UpperCardinality value) {
+                return new ConstantTerm<>(UpperCardinality.class, value);
+        }
+
+        public static Term<UpperCardinality> add(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                return new UpperCardinalityAddTerm(left, right);
+        }
+
+        public static Term<UpperCardinality> mul(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                return new UpperCardinalityMulTerm(left, right);
+        }
+
+        public static Term<UpperCardinality> min(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                return new UpperCardinalityMinTerm(left, right);
+        }
+
+        public static Term<UpperCardinality> max(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                return new UpperCardinalityMaxTerm(left, right);
+        }
+
+        public static Term<Boolean> eq(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                return new EqTerm<>(UpperCardinality.class, left, right);
+        }
+
+        public static Term<Boolean> notEq(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                return new NotEqTerm<>(UpperCardinality.class, left, right);
+        }
+
+        public static Term<Boolean> less(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                return new LessTerm<>(UpperCardinality.class, left, right);
+        }
+
+        public static Term<Boolean> lessEq(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                return new LessEqTerm<>(UpperCardinality.class, left, right);
+        }
+
+        public static Term<Boolean> greater(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                return new GreaterTerm<>(UpperCardinality.class, left, right);
+        }
+
+        public static Term<Boolean> greaterEq(Term<UpperCardinality> left, Term<UpperCardinality> right) {
+                return new GreaterEqTerm<>(UpperCardinality.class, left, right);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/MapBasedValuation.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/MapBasedValuation.java
new file mode 100644
index 00000000..261ceaa5
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/MapBasedValuation.java
@@ -0,0 +1,22 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.valuation;
+
+import tools.refinery.store.query.term.AnyDataVariable;
+import tools.refinery.store.query.term.DataVariable;
+
+import java.util.Map;
+
+record MapBasedValuation(Map<AnyDataVariable, Object> values) implements Valuation {
+        @Override
+        public <T> T getValue(DataVariable<T> variable) {
+                if (!values.containsKey(variable)) {
+                        throw new IllegalArgumentException("No value for variable %s".formatted(variable));
+                }
+                var value = values.get(variable);
+                return variable.getType().cast(value);
+        }
+}
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
index 88fee35b..1588e957 100644
--- 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
@@ -10,6 +10,7 @@ import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.AnyDataVariable;
 import tools.refinery.store.query.term.DataVariable;
 
+import java.util.Map;
 import java.util.Set;
 
 public interface Valuation {
@@ -25,4 +26,12 @@ public interface Valuation {
         default Valuation restrict(Set<? extends AnyDataVariable> allowedVariables) {
                 return new RestrictedValuation(this, Set.copyOf(allowedVariables));
         }
+
+        static ValuationBuilder builder() {
+                return new ValuationBuilder();
+        }
+
+        static Valuation empty() {
+                return new MapBasedValuation(Map.of());
+        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/ValuationBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/ValuationBuilder.java
new file mode 100644
index 00000000..7337dbc3
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/valuation/ValuationBuilder.java
@@ -0,0 +1,40 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.valuation;
+
+import tools.refinery.store.query.term.AnyDataVariable;
+import tools.refinery.store.query.term.DataVariable;
+
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.Map;
+
+public class ValuationBuilder {
+        private final Map<AnyDataVariable, Object> values = new HashMap<>();
+
+        ValuationBuilder() {
+        }
+
+        public <T> ValuationBuilder put(DataVariable<T> variable, T value) {
+                return putChecked(variable, value);
+        }
+
+        public ValuationBuilder putChecked(AnyDataVariable variable, Object value) {
+                if (value != null && !variable.getType().isInstance(value)) {
+                        throw new IllegalArgumentException("Value %s is not an instance of %s"
+                                        .formatted(value, variable.getType().getName()));
+                }
+                if (values.containsKey(variable)) {
+                        throw new IllegalArgumentException("Already has value for variable %s".formatted(variable));
+                }
+                values.put(variable, value);
+                return this;
+        }
+
+        public Valuation build() {
+                return new MapBasedValuation(Collections.unmodifiableMap(values));
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java
index 152840f8..01e2ccf6 100644
--- a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java
@@ -6,13 +6,17 @@
 package tools.refinery.store.query;
 
 import org.junit.jupiter.api.Test;
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.CsvSource;
 import tools.refinery.store.query.dnf.Dnf;
 import tools.refinery.store.query.literal.BooleanLiteral;
 import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.term.bool.BoolTerms;
 import tools.refinery.store.query.view.KeyOnlyView;
 import tools.refinery.store.representation.Symbol;
 
 import static org.hamcrest.MatcherAssert.assertThat;
+import static tools.refinery.store.query.literal.Literals.assume;
 import static tools.refinery.store.query.literal.Literals.not;
 import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo;
 
@@ -34,6 +38,22 @@ class DnfBuilderTest {
         }
 
         @Test
+        void eliminateTrueAssumptionTest() {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(assume(BoolTerms.constant(true)), friendView.call(p, q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
         void eliminateFalseTest() {
                 var p = Variable.of("p");
                 var q = Variable.of("q");
@@ -50,6 +70,27 @@ class DnfBuilderTest {
                 assertThat(actual, structurallyEqualTo(expected));
         }
 
+        @ParameterizedTest
+        @CsvSource(value = {
+                        "false",
+                        "null"
+        }, nullValues = "null")
+        void eliminateFalseAssumptionTest(Boolean value) {
+                var p = Variable.of("p");
+                var q = Variable.of("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(friendView.call(q, p), assume(BoolTerms.constant(value)))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
         @Test
         void alwaysTrueTest() {
                 var p = Variable.of("p");
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/term/TermSubstitutionTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/TermSubstitutionTest.java
new file mode 100644
index 00000000..1cbc101a
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/TermSubstitutionTest.java
@@ -0,0 +1,97 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term;
+
+import org.junit.jupiter.api.Assertions;
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.Arguments;
+import org.junit.jupiter.params.provider.MethodSource;
+import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.bool.BoolTerms;
+import tools.refinery.store.query.term.int_.IntTerms;
+import tools.refinery.store.query.term.real.RealTerms;
+import tools.refinery.store.query.term.uppercardinality.UpperCardinalityTerms;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+import java.util.List;
+import java.util.stream.Stream;
+
+class TermSubstitutionTest {
+        private final static DataVariable<Integer> intA = Variable.of("intA", Integer.class);
+        private final static DataVariable<Integer> intB = Variable.of("intB", Integer.class);
+        private final static DataVariable<Double> realA = Variable.of("realA", Double.class);
+        private final static DataVariable<Double> realB = Variable.of("realB", Double.class);
+        private final static DataVariable<Boolean> boolA = Variable.of("boolA", Boolean.class);
+        private final static DataVariable<Boolean> boolB = Variable.of("boolB", Boolean.class);
+        private final static DataVariable<UpperCardinality> upperCardinalityA = Variable.of("upperCardinalityA",
+                        UpperCardinality.class);
+        private final static DataVariable<UpperCardinality> upperCardinalityB = Variable.of("upperCardinalityB",
+                        UpperCardinality.class);
+        private final static Substitution substitution = Substitution.builder()
+                        .put(intA, intB)
+                        .put(intB, intA)
+                        .put(realA, realB)
+                        .put(realB, realA)
+                        .put(boolA, boolB)
+                        .put(boolB, boolA)
+                        .put(upperCardinalityA, upperCardinalityB)
+                        .put(upperCardinalityB, upperCardinalityA)
+                        .build();
+
+        @ParameterizedTest
+        @MethodSource
+        void substitutionTest(AnyTerm term) {
+                var substitutedTerm1 = term.substitute(substitution);
+                Assertions.assertNotEquals(term, substitutedTerm1, "Original term is not equal to substituted term");
+                var helper = new LiteralEqualityHelper(Dnf::equals, List.of(), List.of());
+                Assertions.assertTrue(term.equalsWithSubstitution(helper, substitutedTerm1), "Terms are equal by helper");
+                // The {@link #substitution} is its own inverse.
+                var substitutedTerm2 = substitutedTerm1.substitute(substitution);
+                Assertions.assertEquals(term, substitutedTerm2, "Original term is not equal to back-substituted term");
+        }
+
+        static Stream<Arguments> substitutionTest() {
+                return Stream.of(
+                                Arguments.of(IntTerms.plus(intA)),
+                                Arguments.of(IntTerms.minus(intA)),
+                                Arguments.of(IntTerms.add(intA, intB)),
+                                Arguments.of(IntTerms.sub(intA, intB)),
+                                Arguments.of(IntTerms.mul(intA, intB)),
+                                Arguments.of(IntTerms.div(intA, intB)),
+                                Arguments.of(IntTerms.pow(intA, intB)),
+                                Arguments.of(IntTerms.min(intA, intB)),
+                                Arguments.of(IntTerms.max(intA, intB)),
+                                Arguments.of(IntTerms.eq(intA, intB)),
+                                Arguments.of(IntTerms.notEq(intA, intB)),
+                                Arguments.of(IntTerms.less(intA, intB)),
+                                Arguments.of(IntTerms.lessEq(intA, intB)),
+                                Arguments.of(IntTerms.greater(intA, intB)),
+                                Arguments.of(IntTerms.greaterEq(intA, intB)),
+                                Arguments.of(IntTerms.asInt(realA)),
+                                Arguments.of(RealTerms.plus(realA)),
+                                Arguments.of(RealTerms.minus(realA)),
+                                Arguments.of(RealTerms.add(realA, realB)),
+                                Arguments.of(RealTerms.sub(realA, realB)),
+                                Arguments.of(RealTerms.mul(realA, realB)),
+                                Arguments.of(RealTerms.div(realA, realB)),
+                                Arguments.of(RealTerms.pow(realA, realB)),
+                                Arguments.of(RealTerms.min(realA, realB)),
+                                Arguments.of(RealTerms.max(realA, realB)),
+                                Arguments.of(RealTerms.asReal(intA)),
+                                Arguments.of(BoolTerms.not(boolA)),
+                                Arguments.of(BoolTerms.and(boolA, boolB)),
+                                Arguments.of(BoolTerms.or(boolA, boolB)),
+                                Arguments.of(BoolTerms.xor(boolA, boolB)),
+                                Arguments.of(RealTerms.eq(realA, realB)),
+                                Arguments.of(UpperCardinalityTerms.add(upperCardinalityA, upperCardinalityB)),
+                                Arguments.of(UpperCardinalityTerms.mul(upperCardinalityA, upperCardinalityB)),
+                                Arguments.of(UpperCardinalityTerms.min(upperCardinalityA, upperCardinalityB)),
+                                Arguments.of(UpperCardinalityTerms.max(upperCardinalityA, upperCardinalityB))
+                );
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/term/bool/BoolTermsEvaluateTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/bool/BoolTermsEvaluateTest.java
new file mode 100644
index 00000000..beff705e
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/bool/BoolTermsEvaluateTest.java
@@ -0,0 +1,75 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.bool;
+
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.CsvSource;
+import tools.refinery.store.query.valuation.Valuation;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+
+class BoolTermsEvaluateTest {
+        @ParameterizedTest(name = "!{0} == {1}")
+        @CsvSource(value = {
+                        "false, true",
+                        "true, false",
+                        "null, null"
+        }, nullValues = "null")
+        void notTest(Boolean a, Boolean result) {
+                var term = BoolTerms.not(BoolTerms.constant(a));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "{0} && {1} == {2}")
+        @CsvSource(value = {
+                        "false, false, false",
+                        "false, true, false",
+                        "true, false, false",
+                        "true, true, true",
+                        "false, null, null",
+                        "null, false, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void andTest(Boolean a, Boolean b, Boolean result) {
+                var term = BoolTerms.and(BoolTerms.constant(a), BoolTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "{0} || {1} == {2}")
+        @CsvSource(value = {
+                        "false, false, false",
+                        "false, true, true",
+                        "true, false, true",
+                        "true, true, true",
+                        "true, null, null",
+                        "null, true, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void orTest(Boolean a, Boolean b, Boolean result) {
+                var term = BoolTerms.or(BoolTerms.constant(a), BoolTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "{0} ^^ {1} == {2}")
+        @CsvSource(value = {
+                        "false, false, false",
+                        "false, true, true",
+                        "true, false, true",
+                        "true, true, false",
+                        "false, null, null",
+                        "null, false, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void xorTest(Boolean a, Boolean b, Boolean result) {
+                var term = BoolTerms.xor(BoolTerms.constant(a), BoolTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/term/int_/IntTermsEvaluateTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/int_/IntTermsEvaluateTest.java
new file mode 100644
index 00000000..abe50d75
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/int_/IntTermsEvaluateTest.java
@@ -0,0 +1,259 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.int_;
+
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.Arguments;
+import org.junit.jupiter.params.provider.CsvSource;
+import org.junit.jupiter.params.provider.MethodSource;
+import tools.refinery.store.query.term.real.RealTerms;
+import tools.refinery.store.query.valuation.Valuation;
+
+import java.util.stream.Stream;
+
+import static org.hamcrest.Matchers.is;
+import static org.hamcrest.MatcherAssert.assertThat;
+
+class IntTermsEvaluateTest {
+        @ParameterizedTest(name = "+{0} == {1}")
+        @CsvSource(value = {
+                        "2, 2",
+                        "null, null"
+        }, nullValues = "null")
+        void plusTest(Integer a, Integer result) {
+                var term = IntTerms.plus(IntTerms.constant(a));
+                assertThat(term.getType(), is(Integer.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "-{0} == {1}")
+        @CsvSource(value = {
+                        "2, -2",
+                        "null, null"
+        }, nullValues = "null")
+        void minusTest(Integer a, Integer result) {
+                var term = IntTerms.minus(IntTerms.constant(a));
+                assertThat(term.getType(), is(Integer.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "{0} + {1} == {2}")
+        @CsvSource(value = {
+                        "1, 2, 3",
+                        "null, 2, null",
+                        "1, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void addTest(Integer a, Integer b, Integer result) {
+                var term = IntTerms.add(IntTerms.constant(a), IntTerms.constant(b));
+                assertThat(term.getType(), is(Integer.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "{0} - {1} == {2}")
+        @CsvSource(value = {
+                        "1, 3, -2",
+                        "null, 3, null",
+                        "1, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void subTest(Integer a, Integer b, Integer result) {
+                var term = IntTerms.sub(IntTerms.constant(a), IntTerms.constant(b));
+                assertThat(term.getType(), is(Integer.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "{0} * {1} == {2}")
+        @CsvSource(value = {
+                        "2, 3, 6",
+                        "null, 3, null",
+                        "2, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void mulTest(Integer a, Integer b, Integer result) {
+                var term = IntTerms.mul(IntTerms.constant(a), IntTerms.constant(b));
+                assertThat(term.getType(), is(Integer.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "{0} * {1} == {2}")
+        @CsvSource(value = {
+                        "6, 3, 2",
+                        "7, 3, 2",
+                        "6, 0, null",
+                        "null, 3, null",
+                        "6, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void divTest(Integer a, Integer b, Integer result) {
+                var term = IntTerms.div(IntTerms.constant(a), IntTerms.constant(b));
+                assertThat(term.getType(), is(Integer.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "{0} ** {1} == {2}")
+        @CsvSource(value = {
+                        "1, 0, 1",
+                        "1, 3, 1",
+                        "1, -3, null",
+                        "2, 0, 1",
+                        "2, 2, 4",
+                        "2, 3, 8",
+                        "2, 4, 16",
+                        "2, 5, 32",
+                        "2, 6, 64",
+                        "2, -3, null",
+                        "null, 3, null",
+                        "2, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void powTest(Integer a, Integer b, Integer result) {
+                var term = IntTerms.pow(IntTerms.constant(a), IntTerms.constant(b));
+                assertThat(term.getType(), is(Integer.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "min({0}, {1}) == {2}")
+        @CsvSource(value = {
+                        "1, 2, 1",
+                        "2, 1, 1",
+                        "null, 2, null",
+                        "1, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void minTest(Integer a, Integer b, Integer result) {
+                var term = IntTerms.min(IntTerms.constant(a), IntTerms.constant(b));
+                assertThat(term.getType(), is(Integer.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "max({0}, {1}) == {2}")
+        @CsvSource(value = {
+                        "1, 2, 2",
+                        "2, 1, 2",
+                        "null, 2, null",
+                        "1, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void maxTest(Integer a, Integer b, Integer result) {
+                var term = IntTerms.max(IntTerms.constant(a), IntTerms.constant(b));
+                assertThat(term.getType(), is(Integer.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "({0} == {1}) == {2}")
+        @CsvSource(value = {
+                        "1, 1, true",
+                        "1, 2, false",
+                        "null, 1, null",
+                        "1, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void eqTest(Integer a, Integer b, Boolean result) {
+                var term = IntTerms.eq(IntTerms.constant(a), IntTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "({0} != {1}) == {2}")
+        @CsvSource(value = {
+                        "1, 1, false",
+                        "1, 2, true",
+                        "null, 1, null",
+                        "1, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void notEqTest(Integer a, Integer b, Boolean result) {
+                var term = IntTerms.notEq(IntTerms.constant(a), IntTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "({0} < {1}) == {2}")
+        @CsvSource(value = {
+                        "1, -2, false",
+                        "1, 1, false",
+                        "1, 2, true",
+                        "null, 1, null",
+                        "1, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void lessTest(Integer a, Integer b, Boolean result) {
+                var term = IntTerms.less(IntTerms.constant(a), IntTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "({0} <= {1}) == {2}")
+        @CsvSource(value = {
+                        "1, -2, false",
+                        "1, 1, true",
+                        "1, 2, true",
+                        "null, 1, null",
+                        "1, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void lessEqTest(Integer a, Integer b, Boolean result) {
+                var term = IntTerms.lessEq(IntTerms.constant(a), IntTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "({0} > {1}) == {2}")
+        @CsvSource(value = {
+                        "1, -2, true",
+                        "1, 1, false",
+                        "1, 2, false",
+                        "null, 1, null",
+                        "1, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void greaterTest(Integer a, Integer b, Boolean result) {
+                var term = IntTerms.greater(IntTerms.constant(a), IntTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "({0} >= {1}) == {2}")
+        @CsvSource(value = {
+                        "1, -2, true",
+                        "1, 1, true",
+                        "1, 2, false",
+                        "null, 1, null",
+                        "1, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void greaterEqTest(Integer a, Integer b, Boolean result) {
+                var term = IntTerms.greaterEq(IntTerms.constant(a), IntTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "{0} as int == {1}")
+        @MethodSource
+        void asIntTest(Double a, Integer result) {
+                var term = IntTerms.asInt(RealTerms.constant(a));
+                assertThat(term.getType(), is(Integer.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        static Stream<Arguments> asIntTest() {
+                return Stream.of(
+                                Arguments.of(2.0, 2),
+                                Arguments.of(2.1, 2),
+                                Arguments.of(2.9, 2),
+                                Arguments.of(-2.0, -2),
+                                Arguments.of(-2.1, -2),
+                                Arguments.of(-2.9, -2),
+                                Arguments.of(0.0, 0),
+                                Arguments.of(-0.0, 0),
+                                Arguments.of(Double.POSITIVE_INFINITY, Integer.MAX_VALUE),
+                                Arguments.of(Double.NEGATIVE_INFINITY, Integer.MIN_VALUE),
+                                Arguments.of(Double.NaN, null),
+                                Arguments.of(null, null)
+                );
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/term/real/RealTermEvaluateTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/real/RealTermEvaluateTest.java
new file mode 100644
index 00000000..6a8eebf1
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/real/RealTermEvaluateTest.java
@@ -0,0 +1,238 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.real;
+
+import org.hamcrest.Matcher;
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.CsvSource;
+import tools.refinery.store.query.term.int_.IntTerms;
+import tools.refinery.store.query.valuation.Valuation;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.*;
+
+class RealTermEvaluateTest {
+        public static final double TOLERANCE = 1e-6;
+
+        private static Matcher<Double> closeToOrNull(Double expected) {
+                return expected == null ? nullValue(Double.class) : closeTo(expected, TOLERANCE);
+        }
+
+        @ParameterizedTest(name = "+{0} == {1}")
+        @CsvSource(value = {
+                        "2.5, 2.5",
+                        "null, null"
+        }, nullValues = "null")
+        void plusTest(Double a, Double result) {
+                var term = RealTerms.plus(RealTerms.constant(a));
+                assertThat(term.getType(), is(Double.class));
+                assertThat(term.evaluate(Valuation.empty()), closeToOrNull(result));
+        }
+
+        @ParameterizedTest(name = "-{0} == {1}")
+        @CsvSource(value = {
+                        "2.5, -2.5",
+                        "null, null"
+        }, nullValues = "null")
+        void minusTest(Double a, Double result) {
+                var term = RealTerms.minus(RealTerms.constant(a));
+                assertThat(term.getType(), is(Double.class));
+                assertThat(term.evaluate(Valuation.empty()), closeToOrNull(result));
+        }
+
+        @ParameterizedTest(name = "{0} + {1} == {2}")
+        @CsvSource(value = {
+                        "1.2, 2.3, 3.5",
+                        "null, 2.3, null",
+                        "1.2, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void addTest(Double a, Double b, Double result) {
+                var term = RealTerms.add(RealTerms.constant(a), RealTerms.constant(b));
+                assertThat(term.getType(), is(Double.class));
+                assertThat(term.evaluate(Valuation.empty()), closeToOrNull(result));
+        }
+
+        @ParameterizedTest(name = "{0} - {1} == {2}")
+        @CsvSource(value = {
+                        "1.2, 3.4, -2.2",
+                        "null, 3.4, null",
+                        "1.2, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void subTest(Double a, Double b, Double result) {
+                var term = RealTerms.sub(RealTerms.constant(a), RealTerms.constant(b));
+                assertThat(term.getType(), is(Double.class));
+                assertThat(term.evaluate(Valuation.empty()), closeToOrNull(result));
+        }
+
+        @ParameterizedTest(name = "{0} * {1} == {2}")
+        @CsvSource(value = {
+                        "2.3, 3.4, 7.82",
+                        "null, 3.4, null",
+                        "2.3, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void mulTest(Double a, Double b, Double result) {
+                var term = RealTerms.mul(RealTerms.constant(a), RealTerms.constant(b));
+                assertThat(term.getType(), is(Double.class));
+                assertThat(term.evaluate(Valuation.empty()), closeToOrNull(result));
+        }
+
+        @ParameterizedTest(name = "{0} * {1} == {2}")
+        @CsvSource(value = {
+                        "7.82, 3.4, 2.3",
+                        "null, 3.4, null",
+                        "7.82, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void divTest(Double a, Double b, Double result) {
+                var term = RealTerms.div(RealTerms.constant(a), RealTerms.constant(b));
+                assertThat(term.getType(), is(Double.class));
+                assertThat(term.evaluate(Valuation.empty()), closeToOrNull(result));
+        }
+
+        @ParameterizedTest(name = "{0} ** {1} == {2}")
+        @CsvSource(value = {
+                        "2.0, 6.0, 64.0",
+                        "null, 6.0, null",
+                        "2.0, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void powTest(Double a, Double b, Double result) {
+                var term = RealTerms.pow(RealTerms.constant(a), RealTerms.constant(b));
+                assertThat(term.getType(), is(Double.class));
+                assertThat(term.evaluate(Valuation.empty()), closeToOrNull(result));
+        }
+
+        @ParameterizedTest(name = "min({0}, {1}) == {2}")
+        @CsvSource(value = {
+                        "1.5, 2.7, 1.5",
+                        "2.7, 1.5, 1.5",
+                        "null, 2.7, null",
+                        "1.5, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void minTest(Double a, Double b, Double result) {
+                var term = RealTerms.min(RealTerms.constant(a), RealTerms.constant(b));
+                assertThat(term.getType(), is(Double.class));
+                assertThat(term.evaluate(Valuation.empty()), closeToOrNull(result));
+        }
+
+        @ParameterizedTest(name = "max({0}, {1}) == {2}")
+        @CsvSource(value = {
+                        "1.5, 2.7, 2.7",
+                        "2.7, 1.7, 2.7",
+                        "null, 2.7, null",
+                        "1.5, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void maxTest(Double a, Double b, Double result) {
+                var term = RealTerms.max(RealTerms.constant(a), RealTerms.constant(b));
+                assertThat(term.getType(), is(Double.class));
+                assertThat(term.evaluate(Valuation.empty()), closeToOrNull(result));
+        }
+
+        @ParameterizedTest(name = "({0} == {1}) == {2}")
+        @CsvSource(value = {
+                        "1.5, 1.5, true",
+                        "1.5, 2.7, false",
+                        "null, 1.5, null",
+                        "1.5, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void eqTest(Double a, Double b, Boolean result) {
+                var term = RealTerms.eq(RealTerms.constant(a), RealTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "({0} != {1}) == {2}")
+        @CsvSource(value = {
+                        "1.5, 1.5, false",
+                        "1.5, 2.7, true",
+                        "null, 1.5, null",
+                        "1.5, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void notEqTest(Double a, Double b, Boolean result) {
+                var term = RealTerms.notEq(RealTerms.constant(a), RealTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "({0} < {1}) == {2}")
+        @CsvSource(value = {
+                        "1.5, -2.7, false",
+                        "1.5, 1.5, false",
+                        "1.5, 2.7, true",
+                        "null, 1.5, null",
+                        "1.5, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void lessTest(Double a, Double b, Boolean result) {
+                var term = RealTerms.less(RealTerms.constant(a), RealTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "({0} <= {1}) == {2}")
+        @CsvSource(value = {
+                        "1.5, -2.7, false",
+                        "1.5, 1.5, true",
+                        "1.5, 2.7, true",
+                        "null, 1.5, null",
+                        "1.5, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void lessEqTest(Double a, Double b, Boolean result) {
+                var term = RealTerms.lessEq(RealTerms.constant(a), RealTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "({0} > {1}) == {2}")
+        @CsvSource(value = {
+                        "1.5, -2.7, true",
+                        "1.5, 1.5, false",
+                        "1.5, 2.7, false",
+                        "null, 1.5, null",
+                        "1.5, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void greaterTest(Double a, Double b, Boolean result) {
+                var term = RealTerms.greater(RealTerms.constant(a), RealTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "({0} >= {1}) == {2}")
+        @CsvSource(value = {
+                        "1.5, -2.7, true",
+                        "1.5, 1.5, true",
+                        "1.5, 2.7, false",
+                        "null, 1.5, null",
+                        "1.5, null, null",
+                        "null, null, null"
+        }, nullValues = "null")
+        void greaterEqTest(Double a, Double b, Boolean result) {
+                var term = RealTerms.greaterEq(RealTerms.constant(a), RealTerms.constant(b));
+                assertThat(term.getType(), is(Boolean.class));
+                assertThat(term.evaluate(Valuation.empty()), is(result));
+        }
+
+        @ParameterizedTest(name = "{0} as real == {1}")
+        @CsvSource(value = {
+                        "0, 0.0",
+                        "5, 5.0",
+                        "null, null"
+        }, nullValues = "null")
+        void asRealTest(Integer a, Double result) {
+                var term = RealTerms.asReal(IntTerms.constant(a));
+                assertThat(term.getType(), is(Double.class));
+                assertThat(term.evaluate(Valuation.empty()), closeToOrNull(result));
+        }
+}
diff --git a/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/internal/cardinality/UpperCardinalitySumAggregationOperatorStreamTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregatorStreamTest.java
index 53d03cbd..31baf36e 100644
--- a/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/internal/cardinality/UpperCardinalitySumAggregationOperatorStreamTest.java
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregatorStreamTest.java
@@ -3,7 +3,7 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.query.viatra.internal.cardinality;
+package tools.refinery.store.query.term.uppercardinality;
 
 import org.junit.jupiter.params.ParameterizedTest;
 import org.junit.jupiter.params.provider.Arguments;
@@ -15,14 +15,14 @@ import java.util.List;
 import java.util.stream.Stream;
 
 import static org.hamcrest.MatcherAssert.assertThat;
-import static org.hamcrest.Matchers.equalTo;
+import static org.hamcrest.Matchers.is;
 
-class UpperCardinalitySumAggregationOperatorStreamTest {
+class UpperCardinalitySumAggregatorStreamTest {
         @ParameterizedTest
         @MethodSource
         void testStream(List<UpperCardinality> list, UpperCardinality expected) {
-                var result = UpperCardinalitySumAggregationOperator.INSTANCE.aggregateStream(list.stream());
-                assertThat(result, equalTo(expected));
+                var result = UpperCardinalitySumAggregator.INSTANCE.aggregateStream(list.stream());
+                assertThat(result, is(expected));
         }
 
         static Stream<Arguments> testStream() {
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregatorTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregatorTest.java
new file mode 100644
index 00000000..780cd0ab
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalitySumAggregatorTest.java
@@ -0,0 +1,80 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.uppercardinality;
+
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.query.term.StatefulAggregate;
+import tools.refinery.store.representation.cardinality.UpperCardinalities;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+
+class UpperCardinalitySumAggregatorTest {
+        private StatefulAggregate<UpperCardinality, UpperCardinality> accumulator;
+
+        @BeforeEach
+        void beforeEach() {
+                accumulator = UpperCardinalitySumAggregator.INSTANCE.createEmptyAggregate();
+        }
+
+        @Test
+        void emptyAggregationTest() {
+                assertThat(accumulator.getResult(), is(UpperCardinality.of(0)));
+        }
+
+        @Test
+        void singleBoundedTest() {
+                accumulator.add(UpperCardinality.of(3));
+                assertThat(accumulator.getResult(), is(UpperCardinality.of(3)));
+        }
+
+        @Test
+        void multipleBoundedTest() {
+                accumulator.add(UpperCardinality.of(2));
+                accumulator.add(UpperCardinality.of(3));
+                assertThat(accumulator.getResult(), is(UpperCardinality.of(5)));
+        }
+
+        @Test
+        void singleUnboundedTest() {
+                accumulator.add(UpperCardinalities.UNBOUNDED);
+                assertThat(accumulator.getResult(), is(UpperCardinalities.UNBOUNDED));
+        }
+
+        @Test
+        void multipleUnboundedTest() {
+                accumulator.add(UpperCardinalities.UNBOUNDED);
+                accumulator.add(UpperCardinalities.UNBOUNDED);
+                assertThat(accumulator.getResult(), is(UpperCardinalities.UNBOUNDED));
+        }
+
+        @Test
+        void removeBoundedTest() {
+                accumulator.add(UpperCardinality.of(2));
+                accumulator.add(UpperCardinality.of(3));
+                accumulator.remove(UpperCardinality.of(2));
+                assertThat(accumulator.getResult(), is(UpperCardinality.of(3)));
+        }
+
+        @Test
+        void removeAllUnboundedTest() {
+                accumulator.add(UpperCardinalities.UNBOUNDED);
+                accumulator.add(UpperCardinality.of(3));
+                accumulator.remove(UpperCardinalities.UNBOUNDED);
+                assertThat(accumulator.getResult(), is(UpperCardinality.of(3)));
+        }
+
+        @Test
+        void removeSomeUnboundedTest() {
+                accumulator.add(UpperCardinalities.UNBOUNDED);
+                accumulator.add(UpperCardinalities.UNBOUNDED);
+                accumulator.add(UpperCardinality.of(3));
+                accumulator.remove(UpperCardinalities.UNBOUNDED);
+                assertThat(accumulator.getResult(), is(UpperCardinalities.UNBOUNDED));
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityTermsEvaluateTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityTermsEvaluateTest.java
new file mode 100644
index 00000000..9d0f3bde
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/term/uppercardinality/UpperCardinalityTermsEvaluateTest.java
@@ -0,0 +1,104 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term.uppercardinality;
+
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.Arguments;
+import org.junit.jupiter.params.provider.MethodSource;
+import tools.refinery.store.query.valuation.Valuation;
+import tools.refinery.store.representation.cardinality.UpperCardinalities;
+import tools.refinery.store.representation.cardinality.UpperCardinality;
+
+import java.util.stream.Stream;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+
+class UpperCardinalityTermsEvaluateTest {
+        @ParameterizedTest(name = "min({0}, {1}) == {2}")
+        @MethodSource
+        void minTest(UpperCardinality a, UpperCardinality b, UpperCardinality expected) {
+                var term = UpperCardinalityTerms.min(UpperCardinalityTerms.constant(a), UpperCardinalityTerms.constant(b));
+                assertThat(term.getType(), is(UpperCardinality.class));
+                assertThat(term.evaluate(Valuation.empty()), is(expected));
+        }
+
+        static Stream<Arguments> minTest() {
+                return Stream.of(
+                                Arguments.of(UpperCardinality.of(0), UpperCardinality.of(0), UpperCardinality.of(0)),
+                                Arguments.of(UpperCardinality.of(0), UpperCardinality.of(1), UpperCardinality.of(0)),
+                                Arguments.of(UpperCardinality.of(1), UpperCardinality.of(0), UpperCardinality.of(0)),
+                                Arguments.of(UpperCardinality.of(0), UpperCardinalities.UNBOUNDED, UpperCardinality.of(0)),
+                                Arguments.of(UpperCardinalities.UNBOUNDED, UpperCardinality.of(0), UpperCardinality.of(0)),
+                                Arguments.of(UpperCardinalities.UNBOUNDED, UpperCardinalities.UNBOUNDED, UpperCardinalities.UNBOUNDED),
+                                Arguments.of(UpperCardinality.of(1), null, null),
+                                Arguments.of(null, UpperCardinality.of(1), null),
+                                Arguments.of(null, null, null)
+                );
+        }
+
+        @ParameterizedTest(name = "max({0}, {1}) == {2}")
+        @MethodSource
+        void maxTest(UpperCardinality a, UpperCardinality b, UpperCardinality expected) {
+                var term = UpperCardinalityTerms.max(UpperCardinalityTerms.constant(a), UpperCardinalityTerms.constant(b));
+                assertThat(term.getType(), is(UpperCardinality.class));
+                assertThat(term.evaluate(Valuation.empty()), is(expected));
+        }
+
+        static Stream<Arguments> maxTest() {
+                return Stream.of(
+                                Arguments.of(UpperCardinality.of(0), UpperCardinality.of(0), UpperCardinality.of(0)),
+                                Arguments.of(UpperCardinality.of(0), UpperCardinality.of(1), UpperCardinality.of(1)),
+                                Arguments.of(UpperCardinality.of(1), UpperCardinality.of(0), UpperCardinality.of(1)),
+                                Arguments.of(UpperCardinality.of(0), UpperCardinalities.UNBOUNDED, UpperCardinalities.UNBOUNDED),
+                                Arguments.of(UpperCardinalities.UNBOUNDED, UpperCardinality.of(0), UpperCardinalities.UNBOUNDED),
+                                Arguments.of(UpperCardinalities.UNBOUNDED, UpperCardinalities.UNBOUNDED, UpperCardinalities.UNBOUNDED),
+                                Arguments.of(UpperCardinality.of(1), null, null),
+                                Arguments.of(null, UpperCardinality.of(1), null),
+                                Arguments.of(null, null, null)
+                );
+        }
+
+        @ParameterizedTest(name = "{0} + {1} == {2}")
+        @MethodSource
+        void addTest(UpperCardinality a, UpperCardinality b, UpperCardinality expected) {
+                var term = UpperCardinalityTerms.add(UpperCardinalityTerms.constant(a), UpperCardinalityTerms.constant(b));
+                assertThat(term.getType(), is(UpperCardinality.class));
+                assertThat(term.evaluate(Valuation.empty()), is(expected));
+        }
+
+        static Stream<Arguments> addTest() {
+                return Stream.of(
+                                Arguments.of(UpperCardinality.of(2), UpperCardinality.of(3), UpperCardinality.of(5)),
+                                Arguments.of(UpperCardinality.of(2), UpperCardinalities.UNBOUNDED, UpperCardinalities.UNBOUNDED),
+                                Arguments.of(UpperCardinalities.UNBOUNDED, UpperCardinality.of(2), UpperCardinalities.UNBOUNDED),
+                                Arguments.of(UpperCardinalities.UNBOUNDED, UpperCardinalities.UNBOUNDED, UpperCardinalities.UNBOUNDED),
+                                Arguments.of(UpperCardinality.of(1), null, null),
+                                Arguments.of(null, UpperCardinality.of(1), null),
+                                Arguments.of(null, null, null)
+                );
+        }
+
+        @ParameterizedTest(name = "{0} * {1} == {2}")
+        @MethodSource
+        void mulTest(UpperCardinality a, UpperCardinality b, UpperCardinality expected) {
+                var term = UpperCardinalityTerms.mul(UpperCardinalityTerms.constant(a), UpperCardinalityTerms.constant(b));
+                assertThat(term.getType(), is(UpperCardinality.class));
+                assertThat(term.evaluate(Valuation.empty()), is(expected));
+        }
+
+        static Stream<Arguments> mulTest() {
+                return Stream.of(
+                                Arguments.of(UpperCardinality.of(2), UpperCardinality.of(3), UpperCardinality.of(6)),
+                                Arguments.of(UpperCardinality.of(2), UpperCardinalities.UNBOUNDED, UpperCardinalities.UNBOUNDED),
+                                Arguments.of(UpperCardinalities.UNBOUNDED, UpperCardinality.of(2), UpperCardinalities.UNBOUNDED),
+                                Arguments.of(UpperCardinalities.UNBOUNDED, UpperCardinalities.UNBOUNDED, UpperCardinalities.UNBOUNDED),
+                                Arguments.of(UpperCardinality.of(1), null, null),
+                                Arguments.of(null, UpperCardinality.of(1), null),
+                                Arguments.of(null, null, null)
+                );
+        }
+}
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java
index dd7a018d..d6a9e02c 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/translator/Advice.java
@@ -5,11 +5,11 @@
  */
 package tools.refinery.store.reasoning.translator;
 
+import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.reasoning.representation.AnyPartialSymbol;
 import tools.refinery.store.reasoning.representation.PartialRelation;
 import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.query.literal.Literal;
-import tools.refinery.store.query.substitution.Substitutions;
 
 import java.util.*;
 
@@ -66,14 +66,9 @@ public final class Advice {
         public List<Literal> substitute(List<Variable> substituteParameters) {
                 checkArity(substituteParameters);
                 markProcessed();
-                int arity = parameters.size();
-                var variableMap = new HashMap<Variable, Variable>(arity);
-                for (int i = 0; i < arity; i++) {
-                        variableMap.put(parameters.get(i), substituteParameters.get(i));
-                }
                 // Use a renewing substitution to remove any non-parameter variables and avoid clashed between variables
                 // coming from different advice in the same clause.
-                var substitution = Substitutions.renewing(variableMap);
+                var substitution = Substitution.builder().putManyChecked(parameters, substituteParameters).renewing().build();
                 return literals.stream().map(literal -> literal.substitute(substitution)).toList();
         }