feat: query parameter binding validation

* Introduce parameter directions for constraints and DNF
* Introduce variable directions for literals
* Infer and check variable directions in DNF and topologically sort literals by
  their input variables

49 files changed, 1595 insertions, 446 deletions

diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/context/RelationalQueryMetaContext.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/context/RelationalQueryMetaContext.java
index cf96b7fd..211eacb4 100644
--- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/context/RelationalQueryMetaContext.java
+++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/context/RelationalQueryMetaContext.java
@@ -9,7 +9,6 @@ import org.eclipse.viatra.query.runtime.matchers.context.AbstractQueryMetaContex
 import org.eclipse.viatra.query.runtime.matchers.context.IInputKey;
 import org.eclipse.viatra.query.runtime.matchers.context.InputKeyImplication;
 import org.eclipse.viatra.query.runtime.matchers.context.common.JavaTransitiveInstancesKey;
-import tools.refinery.store.query.term.DataSort;
 import tools.refinery.store.query.viatra.internal.pquery.SymbolViewWrapper;
 import tools.refinery.store.query.view.AnySymbolView;
 
@@ -62,14 +61,14 @@ public class RelationalQueryMetaContext extends AbstractQueryMetaContext {
                                                 relationViewImplication.impliedIndices()));
                         }
                 }
-                var sorts = symbolView.getSorts();
+                var parameters = symbolView.getParameters();
                 int arity = symbolView.arity();
                 for (int i = 0; i < arity; i++) {
-                        var sort = sorts.get(i);
-                        if (sort instanceof DataSort<?> dataSort) {
-                                var javaTransitiveInstancesKey = new JavaTransitiveInstancesKey(dataSort.type());
-                                var javaImplication = new InputKeyImplication(implyingKey, javaTransitiveInstancesKey,
-                                                List.of(i));
+                        var parameter = parameters.get(i);
+                        var parameterType = parameter.tryGetType();
+                        if (parameterType.isPresent()) {
+                                var javaTransitiveInstancesKey = new JavaTransitiveInstancesKey(parameterType.get());
+                                var javaImplication = new InputKeyImplication(implyingKey, javaTransitiveInstancesKey, List.of(i));
                                 inputKeyImplications.add(javaImplication);
                         }
                 }
diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/Dnf2PQuery.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/Dnf2PQuery.java
index b511a5c7..ec880435 100644
--- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/Dnf2PQuery.java
+++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/Dnf2PQuery.java
@@ -19,11 +19,13 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.Consta
 import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.PositivePatternCall;
 import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeConstraint;
 import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter;
+import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameterDirection;
 import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery;
 import org.eclipse.viatra.query.runtime.matchers.tuple.Tuple;
 import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples;
 import tools.refinery.store.query.dnf.Dnf;
 import tools.refinery.store.query.dnf.DnfClause;
+import tools.refinery.store.query.dnf.SymbolicParameter;
 import tools.refinery.store.query.literal.*;
 import tools.refinery.store.query.term.ConstantTerm;
 import tools.refinery.store.query.term.StatefulAggregator;
@@ -82,15 +84,20 @@ public class Dnf2PQuery {
                 var pQuery = new RawPQuery(dnfQuery.getUniqueName());
                 pQuery.setEvaluationHints(consumeHint(dnfQuery));
 
-                Map<Variable, PParameter> parameters = new HashMap<>();
-                for (Variable variable : dnfQuery.getParameters()) {
-                        parameters.put(variable, new PParameter(variable.getUniqueName()));
-                }
-
+                Map<SymbolicParameter, PParameter> parameters = new HashMap<>();
                 List<PParameter> parameterList = new ArrayList<>();
-                for (var param : dnfQuery.getParameters()) {
-                        parameterList.add(parameters.get(param));
+                for (var parameter : dnfQuery.getSymbolicParameters()) {
+                        var direction = switch (parameter.getDirection()) {
+                                case IN_OUT -> PParameterDirection.INOUT;
+                                case OUT -> PParameterDirection.OUT;
+                                case IN -> throw new IllegalArgumentException("Query %s with input parameter %s is not supported"
+                                                .formatted(dnfQuery, parameter.getVariable()));
+                        };
+                        var pParameter = new PParameter(parameter.getVariable().getUniqueName(), null, null, direction);
+                        parameters.put(parameter, pParameter);
+                        parameterList.add(pParameter);
                 }
+
                 pQuery.setParameters(parameterList);
 
                 for (var functionalDependency : dnfQuery.getFunctionalDependencies()) {
@@ -110,15 +117,15 @@ public class Dnf2PQuery {
                 synchronized (P_CONSTRAINT_LOCK) {
                         for (DnfClause clause : dnfQuery.getClauses()) {
                                 PBody body = new PBody(pQuery);
-                                List<ExportedParameter> symbolicParameters = new ArrayList<>();
-                                for (var param : dnfQuery.getParameters()) {
-                                        PVariable pVar = body.getOrCreateVariableByName(param.getUniqueName());
-                                        symbolicParameters.add(new ExportedParameter(body, pVar, parameters.get(param)));
+                                List<ExportedParameter> parameterExports = new ArrayList<>();
+                                for (var parameter : dnfQuery.getSymbolicParameters()) {
+                                        PVariable pVar = body.getOrCreateVariableByName(parameter.getVariable().getUniqueName());
+                                        parameterExports.add(new ExportedParameter(body, pVar, parameters.get(parameter)));
                                 }
-                                body.setSymbolicParameters(symbolicParameters);
+                                body.setSymbolicParameters(parameterExports);
                                 pQuery.addBody(body);
                                 for (Literal literal : clause.literals()) {
-                                        translateLiteral(literal, clause, body);
+                                        translateLiteral(literal, body);
                                 }
                         }
                 }
@@ -126,11 +133,11 @@ public class Dnf2PQuery {
                 return pQuery;
         }
 
-        private void translateLiteral(Literal literal, DnfClause clause, PBody body) {
+        private void translateLiteral(Literal literal, PBody body) {
                 if (literal instanceof EquivalenceLiteral equivalenceLiteral) {
                         translateEquivalenceLiteral(equivalenceLiteral, body);
                 } else if (literal instanceof CallLiteral callLiteral) {
-                        translateCallLiteral(callLiteral, clause, body);
+                        translateCallLiteral(callLiteral, body);
                 } else if (literal instanceof ConstantLiteral constantLiteral) {
                         translateConstantLiteral(constantLiteral, body);
                 } else if (literal instanceof AssignLiteral<?> assignLiteral) {
@@ -138,25 +145,25 @@ public class Dnf2PQuery {
                 } else if (literal instanceof AssumeLiteral assumeLiteral) {
                         translateAssumeLiteral(assumeLiteral, body);
                 } else if (literal instanceof CountLiteral countLiteral) {
-                        translateCountLiteral(countLiteral, clause, body);
+                        translateCountLiteral(countLiteral, body);
                 } else if (literal instanceof AggregationLiteral<?, ?> aggregationLiteral) {
-                        translateAggregationLiteral(aggregationLiteral, clause, body);
+                        translateAggregationLiteral(aggregationLiteral, body);
                 } else {
                         throw new IllegalArgumentException("Unknown literal: " + literal.toString());
                 }
         }
 
         private void translateEquivalenceLiteral(EquivalenceLiteral equivalenceLiteral, PBody body) {
-                PVariable varSource = body.getOrCreateVariableByName(equivalenceLiteral.left().getUniqueName());
-                PVariable varTarget = body.getOrCreateVariableByName(equivalenceLiteral.right().getUniqueName());
-                if (equivalenceLiteral.positive()) {
+                PVariable varSource = body.getOrCreateVariableByName(equivalenceLiteral.getLeft().getUniqueName());
+                PVariable varTarget = body.getOrCreateVariableByName(equivalenceLiteral.getRight().getUniqueName());
+                if (equivalenceLiteral.isPositive()) {
                         new Equality(body, varSource, varTarget);
                 } else {
                         new Inequality(body, varSource, varTarget);
                 }
         }
 
-        private void translateCallLiteral(CallLiteral callLiteral, DnfClause clause, PBody body) {
+        private void translateCallLiteral(CallLiteral callLiteral, PBody body) {
                 var polarity = callLiteral.getPolarity();
                 switch (polarity) {
                 case POSITIVE -> {
@@ -186,7 +193,7 @@ public class Dnf2PQuery {
                         new BinaryTransitiveClosure(body, substitution, pattern);
                 }
                 case NEGATIVE -> {
-                        var wrappedCall = wrapperFactory.maybeWrapConstraint(callLiteral, clause);
+                        var wrappedCall = wrapperFactory.maybeWrapConstraint(callLiteral);
                         var substitution = translateSubstitution(wrappedCall.remappedArguments(), body);
                         var pattern = wrappedCall.pattern();
                         new NegativePatternCall(body, substitution, pattern);
@@ -206,13 +213,13 @@ public class Dnf2PQuery {
         }
 
         private void translateConstantLiteral(ConstantLiteral constantLiteral, PBody body) {
-                var variable = body.getOrCreateVariableByName(constantLiteral.variable().getUniqueName());
-                new ConstantValue(body, variable, constantLiteral.nodeId());
+                var variable = body.getOrCreateVariableByName(constantLiteral.getVariable().getUniqueName());
+                new ConstantValue(body, variable, constantLiteral.getNodeId());
         }
 
         private <T> void translateAssignLiteral(AssignLiteral<T> assignLiteral, PBody body) {
-                var variable = body.getOrCreateVariableByName(assignLiteral.variable().getUniqueName());
-                var term = assignLiteral.term();
+                var variable = body.getOrCreateVariableByName(assignLiteral.getTargetVariable().getUniqueName());
+                var term = assignLiteral.getTerm();
                 if (term instanceof ConstantTerm<T> constantTerm) {
                         new ConstantValue(body, variable, constantTerm.getValue());
                 } else {
@@ -222,19 +229,18 @@ public class Dnf2PQuery {
         }
 
         private void translateAssumeLiteral(AssumeLiteral assumeLiteral, PBody body) {
-                var evaluator = new AssumptionEvaluator(assumeLiteral.term());
+                var evaluator = new AssumptionEvaluator(assumeLiteral.getTerm());
                 new ExpressionEvaluation(body, evaluator, null);
         }
 
-        private void translateCountLiteral(CountLiteral countLiteral, DnfClause clause, PBody body) {
-                var wrappedCall = wrapperFactory.maybeWrapConstraint(countLiteral, clause);
+        private void translateCountLiteral(CountLiteral countLiteral, PBody body) {
+                var wrappedCall = wrapperFactory.maybeWrapConstraint(countLiteral);
                 var substitution = translateSubstitution(wrappedCall.remappedArguments(), body);
                 var resultVariable = body.getOrCreateVariableByName(countLiteral.getResultVariable().getUniqueName());
                 new PatternMatchCounter(body, substitution, wrappedCall.pattern(), resultVariable);
         }
 
-        private <R, T> void translateAggregationLiteral(AggregationLiteral<R, T> aggregationLiteral, DnfClause clause,
-                                                                                                        PBody body) {
+        private <R, T> void translateAggregationLiteral(AggregationLiteral<R, T> aggregationLiteral, PBody body) {
                 var aggregator = aggregationLiteral.getAggregator();
                 IMultisetAggregationOperator<T, ?, R> aggregationOperator;
                 if (aggregator instanceof StatelessAggregator<R, T> statelessAggregator) {
@@ -244,7 +250,7 @@ public class Dnf2PQuery {
                 } else {
                         throw new IllegalArgumentException("Unknown aggregator: " + aggregator);
                 }
-                var wrappedCall = wrapperFactory.maybeWrapConstraint(aggregationLiteral, clause);
+                var wrappedCall = wrapperFactory.maybeWrapConstraint(aggregationLiteral);
                 var substitution = translateSubstitution(wrappedCall.remappedArguments(), body);
                 var inputVariable = body.getOrCreateVariableByName(aggregationLiteral.getInputVariable().getUniqueName());
                 var aggregatedColumn = substitution.invertIndex().get(inputVariable);
diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/QueryWrapperFactory.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/QueryWrapperFactory.java
index 0d046455..2b7280f2 100644
--- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/QueryWrapperFactory.java
+++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/pquery/QueryWrapperFactory.java
@@ -14,12 +14,13 @@ import org.eclipse.viatra.query.runtime.matchers.psystem.basicenumerables.TypeCo
 import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PParameter;
 import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PQuery;
 import org.eclipse.viatra.query.runtime.matchers.psystem.queries.PVisibility;
+import org.eclipse.viatra.query.runtime.matchers.tuple.Tuple;
 import org.eclipse.viatra.query.runtime.matchers.tuple.Tuples;
 import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.dnf.Dnf;
-import tools.refinery.store.query.dnf.DnfClause;
 import tools.refinery.store.query.dnf.DnfUtils;
 import tools.refinery.store.query.literal.AbstractCallLiteral;
+import tools.refinery.store.query.term.ParameterDirection;
 import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.query.view.AnySymbolView;
 import tools.refinery.store.query.view.SymbolView;
@@ -45,21 +46,17 @@ class QueryWrapperFactory {
                 }
                 return maybeWrapConstraint(symbolView, identity);
         }
-        public WrappedCall maybeWrapConstraint(AbstractCallLiteral callLiteral, DnfClause clause) {
+
+        public WrappedCall maybeWrapConstraint(AbstractCallLiteral callLiteral) {
                 var arguments = callLiteral.getArguments();
                 int arity = arguments.size();
                 var remappedParameters = new int[arity];
-                var boundVariables = clause.boundVariables();
                 var unboundVariableIndices = new HashMap<Variable, Integer>();
                 var appendVariable = new VariableAppender();
                 for (int i = 0; i < arity; i++) {
                         var variable = arguments.get(i);
-                        if (boundVariables.contains(variable)) {
-                                // Do not join bound variable to make sure that the embedded pattern stays as general as possible.
-                                remappedParameters[i] = appendVariable.applyAsInt(variable);
-                        } else {
-                                remappedParameters[i] = unboundVariableIndices.computeIfAbsent(variable, appendVariable::applyAsInt);
-                        }
+                        // Unify all variables to avoid VIATRA bugs, even if they're bound in the containing clause.
+                        remappedParameters[i] = unboundVariableIndices.computeIfAbsent(variable, appendVariable::applyAsInt);
                 }
                 var pattern = maybeWrapConstraint(callLiteral.getTarget(), remappedParameters);
                 return new WrappedCall(pattern, appendVariable.getRemappedArguments());
@@ -89,6 +86,8 @@ class QueryWrapperFactory {
                 var constraint = remappedConstraint.constraint();
                 var remappedParameters = remappedConstraint.remappedParameters();
 
+                checkNoInputParameters(constraint);
+
                 var embeddedPQuery = new RawPQuery(DnfUtils.generateUniqueName(constraint.name()), PVisibility.EMBEDDED);
                 var body = new PBody(embeddedPQuery);
                 int arity = Arrays.stream(remappedParameters).max().orElse(-1) + 1;
@@ -112,6 +111,21 @@ class QueryWrapperFactory {
                 }
                 var argumentTuple = Tuples.flatTupleOf(arguments);
 
+                addPositiveConstraint(constraint, body, argumentTuple);
+                embeddedPQuery.addBody(body);
+                return embeddedPQuery;
+        }
+
+        private static void checkNoInputParameters(Constraint constraint) {
+                for (var constraintParameter : constraint.getParameters()) {
+                        if (constraintParameter.getDirection() == ParameterDirection.IN) {
+                                throw new IllegalArgumentException("Input parameter %s of %s is not supported"
+                                                .formatted(constraintParameter, constraint));
+                        }
+                }
+        }
+
+        private void addPositiveConstraint(Constraint constraint, PBody body, Tuple argumentTuple) {
                 if (constraint instanceof SymbolView<?> view) {
                         new TypeConstraint(body, argumentTuple, getInputKey(view));
                 } else if (constraint instanceof Dnf dnf) {
@@ -120,9 +134,6 @@ class QueryWrapperFactory {
                 } else {
                         throw new IllegalArgumentException("Unknown Constraint: " + constraint);
                 }
-
-                embeddedPQuery.addBody(body);
-                return embeddedPQuery;
         }
 
         public IInputKey getInputKey(AnySymbolView symbolView) {
diff --git a/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/DiagonalQueryTest.java b/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/DiagonalQueryTest.java
index 56ddb9b4..86a27f5b 100644
--- a/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/DiagonalQueryTest.java
+++ b/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/DiagonalQueryTest.java
@@ -298,10 +298,10 @@ class DiagonalQueryTest {
                                         y.assign(x)
                         );
                 });
-                var query = Query.of("Diagonal", Integer.class, (builder, p1, output) -> builder.clause(Integer.class,
-                                (p2, y) -> List.of(
+                var query = Query.of("Diagonal", Integer.class, (builder, p1, output) -> builder.clause(
+                                Integer.class, Integer.class, (p2, y, z) -> List.of(
                                                 personView.call(p1),
-                                                output.assign(subQuery.aggregate(y, INT_SUM, p1, p1, p2, p2, y, y))
+                                                output.assign(subQuery.aggregate(y, INT_SUM, p1, p1, p2, p2, y, z))
                                 )));
 
                 var store = ModelStore.builder()
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java
index 10d8a579..207c627c 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Constraint.java
@@ -14,10 +14,10 @@ import java.util.List;
 public interface Constraint {
         String name();
 
-        List<Sort> getSorts();
+        List<Parameter> getParameters();
 
         default int arity() {
-                return getSorts().size();
+                return getParameters().size();
         }
 
         default boolean invalidIndex(int i) {
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/AbstractQueryBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/AbstractQueryBuilder.java
index ddd69b9f..2a3e3ce0 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/AbstractQueryBuilder.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/AbstractQueryBuilder.java
@@ -8,6 +8,7 @@ package tools.refinery.store.query.dnf;
 import tools.refinery.store.query.dnf.callback.*;
 import tools.refinery.store.query.literal.Literal;
 import tools.refinery.store.query.term.NodeVariable;
+import tools.refinery.store.query.term.ParameterDirection;
 import tools.refinery.store.query.term.Variable;
 
 import java.util.Collection;
@@ -31,11 +32,24 @@ public abstract class AbstractQueryBuilder<T extends AbstractQueryBuilder<T>> {
                 return dnfBuilder.parameter(name);
         }
 
+        public NodeVariable parameter(ParameterDirection direction) {
+                return dnfBuilder.parameter(direction);
+        }
+
+        public NodeVariable parameter(String name, ParameterDirection direction) {
+                return dnfBuilder.parameter(name, direction);
+        }
+
         public T parameter(NodeVariable variable) {
                 dnfBuilder.parameter(variable);
                 return self();
         }
 
+        public T parameter(NodeVariable variable, ParameterDirection direction) {
+                dnfBuilder.parameter(variable, direction);
+                return self();
+        }
+
         public T parameters(NodeVariable... variables) {
                 dnfBuilder.parameters(variables);
                 return self();
@@ -46,6 +60,16 @@ public abstract class AbstractQueryBuilder<T extends AbstractQueryBuilder<T>> {
                 return self();
         }
 
+        public T parameters(List<NodeVariable> variables, ParameterDirection direction) {
+                dnfBuilder.parameters(variables, direction);
+                return self();
+        }
+
+        public T symbolicParameters(List<SymbolicParameter> parameters) {
+                dnfBuilder.symbolicParameters(parameters);
+                return self();
+        }
+
         public T functionalDependencies(Collection<FunctionalDependency<Variable>> functionalDependencies) {
                 dnfBuilder.functionalDependencies(functionalDependencies);
                 return self();
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java
new file mode 100644
index 00000000..7a56145c
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/ClausePostProcessor.java
@@ -0,0 +1,321 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.dnf;
+
+import org.jetbrains.annotations.NotNull;
+import tools.refinery.store.query.literal.EquivalenceLiteral;
+import tools.refinery.store.query.literal.Literal;
+import tools.refinery.store.query.literal.VariableDirection;
+import tools.refinery.store.query.substitution.MapBasedSubstitution;
+import tools.refinery.store.query.substitution.StatelessSubstitution;
+import tools.refinery.store.query.term.NodeVariable;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.*;
+import java.util.function.Function;
+import java.util.stream.Collectors;
+
+class ClausePostProcessor {
+        private final Set<Variable> parameters;
+        private final Map<Variable, Integer> parameterWeights;
+        private final List<Literal> literals;
+        private final Map<NodeVariable, NodeVariable> representatives = new LinkedHashMap<>();
+        private final Map<NodeVariable, Set<NodeVariable>> equivalencePartition = new HashMap<>();
+        private List<Literal> substitutedLiterals;
+        private final Set<Variable> existentiallyQuantifiedVariables = new LinkedHashSet<>();
+        private Set<Variable> inputParameters;
+        private Set<Variable> positiveVariables;
+        private Map<Variable, Set<SortableLiteral>> variableToLiteralInputMap;
+        private PriorityQueue<SortableLiteral> literalsWithAllInputsBound;
+        private LinkedHashSet<Literal> topologicallySortedLiterals;
+
+        public ClausePostProcessor(Set<Variable> parameters, Map<Variable, Integer> parameterWeights,
+                                                           List<Literal> literals) {
+                this.parameters = parameters;
+                this.parameterWeights = parameterWeights;
+                this.literals = literals;
+        }
+
+        public Result postProcessClause() {
+                mergeEquivalentNodeVariables();
+                substitutedLiterals = new ArrayList<>(literals.size());
+                keepParameterEquivalences();
+                substituteLiterals();
+                computePositiveVariables();
+                validatePositiveRepresentatives();
+                validateClosureVariables();
+                topologicallySortLiterals();
+                var filteredLiterals = new ArrayList<Literal>(topologicallySortedLiterals.size());
+                for (var literal : topologicallySortedLiterals) {
+                        var reduction = literal.getReduction();
+                        switch (reduction) {
+                        case NOT_REDUCIBLE -> filteredLiterals.add(literal);
+                        case ALWAYS_TRUE -> {
+                                // Literals reducible to {@code true} can be omitted, because the model is always assumed to have at
+                                // least on object.
+                        }
+                        case ALWAYS_FALSE -> {
+                                // Clauses with {@code false} literals can be omitted entirely.
+                                return ConstantResult.ALWAYS_FALSE;
+                        }
+                        default -> throw new IllegalArgumentException("Invalid reduction: " + reduction);
+                        }
+                }
+                if (filteredLiterals.isEmpty()) {
+                        return ConstantResult.ALWAYS_TRUE;
+                }
+                var clause = new DnfClause(Collections.unmodifiableSet(positiveVariables),
+                                Collections.unmodifiableList(filteredLiterals));
+                return new ClauseResult(clause);
+        }
+
+        private void mergeEquivalentNodeVariables() {
+                for (var literal : literals) {
+                        if (isPositiveEquivalence(literal)) {
+                                var equivalenceLiteral = (EquivalenceLiteral) literal;
+                                mergeVariables(equivalenceLiteral.getLeft(), equivalenceLiteral.getRight());
+                        }
+                }
+        }
+
+        private static boolean isPositiveEquivalence(Literal literal) {
+                return literal instanceof EquivalenceLiteral equivalenceLiteral && equivalenceLiteral.isPositive();
+        }
+
+        private void mergeVariables(NodeVariable left, NodeVariable right) {
+                var leftRepresentative = getRepresentative(left);
+                var rightRepresentative = getRepresentative(right);
+                if (parameters.contains(leftRepresentative) && (!parameters.contains(rightRepresentative) ||
+                                parameterWeights.get(leftRepresentative).compareTo(parameterWeights.get(rightRepresentative)) <= 0)) {
+                        // Prefer the variable occurring earlier in the parameter list as a representative.
+                        doMergeVariables(leftRepresentative, rightRepresentative);
+                } else {
+                        doMergeVariables(rightRepresentative, leftRepresentative);
+                }
+        }
+
+        private void doMergeVariables(NodeVariable parentRepresentative, NodeVariable newChildRepresentative) {
+                var parentSet = getEquivalentVariables(parentRepresentative);
+                var childSet = getEquivalentVariables(newChildRepresentative);
+                parentSet.addAll(childSet);
+                equivalencePartition.remove(newChildRepresentative);
+                for (var childEquivalentNodeVariable : childSet) {
+                        representatives.put(childEquivalentNodeVariable, parentRepresentative);
+                }
+        }
+
+        private NodeVariable getRepresentative(NodeVariable variable) {
+                return representatives.computeIfAbsent(variable, Function.identity());
+        }
+
+        private Set<NodeVariable> getEquivalentVariables(NodeVariable variable) {
+                var representative = getRepresentative(variable);
+                if (!representative.equals(variable)) {
+                        throw new IllegalStateException("NodeVariable %s already has a representative %s"
+                                        .formatted(variable, representative));
+                }
+                return equivalencePartition.computeIfAbsent(variable, key -> {
+                        var set = new HashSet<NodeVariable>(1);
+                        set.add(key);
+                        return set;
+                });
+        }
+
+        private void keepParameterEquivalences() {
+                for (var pair : representatives.entrySet()) {
+                        var left = pair.getKey();
+                        var right = pair.getValue();
+                        if (!left.equals(right) && parameters.contains(left) && parameters.contains(right)) {
+                                substitutedLiterals.add(left.isEquivalent(right));
+                        }
+                }
+        }
+
+        private void substituteLiterals() {
+                var substitution = new MapBasedSubstitution(Collections.unmodifiableMap(representatives),
+                                StatelessSubstitution.IDENTITY);
+                for (var literal : literals) {
+                        if (isPositiveEquivalence(literal)) {
+                                // We already retained all equivalences that cannot be replaced with substitutions in
+                                // {@link#keepParameterEquivalences()}.
+                                continue;
+                        }
+                        var substitutedLiteral = literal.substitute(substitution);
+                        substitutedLiterals.add(substitutedLiteral);
+                }
+        }
+
+        private void computePositiveVariables() {
+                for (var literal : substitutedLiterals) {
+                        var variableBinder = literal.getVariableBinder();
+                        variableBinder.getVariablesWithDirection(VariableDirection.IN_OUT)
+                                        .forEach(existentiallyQuantifiedVariables::add);
+                        variableBinder.getVariablesWithDirection(VariableDirection.OUT).forEach(variable -> {
+                                boolean added = existentiallyQuantifiedVariables.add(variable);
+                                if (!added) {
+                                        throw new IllegalArgumentException("Variable %s has multiple %s bindings"
+                                                        .formatted(variable, VariableDirection.OUT));
+                                }
+                        });
+                }
+                // Input parameters are parameters not bound by any positive literal.
+                inputParameters = new LinkedHashSet<>(parameters);
+                inputParameters.removeAll(existentiallyQuantifiedVariables);
+                // Existentially quantified variables are variables appearing in positive literals that aren't parameters.
+                existentiallyQuantifiedVariables.removeAll(parameters);
+                // Positive variables are parameters (including input parameters) and variables bound by positive literals.
+                positiveVariables = new LinkedHashSet<>(parameters.size() + existentiallyQuantifiedVariables.size());
+                positiveVariables.addAll(parameters);
+                positiveVariables.addAll(existentiallyQuantifiedVariables);
+        }
+
+        private void validatePositiveRepresentatives() {
+                for (var pair : equivalencePartition.entrySet()) {
+                        var representative = pair.getKey();
+                        if (!positiveVariables.contains(representative)) {
+                                var variableSet = pair.getValue();
+                                throw new IllegalArgumentException("Variables %s were merged by equivalence but are not bound"
+                                                .formatted(variableSet));
+                        }
+                }
+        }
+
+        private void validateClosureVariables() {
+                var negativeVariablesMap = new HashMap<Variable, Literal>();
+                for (var literal : substitutedLiterals) {
+                        var variableBinder = literal.getVariableBinder();
+                        variableBinder.getVariablesWithDirection(VariableDirection.CLOSURE, positiveVariables)
+                                        .forEach(variable -> {
+                                                var oldLiteral = negativeVariablesMap.put(variable, literal);
+                                                if (oldLiteral != null) {
+                                                        throw new IllegalArgumentException(
+                                                                        "Unbound variable %s appears in multiple literals %s and %s"
+                                                                                        .formatted(variable, oldLiteral, literal));
+                                                }
+                                        });
+                }
+        }
+
+        private void topologicallySortLiterals() {
+                topologicallySortedLiterals = new LinkedHashSet<>(substitutedLiterals.size());
+                variableToLiteralInputMap = new HashMap<>();
+                literalsWithAllInputsBound = new PriorityQueue<>();
+                int size = substitutedLiterals.size();
+                for (int i = 0; i < size; i++) {
+                        var literal = substitutedLiterals.get(i);
+                        var sortableLiteral = new SortableLiteral(i, literal);
+                        sortableLiteral.enqueue();
+                }
+                while (!literalsWithAllInputsBound.isEmpty()) {
+                        var variable = literalsWithAllInputsBound.remove();
+                        variable.addToSortedLiterals();
+                }
+                if (!variableToLiteralInputMap.isEmpty()) {
+                        throw new IllegalArgumentException("Unbound input variables %s"
+                                        .formatted(variableToLiteralInputMap.keySet()));
+                }
+        }
+
+        private void topologicallySortVariable(Variable variable) {
+                var literalSetForInput = variableToLiteralInputMap.remove(variable);
+                if (literalSetForInput == null) {
+                        return;
+                }
+                for (var targetSortableLiteral : literalSetForInput) {
+                        targetSortableLiteral.bindVariable(variable);
+                }
+        }
+
+        private class SortableLiteral implements Comparable<SortableLiteral> {
+                private final int index;
+                private final Literal literal;
+                private final Set<Variable> remainingInputs;
+
+                private SortableLiteral(int index, Literal literal) {
+                        this.index = index;
+                        this.literal = literal;
+                        remainingInputs = literal.getVariableBinder()
+                                        .getVariablesWithDirection(VariableDirection.IN, positiveVariables)
+                                        .collect(Collectors.toCollection(HashSet::new));
+                        remainingInputs.removeAll(inputParameters);
+                }
+
+                public void enqueue() {
+                        if (allInputsBound()) {
+                                addToAllInputsBoundQueue();
+                        } else {
+                                addToVariableToLiteralInputMap();
+                        }
+                }
+
+                private void bindVariable(Variable input) {
+                        if (!remainingInputs.remove(input)) {
+                                throw new IllegalStateException("Already processed input %s of literal %s".formatted(input, literal));
+                        }
+                        if (allInputsBound()) {
+                                addToAllInputsBoundQueue();
+                        }
+                }
+
+                private boolean allInputsBound() {
+                        return remainingInputs.isEmpty();
+                }
+
+                private void addToVariableToLiteralInputMap() {
+                        for (var inputVariable : remainingInputs) {
+                                var literalSetForInput = variableToLiteralInputMap.computeIfAbsent(
+                                                inputVariable, key -> new HashSet<>());
+                                literalSetForInput.add(this);
+                        }
+                }
+
+                private void addToAllInputsBoundQueue() {
+                        literalsWithAllInputsBound.add(this);
+                }
+
+                public void addToSortedLiterals() {
+                        if (!allInputsBound()) {
+                                throw new AssertionError("Inputs %s of %s are not yet bound".formatted(remainingInputs, literal));
+                        }
+                        // Add literal if we haven't yet added a duplicate of this literal.
+                        topologicallySortedLiterals.add(literal);
+                        var variableBinder = literal.getVariableBinder();
+                        variableBinder.getVariablesWithDirection(VariableDirection.IN_OUT)
+                                        .forEach(ClausePostProcessor.this::topologicallySortVariable);
+                        variableBinder.getVariablesWithDirection(VariableDirection.OUT)
+                                        .forEach(ClausePostProcessor.this::topologicallySortVariable);
+                }
+
+                @Override
+                public int compareTo(@NotNull ClausePostProcessor.SortableLiteral other) {
+                        return Integer.compare(index, other.index);
+                }
+
+                @Override
+                public boolean equals(Object o) {
+                        if (this == o) return true;
+                        if (o == null || getClass() != o.getClass()) return false;
+                        SortableLiteral that = (SortableLiteral) o;
+                        return index == that.index && Objects.equals(literal, that.literal);
+                }
+
+                @Override
+                public int hashCode() {
+                        return Objects.hash(index, literal);
+                }
+        }
+
+        public sealed interface Result permits ClauseResult, ConstantResult {
+        }
+
+        public record ClauseResult(DnfClause clause) implements Result {
+        }
+
+        public enum ConstantResult implements Result {
+                ALWAYS_TRUE,
+                ALWAYS_FALSE
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java
index 8de5079d..7e68d4a0 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/Dnf.java
@@ -5,59 +5,57 @@
  */
 package tools.refinery.store.query.dnf;
 
+import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.equality.DnfEqualityChecker;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
-import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.literal.LiteralReduction;
-import tools.refinery.store.query.term.Sort;
+import tools.refinery.store.query.term.Parameter;
 import tools.refinery.store.query.term.Variable;
 
 import java.util.Collection;
-import java.util.HashSet;
+import java.util.Collections;
 import java.util.List;
 import java.util.Set;
 import java.util.function.Consumer;
+import java.util.stream.Collectors;
 
 public final class Dnf implements Constraint {
         private static final String INDENTATION = "    ";
 
         private final String name;
-
         private final String uniqueName;
-
-        private final List<Variable> parameters;
-
+        private final List<SymbolicParameter> symbolicParameters;
         private final List<FunctionalDependency<Variable>> functionalDependencies;
-
         private final List<DnfClause> clauses;
 
-        Dnf(String name, List<Variable> parameters, List<FunctionalDependency<Variable>> functionalDependencies,
-                List<DnfClause> clauses) {
-                validateFunctionalDependencies(parameters, functionalDependencies);
+        Dnf(String name, List<SymbolicParameter> symbolicParameters,
+                List<FunctionalDependency<Variable>> functionalDependencies, List<DnfClause> clauses) {
+                validateFunctionalDependencies(symbolicParameters, functionalDependencies);
                 this.name = name;
                 this.uniqueName = DnfUtils.generateUniqueName(name);
-                this.parameters = parameters;
+                this.symbolicParameters = symbolicParameters;
                 this.functionalDependencies = functionalDependencies;
                 this.clauses = clauses;
         }
 
         private static void validateFunctionalDependencies(
-                        Collection<Variable> parameters, Collection<FunctionalDependency<Variable>> functionalDependencies) {
-                var parameterSet = new HashSet<>(parameters);
+                        Collection<SymbolicParameter> symbolicParameters,
+                        Collection<FunctionalDependency<Variable>> functionalDependencies) {
+                var parameterSet = symbolicParameters.stream().map(SymbolicParameter::getVariable).collect(Collectors.toSet());
                 for (var functionalDependency : functionalDependencies) {
-                        validateParameters(parameters, parameterSet, functionalDependency.forEach(), functionalDependency);
-                        validateParameters(parameters, parameterSet, functionalDependency.unique(), functionalDependency);
+                        validateParameters(symbolicParameters, parameterSet, functionalDependency.forEach(), functionalDependency);
+                        validateParameters(symbolicParameters, parameterSet, functionalDependency.unique(), functionalDependency);
                 }
         }
 
-        private static void validateParameters(Collection<Variable> parameters, Set<Variable> parameterSet,
-                                                                                   Collection<Variable> toValidate,
+        private static void validateParameters(Collection<SymbolicParameter> symbolicParameters,
+                                                                                   Set<Variable> parameterSet, Collection<Variable> toValidate,
                                                                                    FunctionalDependency<Variable> functionalDependency) {
                 for (var variable : toValidate) {
                         if (!parameterSet.contains(variable)) {
                                 throw new IllegalArgumentException(
                                                 "Variable %s of functional dependency %s does not appear in the parameter list %s"
-                                                                .formatted(variable, functionalDependency, parameters));
+                                                                .formatted(variable, functionalDependency, symbolicParameters));
                         }
                 }
         }
@@ -75,13 +73,12 @@ public final class Dnf implements Constraint {
                 return uniqueName;
         }
 
-        public List<Variable> getParameters() {
-                return parameters;
+        public List<SymbolicParameter> getSymbolicParameters() {
+                return symbolicParameters;
         }
 
-        @Override
-        public List<Sort> getSorts() {
-                return parameters.stream().map(Variable::getSort).toList();
+        public List<Parameter> getParameters() {
+                return Collections.unmodifiableList(symbolicParameters);
         }
 
         public List<FunctionalDependency<Variable>> getFunctionalDependencies() {
@@ -90,7 +87,7 @@ public final class Dnf implements Constraint {
 
         @Override
         public int arity() {
-                return parameters.size();
+                return symbolicParameters.size();
         }
 
         public List<DnfClause> getClauses() {
@@ -127,7 +124,8 @@ public final class Dnf implements Constraint {
                         return false;
                 }
                 for (int i = 0; i < numClauses; i++) {
-                        var literalEqualityHelper = new LiteralEqualityHelper(callEqualityChecker, parameters, other.parameters);
+                        var literalEqualityHelper = new LiteralEqualityHelper(callEqualityChecker, symbolicParameters,
+                                        other.symbolicParameters);
                         if (!clauses.get(i).equalsWithSubstitution(literalEqualityHelper, other.clauses.get(i))) {
                                 return false;
                         }
@@ -145,18 +143,18 @@ public final class Dnf implements Constraint {
 
         @Override
         public String toString() {
-                return "%s/%d".formatted(name, arity());
+                return "%s/%d".formatted(name(), arity());
         }
 
         @Override
         public String toReferenceString() {
-                return "@Dnf " + name;
+                return "@Dnf " + name();
         }
 
         public String toDefinitionString() {
                 var builder = new StringBuilder();
                 builder.append("pred ").append(name()).append("(");
-                var parameterIterator = parameters.iterator();
+                var parameterIterator = symbolicParameters.iterator();
                 if (parameterIterator.hasNext()) {
                         builder.append(parameterIterator.next());
                         while (parameterIterator.hasNext()) {
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java
index a42ae558..3fac4627 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfBuilder.java
@@ -7,20 +7,16 @@ package tools.refinery.store.query.dnf;
 
 import tools.refinery.store.query.dnf.callback.*;
 import tools.refinery.store.query.literal.Literal;
-import tools.refinery.store.query.term.DataVariable;
-import tools.refinery.store.query.term.NodeVariable;
-import tools.refinery.store.query.term.Variable;
+import tools.refinery.store.query.term.*;
 
 import java.util.*;
 
 @SuppressWarnings("UnusedReturnValue")
 public final class DnfBuilder {
         private final String name;
-
         private final List<Variable> parameters = new ArrayList<>();
-
+        private final Map<Variable, ParameterDirection> directions = new HashMap<>();
         private final List<FunctionalDependency<Variable>> functionalDependencies = new ArrayList<>();
-
         private final List<List<Literal>> clauses = new ArrayList<>();
 
         DnfBuilder(String name) {
@@ -37,6 +33,18 @@ public final class DnfBuilder {
                 return variable;
         }
 
+        public NodeVariable parameter(ParameterDirection direction) {
+                var variable = parameter();
+                putDirection(variable, direction);
+                return variable;
+        }
+
+        public NodeVariable parameter(String name, ParameterDirection direction) {
+                var variable = parameter(name);
+                putDirection(variable, direction);
+                return variable;
+        }
+
         public <T> DataVariable<T> parameter(Class<T> type) {
                 return parameter(null, type);
         }
@@ -47,6 +55,18 @@ public final class DnfBuilder {
                 return variable;
         }
 
+        public <T> DataVariable<T> parameter(Class<T> type, ParameterDirection direction) {
+                var variable = parameter(type);
+                putDirection(variable, direction);
+                return variable;
+        }
+
+        public <T> DataVariable<T> parameter(String name, Class<T> type, ParameterDirection direction) {
+                var variable = parameter(name, type);
+                putDirection(variable, direction);
+                return variable;
+        }
+
         public DnfBuilder parameter(Variable variable) {
                 if (parameters.contains(variable)) {
                         throw new IllegalArgumentException("Duplicate parameter: " + variable);
@@ -55,12 +75,49 @@ public final class DnfBuilder {
                 return this;
         }
 
+        public DnfBuilder parameter(Variable variable, ParameterDirection direction) {
+                parameter(variable);
+                putDirection(variable, direction);
+                return this;
+        }
+
+        private void putDirection(Variable variable, ParameterDirection direction) {
+                if (variable.tryGetType().isPresent()) {
+                        if (direction == ParameterDirection.IN_OUT) {
+                                throw new IllegalArgumentException("%s direction is forbidden for data variable %s"
+                                                .formatted(direction, variable));
+                        }
+                } else {
+                        if (direction == ParameterDirection.OUT) {
+                                throw new IllegalArgumentException("%s direction is forbidden for node variable %s"
+                                                .formatted(direction, variable));
+                        }
+                }
+                directions.put(variable, direction);
+        }
+
         public DnfBuilder parameters(Variable... variables) {
                 return parameters(List.of(variables));
         }
 
         public DnfBuilder parameters(Collection<? extends Variable> variables) {
-                parameters.addAll(variables);
+                for (var variable : variables) {
+                        parameter(variable);
+                }
+                return this;
+        }
+
+        public DnfBuilder parameters(Collection<? extends Variable> variables, ParameterDirection direction) {
+                for (var variable : variables) {
+                        parameter(variable, direction);
+                }
+                return this;
+        }
+
+        public DnfBuilder symbolicParameters(Collection<SymbolicParameter> parameters) {
+                for (var parameter : parameters) {
+                        parameter(parameter.getVariable(), parameter.getDirection());
+                }
                 return this;
         }
 
@@ -152,54 +209,98 @@ public final class DnfBuilder {
         }
 
         public DnfBuilder clause(Collection<? extends Literal> literals) {
-                // Remove duplicates by using a hashed data structure.
-                var filteredLiterals = new LinkedHashSet<Literal>(literals.size());
-                for (var literal : literals) {
-                        var reduction = literal.getReduction();
-                        switch (reduction) {
-                        case NOT_REDUCIBLE -> filteredLiterals.add(literal);
-                        case ALWAYS_TRUE -> {
-                                // Literals reducible to {@code true} can be omitted, because the model is always assumed to have at
-                                // least on object.
-                        }
-                        case ALWAYS_FALSE -> {
-                                // Clauses with {@code false} literals can be omitted entirely.
-                                return this;
-                        }
-                        default -> throw new IllegalArgumentException("Invalid reduction: " + reduction);
-                        }
-                }
-                clauses.add(List.copyOf(filteredLiterals));
+                clauses.add(List.copyOf(literals));
                 return this;
         }
 
+        <T> void output(DataVariable<T> outputVariable) {
+                var fromParameters = Set.copyOf(parameters);
+                parameter(outputVariable, ParameterDirection.OUT);
+                functionalDependency(fromParameters, Set.of(outputVariable));
+        }
+
         public Dnf build() {
                 var postProcessedClauses = postProcessClauses();
-                return new Dnf(name, Collections.unmodifiableList(parameters),
+                return new Dnf(name, createParameterList(postProcessedClauses),
                                 Collections.unmodifiableList(functionalDependencies),
                                 Collections.unmodifiableList(postProcessedClauses));
         }
 
-        <T> void output(DataVariable<T> outputVariable) {
-                functionalDependency(Set.copyOf(parameters), Set.of(outputVariable));
-                parameter(outputVariable);
-        }
-
         private List<DnfClause> postProcessClauses() {
+                var parameterSet = Collections.unmodifiableSet(new LinkedHashSet<>(parameters));
+                var parameterWeights = getParameterWeights();
                 var postProcessedClauses = new ArrayList<DnfClause>(clauses.size());
                 for (var literals : clauses) {
-                        if (literals.isEmpty()) {
-                                // Predicate will always match, the other clauses are irrelevant.
-                                return List.of(new DnfClause(Set.of(), List.of()));
-                        }
-                        var variables = new HashSet<Variable>();
-                        for (var literal : literals) {
-                                variables.addAll(literal.getBoundVariables());
+                        var postProcessor = new ClausePostProcessor(parameterSet, parameterWeights, literals);
+                        var result = postProcessor.postProcessClause();
+                        if (result instanceof ClausePostProcessor.ClauseResult clauseResult) {
+                                postProcessedClauses.add(clauseResult.clause());
+                        } else if (result instanceof ClausePostProcessor.ConstantResult constantResult) {
+                                switch (constantResult) {
+                                case ALWAYS_TRUE -> {
+                                        return List.of(new DnfClause(Set.of(), List.of()));
+                                }
+                                case ALWAYS_FALSE -> {
+                                        // Skip this clause because it can never match.
+                                }
+                                default -> throw new IllegalStateException("Unexpected ClausePostProcessor.ConstantResult: " +
+                                                constantResult);
+                                }
+                        } else {
+                                throw new IllegalStateException("Unexpected ClausePostProcessor.Result: " + result);
                         }
-                        parameters.forEach(variables::remove);
-                        postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables),
-                                        Collections.unmodifiableList(literals)));
                 }
                 return postProcessedClauses;
         }
+
+        private Map<Variable, Integer> getParameterWeights() {
+                var mutableParameterWeights = new HashMap<Variable, Integer>();
+                int arity = parameters.size();
+                for (int i = 0; i < arity; i++) {
+                        mutableParameterWeights.put(parameters.get(i), i);
+                }
+                return Collections.unmodifiableMap(mutableParameterWeights);
+        }
+
+        private List<SymbolicParameter> createParameterList(List<DnfClause> postProcessedClauses) {
+                var outputParameterVariables = new HashSet<>(parameters);
+                for (var clause : postProcessedClauses) {
+                        outputParameterVariables.retainAll(clause.positiveVariables());
+                }
+                var parameterList = new ArrayList<SymbolicParameter>(parameters.size());
+                for (var parameter : parameters) {
+                        ParameterDirection direction = getDirection(outputParameterVariables, parameter);
+                        parameterList.add(new SymbolicParameter(parameter, direction));
+                }
+                return Collections.unmodifiableList(parameterList);
+        }
+
+        private ParameterDirection getDirection(HashSet<Variable> outputParameterVariables, Variable parameter) {
+                var direction = getInferredDirection(outputParameterVariables, parameter);
+                var expectedDirection = directions.get(parameter);
+                if (expectedDirection == ParameterDirection.IN && direction == ParameterDirection.IN_OUT) {
+                        // Parameters may be explicitly marked as {@code @In} even if they are bound in all clauses.
+                        return expectedDirection;
+                }
+                if (expectedDirection != null && expectedDirection != direction) {
+                        throw new IllegalArgumentException("Expected parameter %s to have direction %s, but got %s instead"
+                                        .formatted(parameter, expectedDirection, direction));
+                }
+                return direction;
+        }
+
+        private static ParameterDirection getInferredDirection(HashSet<Variable> outputParameterVariables,
+                                                                                                                   Variable parameter) {
+                if (outputParameterVariables.contains(parameter)) {
+                        if (parameter instanceof NodeVariable) {
+                                return ParameterDirection.IN_OUT;
+                        } else if (parameter instanceof AnyDataVariable) {
+                                return ParameterDirection.OUT;
+                        } else {
+                                throw new IllegalArgumentException("Unknown parameter: " + parameter);
+                        }
+                } else {
+                        return ParameterDirection.IN;
+                }
+        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java
index a01d7d55..fdd0d47c 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/DnfClause.java
@@ -12,7 +12,7 @@ import tools.refinery.store.query.term.Variable;
 import java.util.List;
 import java.util.Set;
 
-public record DnfClause(Set<Variable> boundVariables, List<Literal> literals) {
+public record DnfClause(Set<Variable> positiveVariables, List<Literal> literals) {
         public boolean equalsWithSubstitution(LiteralEqualityHelper helper, DnfClause other) {
                 int size = literals.size();
                 if (size != other.literals.size()) {
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQuery.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQuery.java
index 680fa631..57cb8baf 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQuery.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/FunctionalQuery.java
@@ -17,20 +17,21 @@ public final class FunctionalQuery<T> implements Query<T> {
         private final Class<T> type;
 
         FunctionalQuery(Dnf dnf, Class<T> type) {
-                var parameters = dnf.getParameters();
+                var parameters = dnf.getSymbolicParameters();
                 int outputIndex = dnf.arity() - 1;
                 for (int i = 0; i < outputIndex; i++) {
                         var parameter = parameters.get(i);
-                        if (!(parameter instanceof NodeVariable)) {
-                                throw new IllegalArgumentException("Expected parameter %s of %s to be of sort %s, but got %s instead"
-                                                .formatted(parameter, dnf, NodeSort.INSTANCE, parameter.getSort()));
+                        var parameterType = parameter.tryGetType();
+                        if (parameterType.isPresent()) {
+                                throw new IllegalArgumentException("Expected parameter %s of %s to be a node variable, got %s instead"
+                                                .formatted(parameter, dnf, parameterType.get().getName()));
                         }
                 }
                 var outputParameter = parameters.get(outputIndex);
-                if (!(outputParameter instanceof DataVariable<?> dataOutputParameter) ||
-                                !dataOutputParameter.getType().equals(type)) {
-                        throw new IllegalArgumentException("Expected parameter %s of %s to be of sort %s, but got %s instead"
-                                        .formatted(outputParameter, dnf, type, outputParameter.getSort()));
+                var outputParameterType = outputParameter.tryGetType();
+                if (outputParameterType.isEmpty() || !outputParameterType.get().equals(type)) {
+                        throw new IllegalArgumentException("Expected parameter %s of %s to be %s, but got %s instead".formatted(
+                                        outputParameter, dnf, type, outputParameterType.map(Class::getName).orElse("node")));
                 }
                 this.dnf = dnf;
                 this.type = type;
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/RelationalQuery.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/RelationalQuery.java
index 0741d8d9..c043a285 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/RelationalQuery.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/RelationalQuery.java
@@ -8,7 +8,6 @@ package tools.refinery.store.query.dnf;
 import tools.refinery.store.query.literal.CallLiteral;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.term.AssignedValue;
-import tools.refinery.store.query.term.NodeSort;
 import tools.refinery.store.query.term.NodeVariable;
 
 import java.util.Collections;
@@ -19,10 +18,11 @@ public final class RelationalQuery implements Query<Boolean> {
         private final Dnf dnf;
 
         RelationalQuery(Dnf dnf) {
-                for (var parameter : dnf.getParameters()) {
-                        if (!(parameter instanceof NodeVariable)) {
-                                throw new IllegalArgumentException("Expected parameter %s of %s to be of sort %s, but got %s instead"
-                                                .formatted(parameter, dnf, NodeSort.INSTANCE, parameter.getSort()));
+                for (var parameter : dnf.getSymbolicParameters()) {
+                        var parameterType = parameter.tryGetType();
+                        if (parameterType.isPresent()) {
+                                throw new IllegalArgumentException("Expected parameter %s of %s to be a node variable, got %s instead"
+                                                .formatted(parameter, dnf, parameterType.get().getName()));
                         }
                 }
                 this.dnf = dnf;
@@ -77,7 +77,6 @@ public final class RelationalQuery implements Query<Boolean> {
                 return dnf.count(arguments);
         }
 
-
         @Override
         public boolean equals(Object o) {
                 if (this == o) return true;
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/SymbolicParameter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/SymbolicParameter.java
new file mode 100644
index 00000000..e2f05bde
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/dnf/SymbolicParameter.java
@@ -0,0 +1,48 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.dnf;
+
+import tools.refinery.store.query.term.Parameter;
+import tools.refinery.store.query.term.ParameterDirection;
+import tools.refinery.store.query.term.Variable;
+
+import java.util.Objects;
+
+public final class SymbolicParameter extends Parameter {
+        private final Variable variable;
+
+        public SymbolicParameter(Variable variable, ParameterDirection direction) {
+                super(variable.tryGetType().orElse(null), direction);
+                this.variable = variable;
+        }
+
+        public Variable getVariable() {
+                return variable;
+        }
+
+        @Override
+        public String toString() {
+                var direction = getDirection();
+                if (direction == ParameterDirection.IN_OUT) {
+                        return variable.toString();
+                }
+                return "%s %s".formatted(getDirection(), variable);
+        }
+
+        @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;
+                SymbolicParameter that = (SymbolicParameter) o;
+                return Objects.equals(variable, that.variable);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), variable);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java
index 0f6ee6c2..9315fb30 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java
@@ -6,6 +6,7 @@
 package tools.refinery.store.query.equality;
 
 import tools.refinery.store.query.dnf.Dnf;
+import tools.refinery.store.query.dnf.SymbolicParameter;
 import tools.refinery.store.query.term.Variable;
 
 import java.util.HashMap;
@@ -17,8 +18,8 @@ public class LiteralEqualityHelper {
         private final Map<Variable, Variable> leftToRight;
         private final Map<Variable, Variable> rightToLeft;
 
-        public LiteralEqualityHelper(DnfEqualityChecker dnfEqualityChecker, List<Variable> leftParameters,
-                                                                 List<Variable> rightParameters) {
+        public LiteralEqualityHelper(DnfEqualityChecker dnfEqualityChecker, List<SymbolicParameter> leftParameters,
+                                                                 List<SymbolicParameter> rightParameters) {
                 this.dnfEqualityChecker = dnfEqualityChecker;
                 var arity = leftParameters.size();
                 if (arity != rightParameters.size()) {
@@ -27,7 +28,7 @@ public class LiteralEqualityHelper {
                 leftToRight = new HashMap<>(arity);
                 rightToLeft = new HashMap<>(arity);
                 for (int i = 0; i < arity; i++) {
-                        if (!variableEqual(leftParameters.get(i), rightParameters.get(i))) {
+                        if (!variableEqual(leftParameters.get(i).getVariable(), rightParameters.get(i).getVariable())) {
                                 throw new IllegalArgumentException("Parameter lists cannot be unified: duplicate parameter " + i);
                         }
                 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/exceptions/IncompatibleParameterDirectionException.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/exceptions/IncompatibleParameterDirectionException.java
new file mode 100644
index 00000000..52da20ae
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/exceptions/IncompatibleParameterDirectionException.java
@@ -0,0 +1,16 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.exceptions;
+
+public class IncompatibleParameterDirectionException extends RuntimeException {
+        public IncompatibleParameterDirectionException(String message) {
+                super(message);
+        }
+
+        public IncompatibleParameterDirectionException(String message, Throwable cause) {
+                super(message, cause);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java
index b08c1037..55db04e0 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AbstractCallLiteral.java
@@ -25,13 +25,13 @@ public abstract class AbstractCallLiteral implements Literal {
                 }
                 this.target = target;
                 this.arguments = arguments;
-                var sorts = target.getSorts();
+                var parameters = target.getParameters();
                 for (int i = 0; i < arity; i++) {
                         var argument = arguments.get(i);
-                        var sort = sorts.get(i);
-                        if (!sort.isInstance(argument)) {
-                                throw new IllegalArgumentException("Required argument %d of %s to be of sort %s, but got %s instead"
-                                                .formatted(i, target, sort, argument.getSort()));
+                        var parameter = parameters.get(i);
+                        if (!parameter.isAssignable(argument)) {
+                                throw new IllegalArgumentException("Argument %d of %s is not assignable to parameter %s"
+                                                .formatted(i, target, parameter));
                         }
                 }
         }
@@ -80,6 +80,6 @@ public abstract class AbstractCallLiteral implements Literal {
 
         @Override
         public int hashCode() {
-                return Objects.hash(target, arguments);
+                return Objects.hash(getClass(), target, arguments);
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java
index 93e59291..2aa0a0d5 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AggregationLiteral.java
@@ -14,12 +14,12 @@ import tools.refinery.store.query.term.Variable;
 
 import java.util.List;
 import java.util.Objects;
-import java.util.Set;
 
 public class AggregationLiteral<R, T> extends AbstractCallLiteral {
         private final DataVariable<R> resultVariable;
         private final DataVariable<T> inputVariable;
         private final Aggregator<R, T> aggregator;
+        private final VariableBinder variableBinder;
 
         public AggregationLiteral(DataVariable<R> resultVariable, Aggregator<R, T> aggregator,
                                                           DataVariable<T> inputVariable, Constraint target, List<Variable> arguments) {
@@ -32,10 +32,6 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral {
                         throw new IllegalArgumentException("Result variable %s must of type %s, got %s instead".formatted(
                                         resultVariable, aggregator.getResultType().getName(), resultVariable.getType().getName()));
                 }
-                if (!arguments.contains(inputVariable)) {
-                        throw new IllegalArgumentException("Input variable %s must appear in the argument list".formatted(
-                                        inputVariable));
-                }
                 if (arguments.contains(resultVariable)) {
                         throw new IllegalArgumentException("Result variable %s must not appear in the argument list".formatted(
                                         resultVariable));
@@ -43,6 +39,14 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral {
                 this.resultVariable = resultVariable;
                 this.inputVariable = inputVariable;
                 this.aggregator = aggregator;
+                variableBinder = VariableBinder.builder()
+                                .variable(resultVariable, VariableDirection.OUT)
+                                .parameterList(false, target.getParameters(), arguments)
+                                .build();
+                if (variableBinder.getDirection(inputVariable) != VariableDirection.CLOSURE) {
+                        throw new IllegalArgumentException("Input variable %s must appear in the argument list".formatted(
+                                        inputVariable));
+                }
         }
 
         public DataVariable<R> getResultVariable() {
@@ -58,8 +62,8 @@ public class AggregationLiteral<R, T> extends AbstractCallLiteral {
         }
 
         @Override
-        public Set<Variable> getBoundVariables() {
-                return Set.of(resultVariable);
+        public VariableBinder getVariableBinder() {
+                return variableBinder;
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java
index 8cc3fae6..4da92b90 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssignLiteral.java
@@ -9,21 +9,43 @@ import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.DataVariable;
 import tools.refinery.store.query.term.Term;
-import tools.refinery.store.query.term.Variable;
 
-import java.util.Set;
+import java.util.Objects;
 
-public record AssignLiteral<T>(DataVariable<T> variable, Term<T> term) implements Literal {
-        public AssignLiteral {
+public final class AssignLiteral<T> implements Literal {
+        private final DataVariable<T> variable;
+        private final Term<T> term;
+        private final VariableBinder variableBinder;
+
+        public AssignLiteral(DataVariable<T> variable, Term<T> term) {
                 if (!term.getType().equals(variable.getType())) {
                         throw new IllegalArgumentException("Term %s must be of type %s, got %s instead".formatted(
                                         term, variable.getType().getName(), term.getType().getName()));
                 }
+                this.variable = variable;
+                this.term = term;
+                var inputVariables = term.getInputVariables();
+                if (inputVariables.contains(variable)) {
+                        throw new IllegalArgumentException("Result variable %s must not appear in the term %s".formatted(
+                                        variable, term));
+                }
+                variableBinder = VariableBinder.builder()
+                                .variable(variable, VariableDirection.OUT)
+                                .variables(inputVariables, VariableDirection.IN)
+                                .build();
+        }
+
+        public DataVariable<T> getTargetVariable() {
+                return variable;
+        }
+
+        public Term<T> getTerm() {
+                return term;
         }
 
         @Override
-        public Set<Variable> getBoundVariables() {
-                return Set.of(variable);
+        public VariableBinder getVariableBinder() {
+                return variableBinder;
         }
 
         @Override
@@ -41,9 +63,22 @@ public record AssignLiteral<T>(DataVariable<T> variable, Term<T> term) implement
                                 otherLetLiteral.term);
         }
 
-
         @Override
         public String toString() {
                 return "%s is (%s)".formatted(variable, term);
         }
+
+        @Override
+        public boolean equals(Object obj) {
+                if (obj == this) return true;
+                if (obj == null || obj.getClass() != this.getClass()) return false;
+                var that = (AssignLiteral<?>) obj;
+                return Objects.equals(this.variable, that.variable) &&
+                                Objects.equals(this.term, that.term);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(getClass(), variable, term);
+        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/AssumeLiteral.java
index 59538831..61486e4c 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
@@ -9,21 +9,31 @@ 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 java.util.Set;
+import java.util.Objects;
 
-public record AssumeLiteral(Term<Boolean> term) implements Literal {
-        public AssumeLiteral {
+public final class AssumeLiteral implements Literal {
+        private final Term<Boolean> term;
+        private final VariableBinder variableBinder;
+
+        public AssumeLiteral(Term<Boolean> term) {
                 if (!term.getType().equals(Boolean.class)) {
                         throw new IllegalArgumentException("Term %s must be of type %s, got %s instead".formatted(
                                         term, Boolean.class.getName(), term.getType().getName()));
                 }
+                this.term = term;
+                variableBinder = VariableBinder.builder()
+                                .variables(term.getInputVariables(), VariableDirection.IN)
+                                .build();
+        }
+
+        public Term<Boolean> getTerm() {
+                return term;
         }
 
         @Override
-        public Set<Variable> getBoundVariables() {
-                return Set.of();
+        public VariableBinder getVariableBinder() {
+                return variableBinder;
         }
 
         @Override
@@ -54,4 +64,17 @@ public record AssumeLiteral(Term<Boolean> term) implements Literal {
         public String toString() {
                 return "(%s)".formatted(term);
         }
+
+        @Override
+        public boolean equals(Object obj) {
+                if (obj == this) return true;
+                if (obj == null || obj.getClass() != this.getClass()) return false;
+                var that = (AssumeLiteral) obj;
+                return Objects.equals(this.term, that.term);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(getClass(), term);
+        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
index a32cfd80..e61f0535 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
@@ -5,12 +5,9 @@
  */
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.substitution.Substitution;
 
-import java.util.Set;
-
 public enum BooleanLiteral implements CanNegate<BooleanLiteral> {
         TRUE(true),
         FALSE(false);
@@ -22,8 +19,8 @@ public enum BooleanLiteral implements CanNegate<BooleanLiteral> {
         }
 
         @Override
-        public Set<Variable> getBoundVariables() {
-                return Set.of();
+        public VariableBinder getVariableBinder() {
+                return VariableBinder.EMPTY;
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
index 82088c8b..dc6098a8 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
@@ -8,28 +8,31 @@ package tools.refinery.store.query.literal;
 import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.substitution.Substitution;
-import tools.refinery.store.query.term.NodeSort;
 import tools.refinery.store.query.term.Variable;
 
 import java.util.List;
 import java.util.Objects;
-import java.util.Set;
 
 public final class CallLiteral extends AbstractCallLiteral implements CanNegate<CallLiteral> {
         private final CallPolarity polarity;
+        private final VariableBinder variableBinder;
 
         public CallLiteral(CallPolarity polarity, Constraint target, List<Variable> arguments) {
                 super(target, arguments);
+                var parameters = target.getParameters();
+                int arity = target.arity();
                 if (polarity.isTransitive()) {
-                        if (target.arity() != 2) {
+                        if (arity != 2) {
                                 throw new IllegalArgumentException("Transitive closures can only take binary relations");
                         }
-                        var sorts = target.getSorts();
-                        if (!sorts.get(0).equals(NodeSort.INSTANCE) || !sorts.get(1).equals(NodeSort.INSTANCE)) {
+                        if (parameters.get(0).isDataVariable() || parameters.get(1).isDataVariable()) {
                                 throw new IllegalArgumentException("Transitive closures can only be computed over nodes");
                         }
                 }
                 this.polarity = polarity;
+                variableBinder = VariableBinder.builder()
+                                .parameterList(polarity.isPositive(), parameters, arguments)
+                                .build();
         }
 
         public CallPolarity getPolarity() {
@@ -37,8 +40,8 @@ public final class CallLiteral extends AbstractCallLiteral implements CanNegate<
         }
 
         @Override
-        public Set<Variable> getBoundVariables() {
-                return polarity.isPositive() ? Set.copyOf(getArguments()) : Set.of();
+        public VariableBinder getVariableBinder() {
+                return variableBinder;
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
index fa7979d1..7466cb1d 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
@@ -8,14 +8,31 @@ package tools.refinery.store.query.literal;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.term.NodeVariable;
-import tools.refinery.store.query.term.Variable;
 
-import java.util.Set;
+import java.util.Objects;
+
+public final class ConstantLiteral implements Literal {
+        private final NodeVariable variable;
+        private final int nodeId;
+        private final VariableBinder variableBinder;
+
+        public ConstantLiteral(NodeVariable variable, int nodeId) {
+                this.variable = variable;
+                this.nodeId = nodeId;
+                variableBinder = VariableBinder.builder().variable(variable, VariableDirection.IN_OUT).build();
+        }
+
+        public NodeVariable getVariable() {
+                return variable;
+        }
+
+        public int getNodeId() {
+                return nodeId;
+        }
 
-public record ConstantLiteral(NodeVariable variable, int nodeId) implements Literal {
         @Override
-        public Set<Variable> getBoundVariables() {
-                return Set.of(variable);
+        public VariableBinder getVariableBinder() {
+                return variableBinder;
         }
 
         @Override
@@ -32,8 +49,23 @@ public record ConstantLiteral(NodeVariable variable, int nodeId) implements Lite
                 return helper.variableEqual(variable, otherConstantLiteral.variable) && nodeId == otherConstantLiteral.nodeId;
         }
 
+
         @Override
         public String toString() {
                 return "%s === @Constant %d".formatted(variable, nodeId);
         }
+
+        @Override
+        public boolean equals(Object obj) {
+                if (obj == this) return true;
+                if (obj == null || obj.getClass() != this.getClass()) return false;
+                var that = (ConstantLiteral) obj;
+                return Objects.equals(this.variable, that.variable) &&
+                                this.nodeId == that.nodeId;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(getClass(), variable, nodeId);
+        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
index 11f78fa8..a602d982 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CountLiteral.java
@@ -13,10 +13,10 @@ import tools.refinery.store.query.term.Variable;
 
 import java.util.List;
 import java.util.Objects;
-import java.util.Set;
 
 public class CountLiteral extends AbstractCallLiteral {
         private final DataVariable<Integer> resultVariable;
+        private final VariableBinder variableBinder;
 
         public CountLiteral(DataVariable<Integer> resultVariable, Constraint target, List<Variable> arguments) {
                 super(target, arguments);
@@ -29,6 +29,10 @@ public class CountLiteral extends AbstractCallLiteral {
                                         .formatted(resultVariable));
                 }
                 this.resultVariable = resultVariable;
+                variableBinder = VariableBinder.builder()
+                                .variable(resultVariable, VariableDirection.OUT)
+                                .parameterList(false, target.getParameters(), arguments)
+                                .build();
         }
 
         public DataVariable<Integer> getResultVariable() {
@@ -36,8 +40,8 @@ public class CountLiteral extends AbstractCallLiteral {
         }
 
         @Override
-        public Set<Variable> getBoundVariables() {
-                return Set.of(resultVariable);
+        public VariableBinder getVariableBinder() {
+                return variableBinder;
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
index 3876574c..794cee0d 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
@@ -5,20 +5,44 @@
  */
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.term.NodeVariable;
-import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.substitution.Substitution;
+import tools.refinery.store.query.term.NodeVariable;
 
-import java.util.Set;
+import java.util.Objects;
 
-public record EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right)
+public final class EquivalenceLiteral
                 implements CanNegate<EquivalenceLiteral> {
+        private final boolean positive;
+        private final NodeVariable left;
+        private final NodeVariable right;
+        private final VariableBinder variableBinder;
+
+        public EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariable right) {
+                this.positive = positive;
+                this.left = left;
+                this.right = right;
+                variableBinder = VariableBinder.builder()
+                                .variable(left, positive ? VariableDirection.IN_OUT : VariableDirection.IN)
+                                .variable(right, VariableDirection.IN)
+                                .build();
+        }
+
+        public boolean isPositive() {
+                return positive;
+        }
+
+        public NodeVariable getLeft() {
+                return left;
+        }
+
+        public NodeVariable getRight() {
+                return right;
+        }
+
         @Override
-        public Set<Variable> getBoundVariables() {
-                // If one side of a {@code positive} equivalence is bound, it may bind its other side, but we under-approximate
-                // this behavior by not binding any of the sides by default.
-                return Set.of();
+        public VariableBinder getVariableBinder() {
+                return variableBinder;
         }
 
         @Override
@@ -54,4 +78,19 @@ public record EquivalenceLiteral(boolean positive, NodeVariable left, NodeVariab
         public String toString() {
                 return "%s %s %s".formatted(left, positive ? "===" : "!==", right);
         }
+
+        @Override
+        public boolean equals(Object obj) {
+                if (obj == this) return true;
+                if (obj == null || obj.getClass() != this.getClass()) return false;
+                var that = (EquivalenceLiteral) obj;
+                return this.positive == that.positive &&
+                                Objects.equals(this.left, that.left) &&
+                                Objects.equals(this.right, that.right);
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(getClass(), positive, left, right);
+        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
index 52411ee8..c3c111a4 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
@@ -5,14 +5,11 @@
  */
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.substitution.Substitution;
 
-import java.util.Set;
-
 public interface Literal {
-        Set<Variable> getBoundVariables();
+        VariableBinder getVariableBinder();
 
         Literal substitute(Substitution substitution);
 
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java
new file mode 100644
index 00000000..5f43d07d
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinder.java
@@ -0,0 +1,64 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.term.Variable;
+
+import java.util.Map;
+import java.util.Set;
+import java.util.stream.Stream;
+
+public final class VariableBinder {
+        public static final VariableBinder EMPTY = new VariableBinder(Map.of());
+
+        private final Map<Variable, VariableDirection> directionMap;
+
+        VariableBinder(Map<Variable, VariableDirection> directionMap) {
+                this.directionMap = directionMap;
+        }
+
+        public VariableDirection getDirection(Variable variable) {
+                var direction = directionMap.get(variable);
+                if (direction == null) {
+                        throw new IllegalArgumentException("No such variable " + variable);
+                }
+                return direction;
+        }
+
+        public VariableDirection getDirection(Variable variable, Set<? extends Variable> positiveVariables) {
+                var direction = getDirection(variable);
+                return disambiguateDirection(direction, variable, positiveVariables);
+        }
+
+        public Stream<Variable> getVariablesWithDirection(VariableDirection direction) {
+                return directionMap.entrySet().stream()
+                                .filter(pair -> pair.getValue() == direction)
+                                .map(Map.Entry::getKey);
+        }
+
+        public Stream<Variable> getVariablesWithDirection(VariableDirection direction,
+                                                                                                          Set<? extends Variable> positiveVariables) {
+                if (direction == VariableDirection.NEGATIVE) {
+                        throw new IllegalArgumentException("Use #getVariablesWithDirection(VariableDirection) if disambiguation " +
+                                        "of VariableDirection#NEGATIVE variables according to the containing DnfClose is not desired");
+                }
+                return directionMap.entrySet().stream()
+                                .filter(pair -> disambiguateDirection(pair.getValue(), pair.getKey(), positiveVariables) == direction)
+                                .map(Map.Entry::getKey);
+        }
+
+        private VariableDirection disambiguateDirection(VariableDirection direction, Variable variable,
+                                                                                                        Set<? extends Variable> positiveVariables) {
+                if (direction != VariableDirection.NEGATIVE) {
+                        return direction;
+                }
+                return positiveVariables.contains(variable) ? VariableDirection.IN : VariableDirection.CLOSURE;
+        }
+
+        public static VariableBinderBuilder builder() {
+                return new VariableBinderBuilder();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java
new file mode 100644
index 00000000..b0d47240
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableBinderBuilder.java
@@ -0,0 +1,96 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.exceptions.IncompatibleParameterDirectionException;
+import tools.refinery.store.query.term.*;
+
+import java.util.*;
+
+public final class VariableBinderBuilder {
+        private final Map<Variable, VariableDirection> directionMap = new LinkedHashMap<>();
+        private final Set<Variable> uniqueVariables = new HashSet<>();
+
+        VariableBinderBuilder() {
+        }
+
+        public VariableBinderBuilder variable(Variable variable, VariableDirection direction) {
+                return variable(variable, direction, direction == VariableDirection.OUT);
+        }
+
+        private VariableBinderBuilder variable(Variable variable, VariableDirection direction, boolean markAsUnique) {
+                validateDirection(variable, direction);
+                boolean unique = shouldBeUnique(variable, markAsUnique);
+                directionMap.compute(variable, (ignored, oldValue) -> {
+                        if (oldValue == null) {
+                                return direction;
+                        }
+                        if (unique) {
+                                throw new IllegalArgumentException("Duplicate binding for variable " + variable);
+                        }
+                        try {
+                                return oldValue.merge(direction);
+                        } catch (IncompatibleParameterDirectionException e) {
+                                var message = "%s for variable %s".formatted(e.getMessage(), variable);
+                                throw new IncompatibleParameterDirectionException(message, e);
+                        }
+                });
+                return this;
+        }
+
+        private static void validateDirection(Variable variable, VariableDirection direction) {
+                if (variable instanceof AnyDataVariable) {
+                        if (direction == VariableDirection.IN_OUT) {
+                                throw new IllegalArgumentException("%s direction is not supported for data variable %s"
+                                                .formatted(direction, variable));
+                        }
+                } else if (variable instanceof NodeVariable) {
+                        if (direction == VariableDirection.OUT) {
+                                throw new IllegalArgumentException("%s direction is not supported for node variable %s"
+                                                .formatted(direction, variable));
+                        }
+                } else {
+                        throw new IllegalArgumentException("Unknown variable " + variable);
+                }
+        }
+
+        private boolean shouldBeUnique(Variable variable, boolean markAsUnique) {
+                if (markAsUnique) {
+                        uniqueVariables.add(variable);
+                        return true;
+                } else {
+                        return uniqueVariables.contains(variable);
+                }
+        }
+
+        public VariableBinderBuilder variables(Collection<? extends Variable> variables, VariableDirection direction) {
+                for (var variable : variables) {
+                        variable(variable, direction);
+                }
+                return this;
+        }
+
+        public VariableBinderBuilder parameterList(boolean positive, List<Parameter> parameters,
+                                                                                           List<Variable> arguments) {
+                int arity = parameters.size();
+                if (arity != arguments.size()) {
+                        throw new IllegalArgumentException("Got %d arguments for %d parameters"
+                                        .formatted(arguments.size(), arity));
+                }
+                for (int i = 0; i < arity; i++) {
+                        var argument = arguments.get(i);
+                        var parameter = parameters.get(i);
+                        var parameterDirection = parameter.getDirection();
+                        var direction = VariableDirection.from(positive, parameterDirection);
+                        variable(argument, direction, parameterDirection == ParameterDirection.OUT);
+                }
+                return this;
+        }
+
+        public VariableBinder build() {
+                return new VariableBinder(directionMap);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableDirection.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableDirection.java
new file mode 100644
index 00000000..444dcbbf
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/VariableDirection.java
@@ -0,0 +1,101 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.literal;
+
+import tools.refinery.store.query.exceptions.IncompatibleParameterDirectionException;
+import tools.refinery.store.query.term.ParameterDirection;
+
+public enum VariableDirection {
+        /**
+         * Binds a node variable or check equality with a node variable.
+         * <p>
+         * This is the usual direction for positive constraints on nodes. A data variable may have multiple {@code InOut}
+         * bindings, even on the same parameter list.
+         * <p>
+         * Cannot be used for data variables.
+         */
+        IN_OUT("@InOut"),
+
+        /**
+         * Binds a data variable.
+         * <p>
+         * A single variable must have at most one {@code @Out} binding. A variable with a {@code @Out} binding cannot
+         * appear in any other place in a parameter list.
+         * <p>
+         * Cannot be used for node variables.
+         */
+        OUT("@Out"),
+
+        /**
+         * Either takes a bound data variable or enumerates all possible data variable bindings.
+         * <p>
+         * Cannot be used for data variables.
+         */
+        NEGATIVE("@Negative"),
+
+        /**
+         * Takes an already bound variable.
+         * <p>
+         * May be used with node or data variables. An {@code @InOut} or {@code @Out} binding on the same parameter list
+         * cannot satisfy the {@code @In} binding, because it might introduce a (non-monotonic) circular dependency.
+         */
+        IN("@In"),
+
+        /**
+         * Enumerates over all possible data variable bindings.
+         * <p>
+         * May be used with node or data variables. The variable may not appear in any other parameter list. A data
+         * variable may only appear once in the parameter list, but node variables can appear multiple times to form
+         * diagonal constraints.
+         */
+        CLOSURE("@Closure");
+
+        private final String name;
+
+        VariableDirection(String name) {
+                this.name = name;
+        }
+
+        public VariableDirection merge(VariableDirection other) {
+                switch (this) {
+                case IN_OUT -> {
+                        if (other == IN_OUT) {
+                                return this;
+                        }
+                }
+                case OUT -> {
+                        if (other == OUT) {
+                                throw new IncompatibleParameterDirectionException("Multiple %s bindings".formatted(this));
+                        }
+                }
+                case NEGATIVE -> {
+                        if (other == NEGATIVE || other == IN || other == CLOSURE) {
+                                return other;
+                        }
+                }
+                case IN, CLOSURE -> {
+                        if (other == NEGATIVE || other == this) {
+                                return this;
+                        }
+                }
+                }
+                throw new IncompatibleParameterDirectionException("Incompatible variable directions %s and %s"
+                                .formatted(this, other));
+        }
+
+        @Override
+        public String toString() {
+                return name;
+        }
+
+        public static VariableDirection from(boolean positive, ParameterDirection parameterDirection) {
+                return switch (parameterDirection) {
+                        case IN_OUT -> positive ? IN_OUT : NEGATIVE;
+                        case OUT -> positive ? OUT : CLOSURE;
+                        case IN -> IN;
+                };
+        }
+}
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
index 658a26e3..37fb6908 100644
--- 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
@@ -32,9 +32,10 @@ public class SubstitutionBuilder {
         }
 
         public SubstitutionBuilder putChecked(Variable original, Variable substitute) {
-                if (!original.getSort().equals(substitute.getSort())) {
+                if (!original.tryGetType().equals(substitute.tryGetType())) {
                         throw new IllegalArgumentException("Cannot substitute variable %s of sort %s with variable %s of sort %s"
-                                        .formatted(original, original.getSort(), substitute, substitute.getSort()));
+                                        .formatted(original, original.tryGetType().map(Class::getName).orElse("node"), substitute,
+                                                        substitute.tryGetType().map(Class::getName).orElse("node")));
                 }
                 if (map.containsKey(original)) {
                         throw new IllegalArgumentException("Already has substitution for variable %s".formatted(original));
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java
index ccc063af..5864ee56 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/AnyDataVariable.java
@@ -8,6 +8,7 @@ package tools.refinery.store.query.term;
 import org.jetbrains.annotations.Nullable;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
 
+import java.util.Optional;
 import java.util.Set;
 
 public abstract sealed class AnyDataVariable extends Variable implements AnyTerm permits DataVariable {
@@ -16,6 +17,11 @@ public abstract sealed class AnyDataVariable extends Variable implements AnyTerm
         }
 
         @Override
+        public Optional<Class<?>> tryGetType() {
+                return Optional.of(getType());
+        }
+
+        @Override
         public NodeVariable asNodeVariable() {
                 throw new IllegalStateException("%s is a data variable".formatted(this));
         }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataSort.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataSort.java
deleted file mode 100644
index 6b8669ee..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataSort.java
+++ /dev/null
@@ -1,34 +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 org.jetbrains.annotations.Nullable;
-
-public record DataSort<T>(Class<T> type) implements Sort {
-        public static final DataSort<Integer> INT = new DataSort<>(Integer.class);
-
-        public static final DataSort<Boolean> BOOL = new DataSort<>(Boolean.class);
-
-        @Override
-        public boolean isInstance(Variable variable) {
-                return variable instanceof DataVariable<?> dataVariable && type.equals(dataVariable.getType());
-        }
-
-        @Override
-        public DataVariable<T> newInstance(@Nullable String name) {
-                return Variable.of(name, type);
-        }
-
-        @Override
-        public DataVariable<T> newInstance() {
-                return newInstance(null);
-        }
-
-        @Override
-        public String toString() {
-                return type.getName();
-        }
-}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java
index db160f68..00950360 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/DataVariable.java
@@ -22,11 +22,6 @@ public final class DataVariable<T> extends AnyDataVariable implements Term<T> {
         }
 
         @Override
-        public DataSort<T> getSort() {
-                return new DataSort<>(getType());
-        }
-
-        @Override
         public Class<T> getType() {
                 return type;
         }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeSort.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeSort.java
deleted file mode 100644
index b9be03f7..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeSort.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;
-
-import org.jetbrains.annotations.Nullable;
-
-public final class NodeSort implements Sort {
-        public static final NodeSort INSTANCE = new NodeSort();
-
-        private NodeSort() {
-        }
-
-        @Override
-        public boolean isInstance(Variable variable) {
-                return variable instanceof NodeVariable;
-        }
-
-        @Override
-        public NodeVariable newInstance(@Nullable String name) {
-                return new NodeVariable(name);
-        }
-
-        @Override
-        public NodeVariable newInstance() {
-                return newInstance(null);
-        }
-
-        @Override
-        public String toString() {
-                return "<node>";
-        }
-}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java
index de2f945a..37f9d477 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/NodeVariable.java
@@ -9,14 +9,16 @@ import org.jetbrains.annotations.Nullable;
 import tools.refinery.store.query.literal.ConstantLiteral;
 import tools.refinery.store.query.literal.EquivalenceLiteral;
 
+import java.util.Optional;
+
 public final class NodeVariable extends Variable {
         NodeVariable(@Nullable String name) {
                 super(name);
         }
 
         @Override
-        public NodeSort getSort() {
-                return NodeSort.INSTANCE;
+        public Optional<Class<?>> tryGetType() {
+                return Optional.empty();
         }
 
         @Override
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Parameter.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Parameter.java
new file mode 100644
index 00000000..29aedbef
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Parameter.java
@@ -0,0 +1,63 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term;
+
+import java.util.Objects;
+import java.util.Optional;
+
+public class Parameter {
+        public static final Parameter NODE_IN_OUT = new Parameter(null, ParameterDirection.IN_OUT);
+
+        private final Class<?> dataType;
+        private final ParameterDirection direction;
+
+        public Parameter(Class<?> dataType, ParameterDirection direction) {
+                this.dataType = dataType;
+                this.direction = direction;
+                if (isDataVariable()) {
+                        if (direction == ParameterDirection.IN_OUT) {
+                                throw new IllegalArgumentException("IN_OUT direction is not supported for data parameters");
+                        }
+                } else if (direction == ParameterDirection.OUT) {
+                        throw new IllegalArgumentException("OUT direction is not supported for node parameters");
+                }
+        }
+
+        public boolean isDataVariable() {
+                return dataType != null;
+        }
+
+        public Optional<Class<?>> tryGetType() {
+                return Optional.ofNullable(dataType);
+        }
+
+        public ParameterDirection getDirection() {
+                return direction;
+        }
+
+        public boolean isAssignable(Variable variable) {
+                if (variable instanceof AnyDataVariable dataVariable) {
+                        return dataVariable.getType().equals(dataType);
+                } else if (variable instanceof NodeVariable) {
+                        return !isDataVariable();
+                } else {
+                        throw new IllegalArgumentException("Unknown variable " + variable);
+                }
+        }
+
+        @Override
+        public boolean equals(Object o) {
+                if (this == o) return true;
+                if (o == null || getClass() != o.getClass()) return false;
+                Parameter parameter = (Parameter) o;
+                return Objects.equals(dataType, parameter.dataType) && direction == parameter.direction;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(dataType, direction);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ParameterDirection.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ParameterDirection.java
new file mode 100644
index 00000000..652208aa
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/ParameterDirection.java
@@ -0,0 +1,23 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.term;
+
+public enum ParameterDirection {
+        IN_OUT("@InOut"),
+        OUT("@Out"),
+        IN("@In");
+
+        private final String name;
+
+        ParameterDirection(String name) {
+                this.name = name;
+        }
+
+        @Override
+        public String toString() {
+                return name;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Sort.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Sort.java
deleted file mode 100644
index 2b3345f9..00000000
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Sort.java
+++ /dev/null
@@ -1,16 +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 org.jetbrains.annotations.Nullable;
-
-public sealed interface Sort permits DataSort, NodeSort {
-        boolean isInstance(Variable variable);
-
-        Variable newInstance(@Nullable String name);
-
-        Variable newInstance();
-}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java
index c4ca6f77..869120fa 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/term/Variable.java
@@ -9,6 +9,7 @@ import org.jetbrains.annotations.Nullable;
 import tools.refinery.store.query.dnf.DnfUtils;
 
 import java.util.Objects;
+import java.util.Optional;
 
 public abstract sealed class Variable permits AnyDataVariable, NodeVariable {
         private final String explicitName;
@@ -19,7 +20,7 @@ public abstract sealed class Variable permits AnyDataVariable, NodeVariable {
                 uniqueName = DnfUtils.generateUniqueName(name);
         }
 
-        public abstract Sort getSort();
+        public abstract Optional<Class<?>> tryGetType();
 
         public String getName() {
                 return explicitName == null ? uniqueName : explicitName;
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AbstractFunctionView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AbstractFunctionView.java
index c0aa35bf..c6f3dd43 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AbstractFunctionView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AbstractFunctionView.java
@@ -7,12 +7,12 @@ package tools.refinery.store.query.view;
 
 import tools.refinery.store.model.Model;
 import tools.refinery.store.query.dnf.FunctionalDependency;
-import tools.refinery.store.query.term.NodeSort;
-import tools.refinery.store.query.term.Sort;
+import tools.refinery.store.query.term.Parameter;
 import tools.refinery.store.representation.Symbol;
 import tools.refinery.store.tuple.Tuple;
 import tools.refinery.store.tuple.Tuple1;
 
+import java.util.Arrays;
 import java.util.List;
 import java.util.Objects;
 import java.util.Set;
@@ -21,10 +21,12 @@ import java.util.stream.IntStream;
 
 public abstract class AbstractFunctionView<T> extends SymbolView<T> {
         private final T defaultValue;
+        private final List<Parameter> parameters;
 
-        protected AbstractFunctionView(Symbol<T> symbol, String name) {
+        protected AbstractFunctionView(Symbol<T> symbol, String name, Parameter outParameter) {
                 super(symbol, name);
                 defaultValue = symbol.defaultValue();
+                parameters = createParameters(symbol.arity(), outParameter);
         }
 
         @Override
@@ -48,8 +50,6 @@ public abstract class AbstractFunctionView<T> extends SymbolView<T> {
                 return !Objects.equals(defaultValue, value);
         }
 
-        protected abstract Sort getForwardMappedValueSort();
-
         protected Object forwardMapValue(Tuple key, T value) {
                 return value;
         }
@@ -85,19 +85,8 @@ public abstract class AbstractFunctionView<T> extends SymbolView<T> {
         }
 
         @Override
-        public int arity() {
-                return getSymbol().arity() + 1;
-        }
-
-        @Override
-        public List<Sort> getSorts() {
-                var sorts = new Sort[arity()];
-                int valueIndex = sorts.length - 1;
-                for (int i = 0; i < valueIndex; i++) {
-                        sorts[i] = NodeSort.INSTANCE;
-                }
-                sorts[valueIndex] = getForwardMappedValueSort();
-                return List.of(sorts);
+        public List<Parameter> getParameters() {
+                return parameters;
         }
 
         @Override
@@ -106,11 +95,18 @@ public abstract class AbstractFunctionView<T> extends SymbolView<T> {
                 if (o == null || getClass() != o.getClass()) return false;
                 if (!super.equals(o)) return false;
                 AbstractFunctionView<?> that = (AbstractFunctionView<?>) o;
-                return Objects.equals(defaultValue, that.defaultValue);
+                return Objects.equals(defaultValue, that.defaultValue) && Objects.equals(parameters, that.parameters);
         }
 
         @Override
         public int hashCode() {
-                return Objects.hash(super.hashCode(), defaultValue);
+                return Objects.hash(super.hashCode(), defaultValue, parameters);
+        }
+
+        private static List<Parameter> createParameters(int symbolArity, Parameter outParameter) {
+                var parameters = new Parameter[symbolArity + 1];
+                Arrays.fill(parameters, Parameter.NODE_IN_OUT);
+                parameters[symbolArity] = outParameter;
+                return List.of(parameters);
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionView.java
index cf946d54..1b89e77c 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/FunctionView.java
@@ -5,21 +5,16 @@
  */
 package tools.refinery.store.query.view;
 
-import tools.refinery.store.query.term.DataSort;
-import tools.refinery.store.query.term.Sort;
+import tools.refinery.store.query.term.Parameter;
+import tools.refinery.store.query.term.ParameterDirection;
 import tools.refinery.store.representation.Symbol;
 
 public final class FunctionView<T> extends AbstractFunctionView<T> {
         public FunctionView(Symbol<T> symbol, String name) {
-                super(symbol, name);
+                super(symbol, name, new Parameter(symbol.valueType(), ParameterDirection.OUT));
         }
 
         public FunctionView(Symbol<T> symbol) {
                 this(symbol, "function");
         }
-
-        @Override
-        protected Sort getForwardMappedValueSort() {
-                return new DataSort<>(getSymbol().valueType());
-        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/NodeFunctionView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/NodeFunctionView.java
index 73c296e0..e9785c67 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/NodeFunctionView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/NodeFunctionView.java
@@ -5,22 +5,16 @@
  */
 package tools.refinery.store.query.view;
 
-import tools.refinery.store.query.term.NodeSort;
-import tools.refinery.store.query.term.Sort;
+import tools.refinery.store.query.term.Parameter;
 import tools.refinery.store.representation.Symbol;
 import tools.refinery.store.tuple.Tuple1;
 
 public final class NodeFunctionView extends AbstractFunctionView<Tuple1> {
         public NodeFunctionView(Symbol<Tuple1> symbol, String name) {
-                super(symbol, name);
+                super(symbol, name, Parameter.NODE_IN_OUT);
         }
 
         public NodeFunctionView(Symbol<Tuple1> symbol) {
                 this(symbol, "function");
         }
-
-        @Override
-        protected Sort getForwardMappedValueSort() {
-                return NodeSort.INSTANCE;
-        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingView.java
index 19862e3a..7e5b7788 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/TuplePreservingView.java
@@ -6,22 +6,26 @@
 package tools.refinery.store.query.view;
 
 import tools.refinery.store.model.Model;
-import tools.refinery.store.query.term.NodeSort;
-import tools.refinery.store.query.term.Sort;
+import tools.refinery.store.query.term.Parameter;
+import tools.refinery.store.representation.Symbol;
 import tools.refinery.store.tuple.Tuple;
 import tools.refinery.store.tuple.Tuple1;
-import tools.refinery.store.representation.Symbol;
 
 import java.util.Arrays;
 import java.util.List;
+import java.util.Objects;
 
 public abstract class TuplePreservingView<T> extends SymbolView<T> {
+        private final List<Parameter> parameters;
+
         protected TuplePreservingView(Symbol<T> symbol, String name) {
                 super(symbol, name);
+                this.parameters = createParameters(symbol.arity());
         }
 
         protected TuplePreservingView(Symbol<T> symbol) {
                 super(symbol);
+                this.parameters = createParameters(symbol.arity());
         }
 
         public Object[] forwardMap(Tuple key) {
@@ -52,14 +56,27 @@ public abstract class TuplePreservingView<T> extends SymbolView<T> {
         }
 
         @Override
-        public int arity() {
-                return this.getSymbol().arity();
+        public List<Parameter> getParameters() {
+                return parameters;
+        }
+
+        @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;
+                TuplePreservingView<?> that = (TuplePreservingView<?>) o;
+                return Objects.equals(parameters, that.parameters);
         }
 
         @Override
-        public List<Sort> getSorts() {
-                var sorts = new Sort[arity()];
-                Arrays.fill(sorts, NodeSort.INSTANCE);
-                return List.of(sorts);
+        public int hashCode() {
+                return Objects.hash(super.hashCode(), parameters);
+        }
+
+        private static List<Parameter> createParameters(int arity) {
+                var parameters = new Parameter[arity];
+                Arrays.fill(parameters, Parameter.NODE_IN_OUT);
+                return List.of(parameters);
         }
 }
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/dnf/DnfBuilderLiteralEliminationTest.java
index 01e2ccf6..4edea401 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/dnf/DnfBuilderLiteralEliminationTest.java
@@ -3,31 +3,36 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.query;
+package tools.refinery.store.query.dnf;
 
 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.NodeVariable;
 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.query.view.SymbolView;
 import tools.refinery.store.representation.Symbol;
 
+import java.util.List;
+
 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;
 
-class DnfBuilderTest {
+class DnfBuilderLiteralEliminationTest {
+        private final Symbol<Boolean> friend = new Symbol<>("friend", 2, Boolean.class, false);
+        private final SymbolView<Boolean> friendView = new KeyOnlyView<>(friend);
+        private final NodeVariable p = Variable.of("p");
+        private final NodeVariable q = Variable.of("q");
+        private final Dnf trueDnf = Dnf.builder().parameter(p).clause().build();
+        private final Dnf falseDnf = Dnf.builder().parameter(p).build();
+
         @Test
         void eliminateTrueTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(BooleanLiteral.TRUE, friendView.call(p, q))
@@ -39,11 +44,6 @@ 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))
@@ -55,11 +55,6 @@ class DnfBuilderTest {
 
         @Test
         void eliminateFalseTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
@@ -76,11 +71,6 @@ class DnfBuilderTest {
                         "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))
@@ -93,11 +83,6 @@ class DnfBuilderTest {
 
         @Test
         void alwaysTrueTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
@@ -110,11 +95,6 @@ class DnfBuilderTest {
 
         @Test
         void alwaysFalseTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q), BooleanLiteral.FALSE)
@@ -126,12 +106,6 @@ class DnfBuilderTest {
 
         @Test
         void eliminateTrueDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var trueDnf = Dnf.builder().parameter(p).clause().build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(trueDnf.call(q), friendView.call(p, q))
@@ -143,12 +117,6 @@ class DnfBuilderTest {
 
         @Test
         void eliminateFalseDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var falseDnf = Dnf.builder().parameter(p).build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
@@ -161,12 +129,6 @@ class DnfBuilderTest {
 
         @Test
         void alwaysTrueDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var trueDnf = Dnf.builder().parameter(p).clause().build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
@@ -179,12 +141,6 @@ class DnfBuilderTest {
 
         @Test
         void alwaysFalseDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var falseDnf = Dnf.builder().parameter(p).build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q), falseDnf.call(q))
@@ -196,12 +152,6 @@ class DnfBuilderTest {
 
         @Test
         void eliminateNotFalseDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var falseDnf = Dnf.builder().parameter(p).build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(not(falseDnf.call(q)), friendView.call(p, q))
@@ -213,12 +163,6 @@ class DnfBuilderTest {
 
         @Test
         void eliminateNotTrueDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var trueDnf = Dnf.builder().parameter(p).clause().build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
@@ -231,12 +175,6 @@ class DnfBuilderTest {
 
         @Test
         void alwaysNotFalseDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var falseDnf = Dnf.builder().parameter(p).build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q))
@@ -249,12 +187,6 @@ class DnfBuilderTest {
 
         @Test
         void alwaysNotTrueDnfTest() {
-                var p = Variable.of("p");
-                var q = Variable.of("q");
-                var friend = new Symbol<>("friend", 2, Boolean.class, false);
-                var friendView = new KeyOnlyView<>(friend);
-                var trueDnf = Dnf.builder().parameter(p).clause().build();
-
                 var actual = Dnf.builder()
                                 .parameters(p, q)
                                 .clause(friendView.call(p, q), not(trueDnf.call(q)))
@@ -263,4 +195,15 @@ class DnfBuilderTest {
 
                 assertThat(actual, structurallyEqualTo(expected));
         }
+
+        @Test
+        void removeDuplicateTest() {
+                var actual = Dnf.of(builder -> builder.clause((p, q) -> List.of(
+                                friendView.call(p, q),
+                                friendView.call(p, q)
+                )));
+                var expected = Dnf.of(builder -> builder.clause((p, q) -> List.of(friendView.call(p, q))));
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
 }
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderVariableUnificationTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderVariableUnificationTest.java
new file mode 100644
index 00000000..a54ad4d6
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfBuilderVariableUnificationTest.java
@@ -0,0 +1,273 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.query.dnf;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.query.view.KeyOnlyView;
+import tools.refinery.store.query.view.SymbolView;
+import tools.refinery.store.representation.Symbol;
+
+import java.util.List;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo;
+
+class DnfBuilderVariableUnificationTest {
+        private final Symbol<Boolean> friend = new Symbol<>("friend", 2, Boolean.class, false);
+        private final Symbol<Boolean> children = new Symbol<>("friend", 2, Boolean.class, false);
+        private final SymbolView<Boolean> friendView = new KeyOnlyView<>(friend);
+        private final SymbolView<Boolean> childrenView = new KeyOnlyView<>(children);
+
+        @Test
+        void equalToParameterTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        builder.clause(q -> List.of(
+                                        friendView.call(p, q),
+                                        p.isEquivalent(q)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        builder.clause(friendView.call(p, p));
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void equalToParameterReverseTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        builder.clause(q -> List.of(
+                                        friendView.call(p, q),
+                                        q.isEquivalent(p)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        builder.clause(friendView.call(p, p));
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void equalQuantifiedTest() {
+                var actual = Dnf.of(builder -> builder.clause((p, q) -> List.of(
+                                friendView.call(p, q),
+                                p.isEquivalent(q)
+                )));
+                var expected = Dnf.of(builder -> builder.clause(p -> List.of(friendView.call(p, p))));
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void equalQuantifiedTransitiveTest() {
+                var actual = Dnf.of(builder -> builder.clause((p, q, r) -> List.of(
+                                friendView.call(p, q),
+                                p.isEquivalent(q),
+                                childrenView.call(p, r),
+                                q.isEquivalent(r)
+                )));
+                var expected = Dnf.of(builder -> builder.clause(p -> List.of(
+                                friendView.call(p, p),
+                                childrenView.call(p, p)
+                )));
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void equalQuantifiedTransitiveRemoveDuplicateTest() {
+                var actual = Dnf.of(builder -> builder.clause((p, q, r) -> List.of(
+                                friendView.call(p, q),
+                                p.isEquivalent(q),
+                                friendView.call(p, r),
+                                q.isEquivalent(r)
+                )));
+                var expected = Dnf.of(builder -> builder.clause(p -> List.of(friendView.call(p, p))));
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parametersEqualTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        friendView.call(p, q),
+                                        p.isEquivalent(q)
+                        );
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        friendView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parametersEqualTransitiveTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        var r = builder.parameter("r");
+                        builder.clause(
+                                        friendView.call(p, q),
+                                        childrenView.call(p, r),
+                                        p.isEquivalent(q),
+                                        r.isEquivalent(q)
+                        );
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        var r = builder.parameter("r");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        r.isEquivalent(p),
+                                        friendView.call(p, p),
+                                        childrenView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parameterAndQuantifiedEqualsTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause((r) -> List.of(
+                                        friendView.call(p, r),
+                                        p.isEquivalent(r),
+                                        childrenView.call(q, r),
+                                        q.isEquivalent(r)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        friendView.call(p, p),
+                                        childrenView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parameterAndQuantifiedEqualsReverseFirstTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause((r) -> List.of(
+                                        friendView.call(p, r),
+                                        r.isEquivalent(p),
+                                        childrenView.call(q, r),
+                                        q.isEquivalent(r)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        friendView.call(p, p),
+                                        childrenView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parameterAndQuantifiedEqualsReverseSecondTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause((r) -> List.of(
+                                        friendView.call(p, r),
+                                        p.isEquivalent(r),
+                                        childrenView.call(q, r),
+                                        r.isEquivalent(q)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        friendView.call(p, p),
+                                        childrenView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parameterAndQuantifiedEqualsReverseBoth() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause((r) -> List.of(
+                                        friendView.call(p, r),
+                                        p.isEquivalent(r),
+                                        childrenView.call(q, r),
+                                        r.isEquivalent(q)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        friendView.call(p, p),
+                                        childrenView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void parameterAndTwoQuantifiedEqualsTest() {
+                var actual = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause((r, s) -> List.of(
+                                        r.isEquivalent(s),
+                                        friendView.call(p, r),
+                                        p.isEquivalent(r),
+                                        childrenView.call(q, s),
+                                        q.isEquivalent(s)
+                        ));
+                });
+                var expected = Dnf.of(builder -> {
+                        var p = builder.parameter("p");
+                        var q = builder.parameter("q");
+                        builder.clause(
+                                        q.isEquivalent(p),
+                                        friendView.call(p, p),
+                                        childrenView.call(p, p)
+                        );
+                });
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToDefinitionStringTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfToDefinitionStringTest.java
index e89ab682..2e93d78a 100644
--- a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToDefinitionStringTest.java
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/dnf/DnfToDefinitionStringTest.java
@@ -3,10 +3,9 @@
  *
  * SPDX-License-Identifier: EPL-2.0
  */
-package tools.refinery.store.query;
+package tools.refinery.store.query.dnf;
 
 import org.junit.jupiter.api.Test;
-import tools.refinery.store.query.dnf.Dnf;
 import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.query.view.KeyOnlyView;
 import tools.refinery.store.representation.Symbol;
@@ -43,7 +42,7 @@ class DnfToDefinitionStringTest {
                 var dnf = Dnf.builder("Example").parameter(p).clause().build();
 
                 assertThat(dnf.toDefinitionString(), is("""
-                                pred Example(p) <->
+                                pred Example(@In p) <->
                                     <empty>.
                                 """));
         }
diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java
index 526832c4..a5b7f85a 100644
--- a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java
+++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java
@@ -35,11 +35,11 @@ class MismatchDescribingDnfEqualityChecker extends DeepDnfEqualityChecker {
                 var inProgress = getInProgress();
                 int size = inProgress.size();
                 if (size <= 1) {
-                        description.appendText("was ").appendText(pair.left().toDefinitionString());
+                        description.appendText("was ").appendText(pair.right().toDefinitionString());
                         return;
                 }
                 var last = inProgress.get(size - 1);
-                description.appendText("expected ").appendText(last.right().toDefinitionString());
+                description.appendText("expected ").appendText(last.left().toDefinitionString());
                 for (int i = size - 2; i >= 0; i--) {
                         description.appendText(" called from ").appendText(inProgress.get(i).left().toString());
                 }
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java
index 594005f1..ac41d170 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/lifting/DnfLifter.java
@@ -12,7 +12,7 @@ import tools.refinery.store.query.dnf.DnfClause;
 import tools.refinery.store.query.literal.CallLiteral;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.Literal;
-import tools.refinery.store.query.term.DataVariable;
+import tools.refinery.store.query.term.NodeVariable;
 import tools.refinery.store.query.term.Variable;
 import tools.refinery.store.reasoning.ReasoningAdapter;
 import tools.refinery.store.reasoning.literal.ModalConstraint;
@@ -21,7 +21,7 @@ import tools.refinery.store.reasoning.literal.PartialLiterals;
 import tools.refinery.store.util.CycleDetectingMapper;
 
 import java.util.ArrayList;
-import java.util.HashSet;
+import java.util.LinkedHashSet;
 import java.util.List;
 
 public class DnfLifter {
@@ -36,10 +36,10 @@ public class DnfLifter {
                 var modality = modalDnf.modality();
                 var dnf = modalDnf.dnf();
                 var builder = Dnf.builder();
-                builder.parameters(dnf.getParameters());
+                builder.symbolicParameters(dnf.getSymbolicParameters());
                 boolean changed = false;
                 for (var clause : dnf.getClauses()) {
-                        if (liftClause(modality, clause, builder)) {
+                        if (liftClause(modality, dnf, clause, builder)) {
                                 changed = true;
                         }
                 }
@@ -49,12 +49,9 @@ public class DnfLifter {
                 return dnf;
         }
 
-        private boolean liftClause(Modality modality, DnfClause clause, DnfBuilder builder) {
+        private boolean liftClause(Modality modality, Dnf originalDnf, DnfClause clause, DnfBuilder builder) {
                 boolean changed = false;
-                var quantifiedVariables = new HashSet<>(clause.boundVariables()
-                                .stream()
-                                .filter(DataVariable.class::isInstance)
-                                .toList());
+                var quantifiedVariables = getQuantifiedDataVariables(originalDnf, clause);
                 var literals = clause.literals();
                 var liftedLiterals = new ArrayList<Literal>(literals.size());
                 for (var literal : literals) {
@@ -81,6 +78,16 @@ public class DnfLifter {
                 return changed || !quantifiedVariables.isEmpty();
         }
 
+        private static LinkedHashSet<Variable> getQuantifiedDataVariables(Dnf originalDnf, DnfClause clause) {
+                var quantifiedVariables = new LinkedHashSet<>(clause.positiveVariables());
+                for (var symbolicParameter : originalDnf.getSymbolicParameters()) {
+                        // The existence of parameters will be checked outside this DNF.
+                        quantifiedVariables.remove(symbolicParameter.getVariable());
+                }
+                quantifiedVariables.removeIf(variable -> !(variable instanceof NodeVariable));
+                return quantifiedVariables;
+        }
+
         @Nullable
         private Variable isExistsLiteralForVariable(Modality modality, Literal literal) {
                 if (literal instanceof CallLiteral callLiteral &&
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java
index 7fa98104..ce557d82 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/literal/ModalConstraint.java
@@ -8,7 +8,7 @@ package tools.refinery.store.reasoning.literal;
 import tools.refinery.store.query.Constraint;
 import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.literal.LiteralReduction;
-import tools.refinery.store.query.term.Sort;
+import tools.refinery.store.query.term.Parameter;
 
 import java.util.List;
 
@@ -21,8 +21,8 @@ public record ModalConstraint(Modality modality, Constraint constraint) implemen
         }
 
         @Override
-        public List<Sort> getSorts() {
-                return constraint.getSorts();
+        public List<Parameter> getParameters() {
+                return constraint.getParameters();
         }
 
         @Override
diff --git a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java
index fc3dc074..1f74ce38 100644
--- a/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java
+++ b/subprojects/store-reasoning/src/main/java/tools/refinery/store/reasoning/representation/PartialRelation.java
@@ -6,8 +6,7 @@
 package tools.refinery.store.reasoning.representation;
 
 import tools.refinery.store.query.Constraint;
-import tools.refinery.store.query.term.NodeSort;
-import tools.refinery.store.query.term.Sort;
+import tools.refinery.store.query.term.Parameter;
 import tools.refinery.store.representation.AbstractDomain;
 import tools.refinery.store.representation.TruthValue;
 import tools.refinery.store.representation.TruthValueDomain;
@@ -32,10 +31,10 @@ public record PartialRelation(String name, int arity) implements PartialSymbol<T
         }
 
         @Override
-        public List<Sort> getSorts() {
-                var sorts = new Sort[arity()];
-                Arrays.fill(sorts, NodeSort.INSTANCE);
-                return List.of(sorts);
+        public List<Parameter> getParameters() {
+                var parameters = new Parameter[arity];
+                Arrays.fill(parameters, Parameter.NODE_IN_OUT);
+                return List.of(parameters);
         }
 
         @Override