feat: Dnf reduction and structural equality

41 files changed, 1236 insertions, 118 deletions

diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
index a49e0625..8c157187 100644
--- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalDnfCallLiteral.java
@@ -2,13 +2,14 @@ package tools.refinery.store.partial.literal;
 
 import tools.refinery.store.query.Dnf;
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.DnfCallLiteral;
 import tools.refinery.store.query.literal.LiteralReduction;
 import tools.refinery.store.query.literal.PolarLiteral;
+import tools.refinery.store.query.substitution.Substitution;
 
 import java.util.List;
-import java.util.Map;
 
 public class ModalDnfCallLiteral extends ModalLiteral<Dnf> implements PolarLiteral<ModalDnfCallLiteral> {
         public ModalDnfCallLiteral(CallPolarity polarity, Modality modality, Dnf target, List<Variable> arguments) {
@@ -20,7 +21,17 @@ public class ModalDnfCallLiteral extends ModalLiteral<Dnf> implements PolarLiter
         }
 
         @Override
-        public ModalDnfCallLiteral substitute(Map<Variable, Variable> substitution) {
+        public Class<Dnf> getTargetType() {
+                return Dnf.class;
+        }
+
+        @Override
+        protected boolean targetEquals(LiteralEqualityHelper helper, Dnf otherTarget) {
+                return helper.dnfEqual(getTarget(), otherTarget);
+        }
+
+        @Override
+        public ModalDnfCallLiteral substitute(Substitution substitution) {
                 return new ModalDnfCallLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution));
         }
 
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
index a1b6c83e..cebe9c9d 100644
--- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalLiteral.java
@@ -2,8 +2,10 @@ package tools.refinery.store.partial.literal;
 
 import tools.refinery.store.query.RelationLike;
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.literal.CallLiteral;
 import tools.refinery.store.query.literal.CallPolarity;
+import tools.refinery.store.query.literal.Literal;
 
 import java.util.List;
 import java.util.Objects;
@@ -26,6 +28,22 @@ public abstract class ModalLiteral<T extends RelationLike> extends CallLiteral<T
         }
 
         @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (!super.equalsWithSubstitution(helper, other)) {
+                        return false;
+                }
+                // If {@link CallLiteral#equalsWithSubstitution(LiteralEqualityHelper, Literal)} has returned {@code true},
+                // we must have the same dynamic type as {@code other}.
+                var otherModalLiteral = (ModalLiteral<?>) other;
+                return modality == otherModalLiteral.modality;
+        }
+
+        @Override
+        protected String targetToString() {
+                return "%s %s".formatted(modality, super.targetToString());
+        }
+
+        @Override
         public boolean equals(Object o) {
                 if (this == o) return true;
                 if (o == null || getClass() != o.getClass()) return false;
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
index dbaa524f..39054f22 100644
--- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/ModalRelationLiteral.java
@@ -4,9 +4,9 @@ import tools.refinery.store.partial.representation.PartialRelation;
 import tools.refinery.store.query.Variable;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.PolarLiteral;
+import tools.refinery.store.query.substitution.Substitution;
 
 import java.util.List;
-import java.util.Map;
 
 public final class ModalRelationLiteral extends ModalLiteral<PartialRelation>
                 implements PolarLiteral<ModalRelationLiteral> {
@@ -15,12 +15,18 @@ public final class ModalRelationLiteral extends ModalLiteral<PartialRelation>
                 super(polarity, modality, target, arguments);
         }
 
+
         public ModalRelationLiteral(Modality modality, PartialRelationLiteral baseLiteral) {
                 super(modality, baseLiteral);
         }
 
         @Override
-        public ModalRelationLiteral substitute(Map<Variable, Variable> substitution) {
+        public Class<PartialRelation> getTargetType() {
+                return PartialRelation.class;
+        }
+
+        @Override
+        public ModalRelationLiteral substitute(Substitution substitution) {
                 return new ModalRelationLiteral(getPolarity(), getModality(), getTarget(), substituteArguments(substitution));
         }
 
diff --git a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
index dc1a1da3..b81d9a3d 100644
--- a/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
+++ b/subprojects/store-partial/src/main/java/tools/refinery/store/partial/literal/PartialRelationLiteral.java
@@ -5,9 +5,9 @@ import tools.refinery.store.query.Variable;
 import tools.refinery.store.query.literal.CallLiteral;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.PolarLiteral;
+import tools.refinery.store.query.substitution.Substitution;
 
 import java.util.List;
-import java.util.Map;
 
 public final class PartialRelationLiteral extends CallLiteral<PartialRelation>
                 implements PolarLiteral<PartialRelationLiteral> {
@@ -16,7 +16,12 @@ public final class PartialRelationLiteral extends CallLiteral<PartialRelation>
         }
 
         @Override
-        public PartialRelationLiteral substitute(Map<Variable, Variable> substitution) {
+        public Class<PartialRelation> getTargetType() {
+                return PartialRelation.class;
+        }
+
+        @Override
+        public PartialRelationLiteral substitute(Substitution substitution) {
                 return new PartialRelationLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
         }
 
diff --git a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
index ad81e28f..5f528328 100644
--- a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
+++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerExampleHierarchyTest.java
@@ -1,6 +1,5 @@
 package tools.refinery.store.partial.translator.typehierarchy;
 
-import org.hamcrest.Matchers;
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
 import tools.refinery.store.partial.representation.PartialRelation;
@@ -61,16 +60,16 @@ class TypeAnalyzerExampleHierarchyTest {
         @Test
         void inferredTypesTest() {
                 assertAll(
-                                () -> assertThat(sut.getUnknownType(), Matchers.is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))),
-                                () -> assertThat(tester.getInferredType(a1), Matchers.is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))),
-                                () -> assertThat(tester.getInferredType(a3), Matchers.is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))),
-                                () -> assertThat(tester.getInferredType(a4), Matchers.is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))),
-                                () -> assertThat(tester.getInferredType(a5), Matchers.is(new InferredType(Set.of(a5), Set.of(), null))),
-                                () -> assertThat(tester.getInferredType(c1), Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
+                                () -> assertThat(sut.getUnknownType(), is(new InferredType(Set.of(), Set.of(c1, c2, c3, c4), null))),
+                                () -> assertThat(tester.getInferredType(a1), is(new InferredType(Set.of(a1, a4), Set.of(c1, c2), c1))),
+                                () -> assertThat(tester.getInferredType(a3), is(new InferredType(Set.of(a3), Set.of(c2, c3), c2))),
+                                () -> assertThat(tester.getInferredType(a4), is(new InferredType(Set.of(a4), Set.of(c1, c2, c4), c1))),
+                                () -> assertThat(tester.getInferredType(a5), is(new InferredType(Set.of(a5), Set.of(), null))),
+                                () -> assertThat(tester.getInferredType(c1), is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
                                 () -> assertThat(tester.getInferredType(c2),
-                                                Matchers.is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))),
-                                () -> assertThat(tester.getInferredType(c3), Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
-                                () -> assertThat(tester.getInferredType(c4), Matchers.is(new InferredType(Set.of(a4, c4), Set.of(c4), c4)))
+                                                is(new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2))),
+                                () -> assertThat(tester.getInferredType(c3), is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
+                                () -> assertThat(tester.getInferredType(c4), is(new InferredType(Set.of(a4, c4), Set.of(c4), c4)))
                 );
         }
 
@@ -80,8 +79,8 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a3Result = tester.getPreservedType(a3);
                 var expected = new InferredType(Set.of(a1, a3, a4, c2), Set.of(c2), c2);
                 assertAll(
-                                () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)),
-                                () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), Matchers.is(expected)),
+                                () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.TRUE), is(expected)),
+                                () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.TRUE), is(expected)),
                                 () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a1Result.asInferredType())),
                                 () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(a3Result.asInferredType())),
                                 () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.TRUE),
@@ -96,19 +95,19 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a4Result = tester.getPreservedType(a4);
                 assertAll(
                                 () -> assertThat(a1Result.merge(a3Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
+                                                is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
                                 () -> assertThat(a3Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
+                                                is(new InferredType(Set.of(a1, a4, c1), Set.of(c1), c1))),
                                 () -> assertThat(a4Result.merge(a3Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
+                                                is(new InferredType(Set.of(a3, c3), Set.of(c3), c3))),
                                 () -> assertThat(a3Result.merge(a4Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))),
+                                                is(new InferredType(Set.of(a4), Set.of(c1, c4), c1))),
                                 () -> assertThat(a1Result.merge(sut.getUnknownType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(), Set.of(c3, c4), null))),
+                                                is(new InferredType(Set.of(), Set.of(c3, c4), null))),
                                 () -> assertThat(a3Result.merge(sut.getUnknownType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(), Set.of(c1, c4), null))),
+                                                is(new InferredType(Set.of(), Set.of(c1, c4), null))),
                                 () -> assertThat(a4Result.merge(sut.getUnknownType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(), Set.of(c3), null)))
+                                                is(new InferredType(Set.of(), Set.of(c3), null)))
                 );
         }
 
@@ -118,8 +117,8 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a4Result = tester.getPreservedType(a4);
                 var expected = new InferredType(Set.of(c1, a1, a4), Set.of(), null);
                 assertAll(
-                                () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected)),
-                                () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), Matchers.is(expected))
+                                () -> assertThat(c1Result.merge(a4Result.asInferredType(), TruthValue.ERROR), is(expected)),
+                                () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.ERROR), is(expected))
                 );
         }
 
@@ -141,9 +140,9 @@ class TypeAnalyzerExampleHierarchyTest {
                 var c3Result = tester.getPreservedType(c3);
                 assertAll(
                                 () -> assertThat(a1Result.merge(c3Result.asInferredType(), TruthValue.TRUE),
-                                                Matchers.is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a3, c3), Set.of(), null))),
                                 () -> assertThat(c3Result.merge(a1Result.asInferredType(), TruthValue.TRUE),
-                                                Matchers.is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null)))
+                                                is(new InferredType(Set.of(a1, a3, a4, c3), Set.of(), null)))
                 );
         }
 
@@ -154,13 +153,13 @@ class TypeAnalyzerExampleHierarchyTest {
                 var c1Result = tester.getPreservedType(c1);
                 assertAll(
                                 () -> assertThat(a4Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a4), Set.of(), null))),
                                 () -> assertThat(a1Result.merge(c1Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
                                 () -> assertThat(a4Result.merge(c1Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a4, c1), Set.of(), null))),
                                 () -> assertThat(a1Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4), Set.of(), null)))
+                                                is(new InferredType(Set.of(a1, a4), Set.of(), null)))
                 );
         }
 
@@ -170,9 +169,9 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a5Result = tester.getPreservedType(a5);
                 assertAll(
                                 () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.TRUE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
                                 () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.TRUE),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null)))
+                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null)))
                 );
         }
 
@@ -194,9 +193,9 @@ class TypeAnalyzerExampleHierarchyTest {
                 var a5Result = tester.getPreservedType(a5);
                 assertAll(
                                 () -> assertThat(c1Result.merge(a5Result.asInferredType(), TruthValue.ERROR),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
                                 () -> assertThat(a5Result.merge(c1Result.asInferredType(), TruthValue.ERROR),
-                                                Matchers.is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
+                                                is(new InferredType(Set.of(a1, a4, a5, c1), Set.of(), null))),
                                 () -> assertThat(a5Result.merge(a5Result.asInferredType(), TruthValue.ERROR),
                                                 is(a5Result.asInferredType()))
                 );
diff --git a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java
index 1aab75bb..02903026 100644
--- a/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java
+++ b/subprojects/store-partial/src/test/java/tools/refinery/store/partial/translator/typehierarchy/TypeAnalyzerTest.java
@@ -1,6 +1,5 @@
 package tools.refinery.store.partial.translator.typehierarchy;
 
-import org.hamcrest.Matchers;
 import org.junit.jupiter.api.Test;
 import tools.refinery.store.partial.representation.PartialRelation;
 import tools.refinery.store.representation.TruthValue;
@@ -137,8 +136,8 @@ class TypeAnalyzerTest {
 
                 var expected = new InferredType(Set.of(c3), Set.of(c1, c2, c3), c3);
                 assertAll(
-                                () -> assertThat(tester.getInferredType(c3), Matchers.is(expected)),
-                                () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), Matchers.is(expected))
+                                () -> assertThat(tester.getInferredType(c3), is(expected)),
+                                () -> assertThat(c3Result.merge(sut.getUnknownType(), TruthValue.TRUE), is(expected))
                 );
         }
 
@@ -162,7 +161,7 @@ class TypeAnalyzerTest {
                 var a1Result = tester.getPreservedType(a1);
 
                 assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2)));
+                                is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c2)));
         }
 
         @Test
@@ -185,7 +184,7 @@ class TypeAnalyzerTest {
                 var a1Result = tester.getPreservedType(a1);
 
                 assertThat(c1Result.merge(a1Result.asInferredType(), TruthValue.FALSE),
-                                Matchers.is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3)));
+                                is(new InferredType(Set.of(a1), Set.of(c2, c3, c4), c3)));
         }
 
         @Test
diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryAdapterImpl.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryAdapterImpl.java
index e5d8e2f6..e0341598 100644
--- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryAdapterImpl.java
+++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryAdapterImpl.java
@@ -8,6 +8,7 @@ import org.eclipse.viatra.query.runtime.matchers.backend.IQueryBackend;
 import org.eclipse.viatra.query.runtime.matchers.backend.IQueryBackendFactory;
 import tools.refinery.store.model.Model;
 import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.EmptyResultSet;
 import tools.refinery.store.query.ResultSet;
 import tools.refinery.store.query.viatra.ViatraModelQueryAdapter;
 
@@ -15,7 +16,7 @@ import java.lang.invoke.MethodHandle;
 import java.lang.invoke.MethodHandles;
 import java.util.Collection;
 import java.util.Collections;
-import java.util.HashMap;
+import java.util.LinkedHashMap;
 import java.util.Map;
 
 public class ViatraModelQueryAdapterImpl implements ViatraModelQueryAdapter {
@@ -51,11 +52,15 @@ public class ViatraModelQueryAdapterImpl implements ViatraModelQueryAdapter {
                 GenericQueryGroup.of(
                                 Collections.<IQuerySpecification<?>>unmodifiableCollection(querySpecifications.values()).stream()
                 ).prepare(queryEngine);
-                resultSets = new HashMap<>(querySpecifications.size());
+                var vacuousQueries = storeAdapter.getVacuousQueries();
+                resultSets = new LinkedHashMap<>(querySpecifications.size() + vacuousQueries.size());
                 for (var entry : querySpecifications.entrySet()) {
                         var matcher = queryEngine.getMatcher(entry.getValue());
                         resultSets.put(entry.getKey(), matcher);
                 }
+                for (var vacuousQuery : vacuousQueries) {
+                        resultSets.put(vacuousQuery, new EmptyResultSet());
+                }
 
                 setUpdatePropagationDelayed(true);
         }
diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryBuilderImpl.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryBuilderImpl.java
index af20033a..13641ace 100644
--- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryBuilderImpl.java
+++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryBuilderImpl.java
@@ -14,14 +14,13 @@ import tools.refinery.store.query.viatra.ViatraModelQueryBuilder;
 import tools.refinery.store.query.viatra.internal.pquery.Dnf2PQuery;
 import tools.refinery.store.query.viatra.internal.pquery.RawPatternMatcher;
 
-import java.util.Collections;
-import java.util.LinkedHashMap;
-import java.util.Map;
+import java.util.*;
 import java.util.function.Function;
 
 public class ViatraModelQueryBuilderImpl extends AbstractModelAdapterBuilder implements ViatraModelQueryBuilder {
         private ViatraQueryEngineOptions.Builder engineOptionsBuilder;
         private final Dnf2PQuery dnf2PQuery = new Dnf2PQuery();
+        private final Set<Dnf> vacuousQueries = new LinkedHashSet<>();
         private final Map<Dnf, IQuerySpecification<RawPatternMatcher>> querySpecifications = new LinkedHashMap<>();
 
         public ViatraModelQueryBuilderImpl(ModelStoreBuilder storeBuilder) {
@@ -64,11 +63,21 @@ public class ViatraModelQueryBuilderImpl extends AbstractModelAdapterBuilder imp
 
         @Override
         public ViatraModelQueryBuilder query(Dnf query) {
-                if (querySpecifications.containsKey(query)) {
-                        throw new IllegalArgumentException("%s was already added to the query engine".formatted(query.name()));
+                if (querySpecifications.containsKey(query) || vacuousQueries.contains(query)) {
+                        // Ignore duplicate queries.
+                        return this;
+                }
+                var reduction = query.getReduction();
+                switch (reduction) {
+                case NOT_REDUCIBLE -> {
+                        var pQuery = dnf2PQuery.translate(query);
+                        querySpecifications.put(query, pQuery.build());
+                }
+                case ALWAYS_FALSE -> vacuousQueries.add(query);
+                case ALWAYS_TRUE -> throw new IllegalArgumentException(
+                                "Query %s is relationally unsafe (it matches every tuple)".formatted(query.name()));
+                default -> throw new IllegalArgumentException("Unknown reduction: " + reduction);
                 }
-                var pQuery = dnf2PQuery.translate(query);
-                querySpecifications.put(query, pQuery.build());
                 return this;
         }
 
@@ -89,6 +98,10 @@ public class ViatraModelQueryBuilderImpl extends AbstractModelAdapterBuilder imp
         public ViatraModelQueryBuilder hint(Dnf dnf, QueryEvaluationHint queryEvaluationHint) {
                 var pQuery = dnf2PQuery.getAlreadyTranslated(dnf);
                 if (pQuery == null) {
+                        if (vacuousQueries.contains(dnf)) {
+                                // Ignore hits for queries that will never be executed by the query engine.
+                                return this;
+                        }
                         throw new IllegalArgumentException(
                                         "Cannot specify hint for %s, because it was not added to the query engine".formatted(dnf.name()));
                 }
@@ -100,7 +113,7 @@ public class ViatraModelQueryBuilderImpl extends AbstractModelAdapterBuilder imp
         public ViatraModelQueryStoreAdapterImpl createStoreAdapter(ModelStore store) {
                 validateSymbols(store);
                 return new ViatraModelQueryStoreAdapterImpl(store, engineOptionsBuilder.build(), dnf2PQuery.getRelationViews(),
-                                Collections.unmodifiableMap(querySpecifications));
+                                Collections.unmodifiableMap(querySpecifications), Collections.unmodifiableSet(vacuousQueries));
         }
 
         private void validateSymbols(ModelStore store) {
diff --git a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryStoreAdapterImpl.java b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryStoreAdapterImpl.java
index 8323118b..00660d0b 100644
--- a/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryStoreAdapterImpl.java
+++ b/subprojects/store-query-viatra/src/main/java/tools/refinery/store/query/viatra/internal/ViatraModelQueryStoreAdapterImpl.java
@@ -10,22 +10,29 @@ import tools.refinery.store.query.viatra.ViatraModelQueryStoreAdapter;
 import tools.refinery.store.query.viatra.internal.pquery.RawPatternMatcher;
 import tools.refinery.store.query.view.AnyRelationView;
 
-import java.util.Collection;
-import java.util.Map;
+import java.util.*;
 
 public class ViatraModelQueryStoreAdapterImpl implements ViatraModelQueryStoreAdapter {
         private final ModelStore store;
         private final ViatraQueryEngineOptions engineOptions;
         private final Map<AnyRelationView, IInputKey> inputKeys;
         private final Map<Dnf, IQuerySpecification<RawPatternMatcher>> querySpecifications;
+        private final Set<Dnf> vacuousQueries;
+        private final Set<Dnf> allQueries;
 
         ViatraModelQueryStoreAdapterImpl(ModelStore store, ViatraQueryEngineOptions engineOptions,
                                                                          Map<AnyRelationView, IInputKey> inputKeys,
-                                                                         Map<Dnf, IQuerySpecification<RawPatternMatcher>> querySpecifications) {
+                                                                         Map<Dnf, IQuerySpecification<RawPatternMatcher>> querySpecifications,
+                                                                         Set<Dnf> vacuousQueries) {
                 this.store = store;
                 this.engineOptions = engineOptions;
                 this.inputKeys = inputKeys;
                 this.querySpecifications = querySpecifications;
+                this.vacuousQueries = vacuousQueries;
+                var mutableAllQueries = new LinkedHashSet<Dnf>(querySpecifications.size() + vacuousQueries.size());
+                mutableAllQueries.addAll(querySpecifications.keySet());
+                mutableAllQueries.addAll(vacuousQueries);
+                this.allQueries = Collections.unmodifiableSet(mutableAllQueries);
         }
 
         @Override
@@ -43,13 +50,17 @@ public class ViatraModelQueryStoreAdapterImpl implements ViatraModelQueryStoreAd
 
         @Override
         public Collection<Dnf> getQueries() {
-                return querySpecifications.keySet();
+                return allQueries;
         }
 
         Map<Dnf, IQuerySpecification<RawPatternMatcher>> getQuerySpecifications() {
                 return querySpecifications;
         }
 
+        Set<Dnf> getVacuousQueries() {
+                return vacuousQueries;
+        }
+
         @Override
         public ViatraQueryEngineOptions getEngineOptions() {
                 return engineOptions;
diff --git a/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/QueryTest.java b/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/QueryTest.java
index 6a3a62e3..54ae70c3 100644
--- a/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/QueryTest.java
+++ b/subprojects/store-query-viatra/src/test/java/tools/refinery/store/query/viatra/QueryTest.java
@@ -17,6 +17,7 @@ import java.util.Set;
 import java.util.stream.Stream;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;
+import static org.junit.jupiter.api.Assertions.assertThrows;
 import static tools.refinery.store.query.literal.Literals.not;
 
 class QueryTest {
@@ -669,6 +670,45 @@ class QueryTest {
                 assertEquals(3, predicateResultSet.countResults());
         }
 
+        @Test
+        void alwaysFalseTest() {
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+
+                var p1 = new Variable("p1");
+                var predicate = Dnf.builder("AlwaysFalse").parameters(p1).build();
+
+                var store = ModelStore.builder()
+                                .symbols(person)
+                                .with(ViatraModelQuery.ADAPTER)
+                                .queries(predicate)
+                                .build();
+
+                var model = store.createEmptyModel();
+                var personInterpretation = model.getInterpretation(person);
+                var queryEngine = model.getAdapter(ModelQuery.ADAPTER);
+                var predicateResultSet = queryEngine.getResultSet(predicate);
+
+                personInterpretation.put(Tuple.of(0), true);
+                personInterpretation.put(Tuple.of(1), true);
+                personInterpretation.put(Tuple.of(2), true);
+
+                queryEngine.flushChanges();
+                assertEquals(0, predicateResultSet.countResults());
+        }
+
+        @Test
+        void alwaysTrueTest() {
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+
+                var p1 = new Variable("p1");
+                var predicate = Dnf.builder("AlwaysTrue").parameters(p1).clause().build();
+
+                var storeBuilder = ModelStore.builder().symbols(person);
+                var queryBuilder = storeBuilder.with(ViatraModelQuery.ADAPTER);
+
+                assertThrows(IllegalArgumentException.class, () -> queryBuilder.queries(predicate));
+        }
+
         static void compareMatchSets(Stream<TupleLike> matchSet, Set<Tuple> expected) {
                 Set<Tuple> translatedMatchSet = new HashSet<>();
                 var iterator = matchSet.iterator();
diff --git a/subprojects/store-query/build.gradle b/subprojects/store-query/build.gradle
index 2b76e608..97761936 100644
--- a/subprojects/store-query/build.gradle
+++ b/subprojects/store-query/build.gradle
@@ -1,7 +1,9 @@
 plugins {
         id 'refinery-java-library'
+        id 'refinery-java-test-fixtures'
 }
 
 dependencies {
         api project(':refinery-store')
+        testFixturesApi libs.hamcrest
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java
index 760b264b..b6744b50 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Dnf.java
@@ -1,5 +1,7 @@
 package tools.refinery.store.query;
 
+import tools.refinery.store.query.equality.DnfEqualityChecker;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.literal.CallPolarity;
 import tools.refinery.store.query.literal.DnfCallLiteral;
 import tools.refinery.store.query.literal.LiteralReduction;
@@ -7,6 +9,8 @@ import tools.refinery.store.query.literal.LiteralReduction;
 import java.util.*;
 
 public final class Dnf implements RelationLike {
+        private static final String INDENTATION = "    ";
+
         private final String name;
 
         private final String uniqueName;
@@ -50,7 +54,11 @@ public final class Dnf implements RelationLike {
 
         @Override
         public String name() {
-                return name;
+                return name == null ? uniqueName : name;
+        }
+
+        public boolean isExplicitlyNamed() {
+                return name == null;
         }
 
         public String getUniqueName() {
@@ -102,6 +110,61 @@ public final class Dnf implements RelationLike {
                 return call(CallPolarity.TRANSITIVE, List.of(left, right));
         }
 
+        public boolean equalsWithSubstitution(DnfEqualityChecker callEqualityChecker, Dnf other) {
+                if (arity() != other.arity()) {
+                        return false;
+                }
+                int numClauses = clauses.size();
+                if (numClauses != other.clauses.size()) {
+                        return false;
+                }
+                for (int i = 0; i < numClauses; i++) {
+                        var literalEqualityHelper = new LiteralEqualityHelper(callEqualityChecker, parameters, other.parameters);
+                        if (!clauses.get(i).equalsWithSubstitution(literalEqualityHelper, other.clauses.get(i))) {
+                                return false;
+                        }
+                }
+                return true;
+        }
+
+        @Override
+        public String toString() {
+                var builder = new StringBuilder();
+                builder.append("pred ").append(name()).append("(");
+                var parameterIterator = parameters.iterator();
+                if (parameterIterator.hasNext()) {
+                        builder.append(parameterIterator.next());
+                        while (parameterIterator.hasNext()) {
+                                builder.append(", ").append(parameterIterator.next());
+                        }
+                }
+                builder.append(") <->");
+                var clauseIterator = clauses.iterator();
+                if (clauseIterator.hasNext()) {
+                        appendClause(clauseIterator.next(), builder);
+                        while (clauseIterator.hasNext()) {
+                                builder.append("\n;");
+                                appendClause(clauseIterator.next(), builder);
+                        }
+                } else {
+                        builder.append("\n").append(INDENTATION).append("<no clauses>");
+                }
+                builder.append(".\n");
+                return builder.toString();
+        }
+
+        private static void appendClause(DnfClause clause, StringBuilder builder) {
+                var iterator = clause.literals().iterator();
+                if (!iterator.hasNext()) {
+                        builder.append("\n").append(INDENTATION).append("<empty>");
+                        return;
+                }
+                builder.append("\n").append(INDENTATION).append(iterator.next());
+                while (iterator.hasNext()) {
+                        builder.append(",\n").append(INDENTATION).append(iterator.next());
+                }
+        }
+
         public static DnfBuilder builder() {
                 return builder(null);
         }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java
index b18b5177..ca47e979 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfBuilder.java
@@ -52,7 +52,8 @@ public class DnfBuilder {
         }
 
         public DnfBuilder clause(Collection<Literal> literals) {
-                var filteredLiterals = new ArrayList<Literal>(literals.size());
+                // 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) {
@@ -65,10 +66,10 @@ public class DnfBuilder {
                                 // Clauses with {@code false} literals can be omitted entirely.
                                 return this;
                         }
-                        default -> throw new IllegalStateException("Invalid reduction %s".formatted(reduction));
+                        default -> throw new IllegalArgumentException("Invalid reduction: " + reduction);
                         }
                 }
-                clauses.add(Collections.unmodifiableList(filteredLiterals));
+                clauses.add(List.copyOf(filteredLiterals));
                 return this;
         }
 
@@ -77,10 +78,7 @@ public class DnfBuilder {
         }
 
         public DnfBuilder clauses(DnfClause... clauses) {
-                for (var clause : clauses) {
-                        this.clause(clause);
-                }
-                return this;
+                return clauses(List.of(clauses));
         }
 
         public DnfBuilder clauses(Collection<DnfClause> clauses) {
@@ -91,18 +89,27 @@ public class DnfBuilder {
         }
 
         public Dnf build() {
+                var postProcessedClauses = postProcessClauses();
+                return new Dnf(name, Collections.unmodifiableList(parameters),
+                                Collections.unmodifiableList(functionalDependencies),
+                                Collections.unmodifiableList(postProcessedClauses));
+        }
+
+        private List<DnfClause> postProcessClauses() {
                 var postProcessedClauses = new ArrayList<DnfClause>(clauses.size());
-                for (var constraints : clauses) {
+                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 constraint : constraints) {
+                        for (var constraint : literals) {
                                 constraint.collectAllVariables(variables);
                         }
                         parameters.forEach(variables::remove);
                         postProcessedClauses.add(new DnfClause(Collections.unmodifiableSet(variables),
-                                        Collections.unmodifiableList(constraints)));
+                                        Collections.unmodifiableList(literals)));
                 }
-                return new Dnf(name, Collections.unmodifiableList(parameters),
-                                Collections.unmodifiableList(functionalDependencies),
-                                Collections.unmodifiableList(postProcessedClauses));
+                return postProcessedClauses;
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java
index 2ba6becc..c6e8b8c9 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfClause.java
@@ -1,9 +1,22 @@
 package tools.refinery.store.query;
 
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
 import tools.refinery.store.query.literal.Literal;
 
 import java.util.List;
 import java.util.Set;
 
 public record DnfClause(Set<Variable> quantifiedVariables, List<Literal> literals) {
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, DnfClause other) {
+                int size = literals.size();
+                if (size != other.literals.size()) {
+                        return false;
+                }
+                for (int i = 0; i < size; i++) {
+                        if (!literals.get(i).equalsWithSubstitution(helper, other.literals.get(i))) {
+                                return false;
+                        }
+                }
+                return true;
+        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java
index 17564d43..c7a2849c 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/DnfUtils.java
@@ -1,6 +1,5 @@
 package tools.refinery.store.query;
 
-import java.util.Map;
 import java.util.UUID;
 
 public final class DnfUtils {
@@ -17,8 +16,4 @@ public final class DnfUtils {
                         return originalName + uniqueString;
                 }
         }
-
-        public static Variable maybeSubstitute(Variable variable, Map<Variable, Variable> substitution) {
-                return substitution.getOrDefault(variable, variable);
-        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java
new file mode 100644
index 00000000..a01a5a2f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/EmptyResultSet.java
@@ -0,0 +1,49 @@
+package tools.refinery.store.query;
+
+import tools.refinery.store.tuple.Tuple;
+import tools.refinery.store.tuple.TupleLike;
+
+import java.util.Optional;
+import java.util.stream.Stream;
+
+public class EmptyResultSet implements ResultSet {
+        @Override
+        public boolean hasResult() {
+                return false;
+        }
+
+        @Override
+        public boolean hasResult(Tuple parameters) {
+                return false;
+        }
+
+        @Override
+        public Optional<TupleLike> oneResult() {
+                return Optional.empty();
+        }
+
+        @Override
+        public Optional<TupleLike> oneResult(Tuple parameters) {
+                return Optional.empty();
+        }
+
+        @Override
+        public Stream<TupleLike> allResults() {
+                return Stream.of();
+        }
+
+        @Override
+        public Stream<TupleLike> allResults(Tuple parameters) {
+                return Stream.of();
+        }
+
+        @Override
+        public int countResults() {
+                return 0;
+        }
+
+        @Override
+        public int countResults(Tuple parameters) {
+                return 0;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java
index 2eb87649..d0e0dead 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/Variable.java
@@ -20,15 +20,15 @@ public class Variable {
 
         }
         public String getName() {
-                return name;
+                return name == null ? uniqueName : name;
         }
 
-        public String getUniqueName() {
-                return uniqueName;
+        public boolean isExplicitlyNamed() {
+                return name != null;
         }
 
-        public boolean isNamed() {
-                return name != null;
+        public String getUniqueName() {
+                return uniqueName;
         }
 
         public ConstantLiteral isConstant(int value) {
@@ -44,6 +44,11 @@ public class Variable {
         }
 
         @Override
+        public String toString() {
+                return getName();
+        }
+
+        @Override
         public boolean equals(Object o) {
                 if (this == o) return true;
                 if (o == null || getClass() != o.getClass()) return false;
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java
new file mode 100644
index 00000000..ebd7f5b0
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DeepDnfEqualityChecker.java
@@ -0,0 +1,31 @@
+package tools.refinery.store.query.equality;
+
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.util.CycleDetectingMapper;
+
+import java.util.List;
+
+public class DeepDnfEqualityChecker implements DnfEqualityChecker {
+        private final CycleDetectingMapper<Pair, Boolean> mapper = new CycleDetectingMapper<>(Pair::toString,
+                        this::doCheckEqual);
+
+        @Override
+        public boolean dnfEqual(Dnf left, Dnf right) {
+                return mapper.map(new Pair(left, right));
+        }
+
+        protected boolean doCheckEqual(Pair pair) {
+                return pair.left.equalsWithSubstitution(this, pair.right);
+        }
+
+        protected List<Pair> getInProgress() {
+                return mapper.getInProgress();
+        }
+
+        protected record Pair(Dnf left, Dnf right) {
+                @Override
+                public String toString() {
+                        return "(%s, %s)".formatted(left.name(), right.name());
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java
new file mode 100644
index 00000000..eb77de17
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/DnfEqualityChecker.java
@@ -0,0 +1,8 @@
+package tools.refinery.store.query.equality;
+
+import tools.refinery.store.query.Dnf;
+
+@FunctionalInterface
+public interface DnfEqualityChecker {
+        boolean dnfEqual(Dnf left, Dnf right);
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java
new file mode 100644
index 00000000..23f1acc7
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/equality/LiteralEqualityHelper.java
@@ -0,0 +1,48 @@
+package tools.refinery.store.query.equality;
+
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.Variable;
+
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+public class LiteralEqualityHelper {
+        private final DnfEqualityChecker dnfEqualityChecker;
+        private final Map<Variable, Variable> leftToRight;
+        private final Map<Variable, Variable> rightToLeft;
+
+        public LiteralEqualityHelper(DnfEqualityChecker dnfEqualityChecker, List<Variable> leftParameters,
+                                                                 List<Variable> rightParameters) {
+                this.dnfEqualityChecker = dnfEqualityChecker;
+                var arity = leftParameters.size();
+                if (arity != rightParameters.size()) {
+                        throw new IllegalArgumentException("Parameter lists have unequal length");
+                }
+                leftToRight = new HashMap<>(arity);
+                rightToLeft = new HashMap<>(arity);
+                for (int i = 0; i < arity; i++) {
+                        if (!variableEqual(leftParameters.get(i), rightParameters.get(i))) {
+                                throw new IllegalArgumentException("Parameter lists cannot be unified: duplicate parameter " + i);
+                        }
+                }
+        }
+
+        public boolean dnfEqual(Dnf left, Dnf right) {
+                return dnfEqualityChecker.dnfEqual(left, right);
+        }
+
+        public boolean variableEqual(Variable left, Variable right) {
+                if (checkMapping(leftToRight, left, right) && checkMapping(rightToLeft, right, left)) {
+                        leftToRight.put(left, right);
+                        rightToLeft.put(right, left);
+                        return true;
+                }
+                return false;
+        }
+
+        private static boolean checkMapping(Map<Variable, Variable> map, Variable key, Variable expectedValue) {
+                var currentValue = map.get(key);
+                return currentValue == null || currentValue.equals(expectedValue);
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
index fd2f1eec..6d751be8 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/BooleanLiteral.java
@@ -1,18 +1,19 @@
 package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
 
-import java.util.Map;
 import java.util.Set;
 
-public class BooleanLiteral implements Literal {
-        public static final BooleanLiteral TRUE = new BooleanLiteral(LiteralReduction.ALWAYS_TRUE);
-        public static final BooleanLiteral FALSE = new BooleanLiteral(LiteralReduction.ALWAYS_FALSE);
+public enum BooleanLiteral implements PolarLiteral<BooleanLiteral> {
+        TRUE(true),
+        FALSE(false);
 
-        private final LiteralReduction reduction;
+        private final boolean value;
 
-        private BooleanLiteral(LiteralReduction reduction) {
-                this.reduction = reduction;
+        BooleanLiteral(boolean value) {
+                this.value = value;
         }
 
         @Override
@@ -21,14 +22,29 @@ public class BooleanLiteral implements Literal {
         }
 
         @Override
-        public Literal substitute(Map<Variable, Variable> substitution) {
+        public Literal substitute(Substitution substitution) {
                 // No variables to substitute.
                 return this;
         }
 
         @Override
         public LiteralReduction getReduction() {
-                return reduction;
+                return value ? LiteralReduction.ALWAYS_TRUE : LiteralReduction.ALWAYS_FALSE;
+        }
+
+        @Override
+        public BooleanLiteral negate() {
+                return fromBoolean(!value);
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                return equals(other);
+        }
+
+        @Override
+        public String toString() {
+                return Boolean.toString(value);
         }
 
         public static BooleanLiteral fromBoolean(boolean value) {
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 5e1ae94d..091b4e04 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/CallLiteral.java
@@ -1,11 +1,11 @@
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.DnfUtils;
 import tools.refinery.store.query.RelationLike;
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
 
 import java.util.List;
-import java.util.Map;
 import java.util.Objects;
 import java.util.Set;
 
@@ -31,6 +31,8 @@ public abstract class CallLiteral<T extends RelationLike> implements Literal {
                 return polarity;
         }
 
+        public abstract Class<T> getTargetType();
+
         public T getTarget() {
                 return target;
         }
@@ -46,8 +48,44 @@ public abstract class CallLiteral<T extends RelationLike> implements Literal {
                 }
         }
 
-        protected List<Variable> substituteArguments(Map<Variable, Variable> substitution) {
-                return arguments.stream().map(variable -> DnfUtils.maybeSubstitute(variable, substitution)).toList();
+        protected List<Variable> substituteArguments(Substitution substitution) {
+                return arguments.stream().map(substitution::getSubstitute).toList();
+        }
+
+        /**
+         * Compares the target of this call literal with another object.
+         *
+         * @param helper      Equality helper for comparing {@link Variable} and {@link tools.refinery.store.query.Dnf}
+         *                    instances.
+         * @param otherTarget The object to compare the target to.
+         * @return {@code true} if {@code otherTarget} is equal to the return value of {@link #getTarget()} according to
+         * {@code helper}, {@code false} otherwise.
+         */
+        protected boolean targetEquals(LiteralEqualityHelper helper, T otherTarget) {
+                return target.equals(otherTarget);
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (other.getClass() != getClass()) {
+                        return false;
+                }
+                var otherCallLiteral = (CallLiteral<?>) other;
+                if (getTargetType() != otherCallLiteral.getTargetType() || polarity != otherCallLiteral.polarity) {
+                        return false;
+                }
+                var arity = arguments.size();
+                if (arity != otherCallLiteral.arguments.size()) {
+                        return false;
+                }
+                for (int i = 0; i < arity; i++) {
+                        if (!helper.variableEqual(arguments.get(i), otherCallLiteral.arguments.get(i))) {
+                                return false;
+                        }
+                }
+                @SuppressWarnings("unchecked")
+                var otherTarget = (T) otherCallLiteral.target;
+                return targetEquals(helper, otherTarget);
         }
 
         @Override
@@ -63,4 +101,33 @@ public abstract class CallLiteral<T extends RelationLike> implements Literal {
         public int hashCode() {
                 return Objects.hash(polarity, target, arguments);
         }
+
+        protected String targetToString() {
+                return "@%s %s".formatted(getTargetType().getSimpleName(), target.name());
+        }
+
+        @Override
+        public String toString() {
+                var builder = new StringBuilder();
+                if (!polarity.isPositive()) {
+                        builder.append("!(");
+                }
+                builder.append(targetToString());
+                if (polarity.isTransitive()) {
+                        builder.append("+");
+                }
+                builder.append("(");
+                var argumentIterator = arguments.iterator();
+                if (argumentIterator.hasNext()) {
+                        builder.append(argumentIterator.next());
+                        while (argumentIterator.hasNext()) {
+                                builder.append(", ").append(argumentIterator.next());
+                        }
+                }
+                builder.append(")");
+                if (!polarity.isPositive()) {
+                        builder.append(")");
+                }
+                return builder.toString();
+        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
index 746d23af..d01c7d20 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/ConstantLiteral.java
@@ -1,9 +1,9 @@
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.DnfUtils;
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
 
-import java.util.Map;
 import java.util.Set;
 
 public record ConstantLiteral(Variable variable, int nodeId) implements Literal {
@@ -13,7 +13,21 @@ public record ConstantLiteral(Variable variable, int nodeId) implements Literal
         }
 
         @Override
-        public ConstantLiteral substitute(Map<Variable, Variable> substitution) {
-                return new ConstantLiteral(DnfUtils.maybeSubstitute(variable, substitution), nodeId);
+        public ConstantLiteral substitute(Substitution substitution) {
+                return new ConstantLiteral(substitution.getSubstitute(variable), nodeId);
+        }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (other.getClass() != getClass()) {
+                        return false;
+                }
+                var otherConstantLiteral = (ConstantLiteral) other;
+                return helper.variableEqual(variable, otherConstantLiteral.variable) && nodeId == otherConstantLiteral.nodeId;
+        }
+
+        @Override
+        public String toString() {
+                return "%s === @Constant %d".formatted(variable, nodeId);
         }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java
index de6c6005..27917265 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/DnfCallLiteral.java
@@ -2,9 +2,10 @@ package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.Dnf;
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
 
 import java.util.List;
-import java.util.Map;
 
 public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiteral<DnfCallLiteral> {
         public DnfCallLiteral(CallPolarity polarity, Dnf target, List<Variable> arguments) {
@@ -12,7 +13,12 @@ public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiter
         }
 
         @Override
-        public DnfCallLiteral substitute(Map<Variable, Variable> substitution) {
+        public Class<Dnf> getTargetType() {
+                return Dnf.class;
+        }
+
+        @Override
+        public DnfCallLiteral substitute(Substitution substitution) {
                 return new DnfCallLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
         }
 
@@ -26,4 +32,9 @@ public final class DnfCallLiteral extends CallLiteral<Dnf> implements PolarLiter
                 var dnfReduction = getTarget().getReduction();
                 return getPolarity().isPositive() ? dnfReduction : dnfReduction.negate();
         }
+
+        @Override
+        protected boolean targetEquals(LiteralEqualityHelper helper, Dnf otherTarget) {
+                return helper.dnfEqual(getTarget(), otherTarget);
+        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
index f30179b2..61c753c3 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/EquivalenceLiteral.java
@@ -1,9 +1,9 @@
 package tools.refinery.store.query.literal;
 
-import tools.refinery.store.query.DnfUtils;
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
 
-import java.util.Map;
 import java.util.Set;
 
 public record EquivalenceLiteral(boolean positive, Variable left, Variable right)
@@ -20,9 +20,8 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right
         }
 
         @Override
-        public EquivalenceLiteral substitute(Map<Variable, Variable> substitution) {
-                return new EquivalenceLiteral(positive, DnfUtils.maybeSubstitute(left, substitution),
-                                DnfUtils.maybeSubstitute(right, substitution));
+        public EquivalenceLiteral substitute(Substitution substitution) {
+                return new EquivalenceLiteral(positive, substitution.getSubstitute(left), substitution.getSubstitute(right));
         }
 
         @Override
@@ -32,4 +31,19 @@ public record EquivalenceLiteral(boolean positive, Variable left, Variable right
                 }
                 return LiteralReduction.NOT_REDUCIBLE;
         }
+
+        @Override
+        public boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other) {
+                if (other.getClass() != getClass()) {
+                        return false;
+                }
+                var otherEquivalenceLiteral = (EquivalenceLiteral) other;
+                return helper.variableEqual(left, otherEquivalenceLiteral.left) && helper.variableEqual(right,
+                                otherEquivalenceLiteral.right);
+        }
+
+        @Override
+        public String toString() {
+                return "%s %s %s".formatted(left, positive ? "===" : "!==", right);
+        }
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
index a6893acf..ddd91775 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/Literal.java
@@ -1,16 +1,20 @@
 package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.equality.LiteralEqualityHelper;
+import tools.refinery.store.query.substitution.Substitution;
 
-import java.util.Map;
 import java.util.Set;
 
 public interface Literal {
         void collectAllVariables(Set<Variable> variables);
 
-        Literal substitute(Map<Variable, Variable> substitution);
+        Literal substitute(Substitution substitution);
 
         default LiteralReduction getReduction() {
                 return LiteralReduction.NOT_REDUCIBLE;
         }
+
+        @SuppressWarnings("BooleanMethodIsAlwaysInverted")
+        boolean equalsWithSubstitution(LiteralEqualityHelper helper, Literal other);
 }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java
index 4718b550..fb8b3332 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/literal/RelationViewLiteral.java
@@ -1,10 +1,10 @@
 package tools.refinery.store.query.literal;
 
 import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.substitution.Substitution;
 import tools.refinery.store.query.view.AnyRelationView;
 
 import java.util.List;
-import java.util.Map;
 
 public final class RelationViewLiteral extends CallLiteral<AnyRelationView>
                 implements PolarLiteral<RelationViewLiteral> {
@@ -13,7 +13,18 @@ public final class RelationViewLiteral extends CallLiteral<AnyRelationView>
         }
 
         @Override
-        public RelationViewLiteral substitute(Map<Variable, Variable> substitution) {
+        public Class<AnyRelationView> getTargetType() {
+                return AnyRelationView.class;
+        }
+
+        @Override
+        protected String targetToString() {
+                var target = getTarget();
+                return "@RelationView(\"%s\") %s".formatted(target.getViewName(), target.getSymbol().name());
+        }
+
+        @Override
+        public RelationViewLiteral substitute(Substitution substitution) {
                 return new RelationViewLiteral(getPolarity(), getTarget(), substituteArguments(substitution));
         }
 
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java
new file mode 100644
index 00000000..ffc65047
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/MapBasedSubstitution.java
@@ -0,0 +1,13 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.Variable;
+
+import java.util.Map;
+
+public record MapBasedSubstitution(Map<Variable, Variable> map, Substitution fallback) implements Substitution {
+        @Override
+        public Variable getSubstitute(Variable variable) {
+                var value = map.get(variable);
+                return value == null ? fallback.getSubstitute(variable) : value;
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java
new file mode 100644
index 00000000..54d18a3f
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/RenewingSubstitution.java
@@ -0,0 +1,19 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.Variable;
+
+import java.util.HashMap;
+import java.util.Map;
+
+public class RenewingSubstitution implements Substitution {
+        private final Map<Variable, Variable> alreadyRenewed = new HashMap<>();
+
+        @Override
+        public Variable getSubstitute(Variable variable) {
+                return alreadyRenewed.computeIfAbsent(variable, RenewingSubstitution::renew);
+        }
+
+        private static Variable renew(Variable variable) {
+                return variable.isExplicitlyNamed() ? new Variable(variable.getName()) : new Variable();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java
new file mode 100644
index 00000000..d33ad6fb
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/StatelessSubstitution.java
@@ -0,0 +1,18 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.Variable;
+
+public enum StatelessSubstitution implements Substitution {
+        FAILING {
+                @Override
+                public Variable getSubstitute(Variable variable) {
+                        throw new IllegalArgumentException("No substitute for " + variable);
+                }
+        },
+        IDENTITY {
+                @Override
+                public Variable getSubstitute(Variable variable) {
+                        return variable;
+                }
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java
new file mode 100644
index 00000000..9d086bf5
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitution.java
@@ -0,0 +1,8 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.Variable;
+
+@FunctionalInterface
+public interface Substitution {
+        Variable getSubstitute(Variable variable);
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java
new file mode 100644
index 00000000..26cf1a20
--- /dev/null
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/substitution/Substitutions.java
@@ -0,0 +1,27 @@
+package tools.refinery.store.query.substitution;
+
+import tools.refinery.store.query.Variable;
+
+import java.util.Map;
+
+public final class Substitutions {
+        private Substitutions() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiate directly");
+        }
+
+        public static Substitution total(Map<Variable, Variable> map) {
+                return new MapBasedSubstitution(map, StatelessSubstitution.FAILING);
+        }
+
+        public static Substitution partial(Map<Variable, Variable> map) {
+                return new MapBasedSubstitution(map, StatelessSubstitution.IDENTITY);
+        }
+
+        public static Substitution renewing(Map<Variable, Variable> map) {
+                return new MapBasedSubstitution(map, renewing());
+        }
+
+        public static Substitution renewing() {
+                return new RenewingSubstitution();
+        }
+}
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java
index 328cde3a..bc3ac1ea 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/AnyRelationView.java
@@ -10,6 +10,8 @@ import java.util.Set;
 public sealed interface AnyRelationView extends RelationLike permits RelationView {
         AnySymbol getSymbol();
 
+        String getViewName();
+
         default Set<FunctionalDependency<Integer>> getFunctionalDependencies() {
                 return Set.of();
         }
diff --git a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java
index 2714a8c5..ea9fd5e2 100644
--- a/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java
+++ b/subprojects/store-query/src/main/java/tools/refinery/store/query/view/RelationView.java
@@ -21,11 +21,11 @@ import java.util.UUID;
 public abstract non-sealed class RelationView<T> implements AnyRelationView {
         private final Symbol<T> symbol;
 
-        private final String name;
+        private final String viewName;
 
-        protected RelationView(Symbol<T> symbol, String name) {
+        protected RelationView(Symbol<T> symbol, String viewName) {
                 this.symbol = symbol;
-                this.name = name;
+                this.viewName = viewName;
         }
 
         protected RelationView(Symbol<T> representation) {
@@ -38,8 +38,13 @@ public abstract non-sealed class RelationView<T> implements AnyRelationView {
         }
 
         @Override
+        public String getViewName() {
+                return viewName;
+        }
+
+        @Override
         public String name() {
-                return symbol.name() + "#" + name;
+                return symbol.name() + "#" + viewName;
         }
 
         public abstract boolean filter(Tuple key, T value);
@@ -72,11 +77,11 @@ public abstract non-sealed class RelationView<T> implements AnyRelationView {
                 if (this == o) return true;
                 if (o == null || getClass() != o.getClass()) return false;
                 RelationView<?> that = (RelationView<?>) o;
-                return Objects.equals(symbol, that.symbol) && Objects.equals(name, that.name);
+                return Objects.equals(symbol, that.symbol) && Objects.equals(viewName, that.viewName);
         }
 
         @Override
         public int hashCode() {
-                return Objects.hash(symbol, name);
+                return Objects.hash(symbol, viewName);
         }
 }
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java
new file mode 100644
index 00000000..e6701fe3
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfBuilderTest.java
@@ -0,0 +1,218 @@
+package tools.refinery.store.query;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.query.literal.BooleanLiteral;
+import tools.refinery.store.query.view.KeyOnlyRelationView;
+import tools.refinery.store.representation.Symbol;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static tools.refinery.store.query.literal.Literals.not;
+import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo;
+
+class DnfBuilderTest {
+        @Test
+        void eliminateTrueTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(BooleanLiteral.TRUE, friendView.call(p, q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateFalseTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(friendView.call(q, p), BooleanLiteral.FALSE)
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysTrueTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(BooleanLiteral.TRUE)
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause().build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysFalseTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q), BooleanLiteral.FALSE)
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateTrueDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var trueDnf = Dnf.builder().parameter(p).clause().build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(trueDnf.call(q), friendView.call(p, q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateFalseDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var falseDnf = Dnf.builder().parameter(p).build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(friendView.call(q, p), falseDnf.call(q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysTrueDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var trueDnf = Dnf.builder().parameter(p).clause().build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(trueDnf.call(q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause().build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysFalseDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var falseDnf = Dnf.builder().parameter(p).build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q), falseDnf.call(q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateNotFalseDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var falseDnf = Dnf.builder().parameter(p).build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(not(falseDnf.call(q)), friendView.call(p, q))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void eliminateNotTrueDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var trueDnf = Dnf.builder().parameter(p).clause().build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(friendView.call(q, p), not(trueDnf.call(q)))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysNotFalseDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var falseDnf = Dnf.builder().parameter(p).build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q))
+                                .clause(not(falseDnf.call(q)))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).clause().build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void alwaysNotTrueDnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var trueDnf = Dnf.builder().parameter(p).clause().build();
+
+                var actual = Dnf.builder()
+                                .parameters(p, q)
+                                .clause(friendView.call(p, q), not(trueDnf.call(q)))
+                                .build();
+                var expected = Dnf.builder().parameters(p, q).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToStringTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToStringTest.java
new file mode 100644
index 00000000..e6e4bef3
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/DnfToStringTest.java
@@ -0,0 +1,172 @@
+package tools.refinery.store.query;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.query.view.KeyOnlyRelationView;
+import tools.refinery.store.representation.Symbol;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.is;
+import static tools.refinery.store.query.literal.Literals.not;
+
+class DnfToStringTest {
+        @Test
+        void noClausesTest() {
+                var p = new Variable("p");
+                var dnf = Dnf.builder("Example").parameter(p).build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    <no clauses>.
+                                """));
+        }
+
+        @Test
+        void noParametersTest() {
+                var dnf = Dnf.builder("Example").build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example() <->
+                                    <no clauses>.
+                                """));
+        }
+
+        @Test
+        void emptyClauseTest() {
+                var p = new Variable("p");
+                var dnf = Dnf.builder("Example").parameter(p).clause().build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    <empty>.
+                                """));
+        }
+
+        @Test
+        void relationViewPositiveTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example").parameter(p).clause(friendView.call(p, q)).build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") friend(p, q).
+                                """));
+        }
+
+        @Test
+        void relationViewNegativeTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example").parameter(p).clause(not(friendView.call(p, q))).build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    !(@RelationView("key") friend(p, q)).
+                                """));
+        }
+
+        @Test
+        void relationViewTransitiveTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example").parameter(p).clause(friendView.callTransitive(p, q)).build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") friend+(p, q).
+                                """));
+        }
+
+        @Test
+        void multipleParametersTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example").parameters(p, q).clause(friendView.call(p, q)).build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p, q) <->
+                                    @RelationView("key") friend(p, q).
+                                """));
+        }
+
+        @Test
+        void multipleLiteralsTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var person = new Symbol<>("person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example")
+                                .parameter(p)
+                                .clause(
+                                                personView.call(p),
+                                                personView.call(q),
+                                                friendView.call(p, q)
+                                )
+                                .build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") person(p),
+                                    @RelationView("key") person(q),
+                                    @RelationView("key") friend(p, q).
+                                """));
+        }
+
+        @Test
+        void multipleClausesTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var dnf = Dnf.builder("Example")
+                                .parameter(p)
+                                .clause(friendView.call(p, q))
+                                .clause(friendView.call(q, p))
+                                .build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") friend(p, q)
+                                ;
+                                    @RelationView("key") friend(q, p).
+                                """));
+        }
+
+        @Test
+        void dnfTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var r = new Variable("r");
+                var s = new Variable("s");
+                var person = new Symbol<>("person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+                var friend = new Symbol<>("friend", 2, Boolean.class, false);
+                var friendView = new KeyOnlyRelationView<>(friend);
+                var called  = Dnf.builder("Called").parameters(r, s).clause(friendView.call(r, s)).build();
+                var dnf = Dnf.builder("Example")
+                                .parameter(p)
+                                .clause(
+                                                personView.call(p),
+                                                personView.call(q),
+                                                not(called.call(p, q))
+                                )
+                                .build();
+
+                assertThat(dnf.toString(), is("""
+                                pred Example(p) <->
+                                    @RelationView("key") person(p),
+                                    @RelationView("key") person(q),
+                                    !(@Dnf Called(p, q)).
+                                """));
+        }
+}
diff --git a/subprojects/store-query/src/test/java/tools/refinery/store/query/tests/StructurallyEqualToTest.java b/subprojects/store-query/src/test/java/tools/refinery/store/query/tests/StructurallyEqualToTest.java
new file mode 100644
index 00000000..0cda22df
--- /dev/null
+++ b/subprojects/store-query/src/test/java/tools/refinery/store/query/tests/StructurallyEqualToTest.java
@@ -0,0 +1,77 @@
+package tools.refinery.store.query.tests;
+
+import org.junit.jupiter.api.Test;
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.Variable;
+import tools.refinery.store.query.view.KeyOnlyRelationView;
+import tools.refinery.store.representation.Symbol;
+
+import static org.hamcrest.CoreMatchers.containsString;
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.junit.jupiter.api.Assertions.assertThrows;
+import static tools.refinery.store.query.tests.QueryMatchers.structurallyEqualTo;
+
+class StructurallyEqualToTest {
+        @Test
+        void flatEqualsTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+
+                var expected = Dnf.builder("Expected").parameters(q).clause(personView.call(q)).build();
+                var actual = Dnf.builder("Actual").parameters(p).clause(personView.call(p)).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void flatNotEqualsTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+
+                var expected = Dnf.builder("Expected").parameters(q).clause(personView.call(q)).build();
+                var actual = Dnf.builder("Actual").parameters(p).clause(personView.call(q)).build();
+
+                var assertion = structurallyEqualTo(expected);
+                assertThrows(AssertionError.class, () -> assertThat(actual, assertion));
+        }
+
+        @Test
+        void deepEqualsTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+
+                var expected = Dnf.builder("Expected").parameters(q).clause(
+                                Dnf.builder("Expected2").parameters(p).clause(personView.call(p)).build().call(q)
+                ).build();
+                var actual = Dnf.builder("Actual").parameters(q).clause(
+                                Dnf.builder("Actual2").parameters(p).clause(personView.call(p)).build().call(q)
+                ).build();
+
+                assertThat(actual, structurallyEqualTo(expected));
+        }
+
+        @Test
+        void deepNotEqualsTest() {
+                var p = new Variable("p");
+                var q = new Variable("q");
+                var person = new Symbol<>("Person", 1, Boolean.class, false);
+                var personView = new KeyOnlyRelationView<>(person);
+
+                var expected = Dnf.builder("Expected").parameters(q).clause(
+                                Dnf.builder("Expected2").parameters(p).clause(personView.call(p)).build().call(q)
+                ).build();
+                var actual = Dnf.builder("Actual").parameters(q).clause(
+                                Dnf.builder("Actual2").parameters(p).clause(personView.call(q)).build().call(q)
+                ).build();
+
+                var assertion = structurallyEqualTo(expected);
+                var error = assertThrows(AssertionError.class, () -> assertThat(actual, assertion));
+                assertThat(error.getMessage(), containsString(" called from Expected "));
+        }
+}
diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java
new file mode 100644
index 00000000..aaab2e7e
--- /dev/null
+++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/MismatchDescribingDnfEqualityChecker.java
@@ -0,0 +1,43 @@
+package tools.refinery.store.query.tests;
+
+import org.hamcrest.Description;
+import tools.refinery.store.query.equality.DeepDnfEqualityChecker;
+
+class MismatchDescribingDnfEqualityChecker extends DeepDnfEqualityChecker {
+        private final Description description;
+        private boolean described;
+
+        MismatchDescribingDnfEqualityChecker(Description description) {
+                this.description = description;
+        }
+
+        public boolean isDescribed() {
+                return described;
+        }
+
+        @Override
+        protected boolean doCheckEqual(Pair pair) {
+                boolean result = super.doCheckEqual(pair);
+                if (!result && !described) {
+                        describeMismatch(pair);
+                        // Only describe the first found (innermost) mismatch.
+                        described = true;
+                }
+                return result;
+        }
+
+        private void describeMismatch(Pair pair) {
+                var inProgress = getInProgress();
+                int size = inProgress.size();
+                if (size <= 1) {
+                        description.appendText("was ").appendValue(pair.left());
+                        return;
+                }
+                var last = inProgress.get(size - 1);
+                description.appendText("expected ").appendValue(last.right());
+                for (int i = size - 2; i >= 0; i--) {
+                        description.appendText(" called from ").appendText(inProgress.get(i).left().name());
+                }
+                description.appendText(" was not structurally equal to ").appendValue(last.right());
+        }
+}
diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/QueryMatchers.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/QueryMatchers.java
new file mode 100644
index 00000000..83614278
--- /dev/null
+++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/QueryMatchers.java
@@ -0,0 +1,14 @@
+package tools.refinery.store.query.tests;
+
+import org.hamcrest.Matcher;
+import tools.refinery.store.query.Dnf;
+
+public final class QueryMatchers {
+        private QueryMatchers() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+
+        public static Matcher<Dnf> structurallyEqualTo(Dnf expected) {
+                return new StructurallyEqualTo(expected);
+        }
+}
diff --git a/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/StructurallyEqualTo.java b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/StructurallyEqualTo.java
new file mode 100644
index 00000000..a42396dd
--- /dev/null
+++ b/subprojects/store-query/src/testFixtures/java/tools/refinery/store/query/tests/StructurallyEqualTo.java
@@ -0,0 +1,36 @@
+package tools.refinery.store.query.tests;
+
+import org.hamcrest.Description;
+import org.hamcrest.TypeSafeMatcher;
+import tools.refinery.store.query.Dnf;
+import tools.refinery.store.query.equality.DeepDnfEqualityChecker;
+
+public class StructurallyEqualTo extends TypeSafeMatcher<Dnf> {
+        private final Dnf expected;
+
+        public StructurallyEqualTo(Dnf expected) {
+                this.expected = expected;
+        }
+
+        @Override
+        protected boolean matchesSafely(Dnf item) {
+                var checker = new DeepDnfEqualityChecker();
+                return checker.dnfEqual(expected, item);
+        }
+
+        @Override
+        protected void describeMismatchSafely(Dnf item, Description mismatchDescription) {
+                var describingChecker = new MismatchDescribingDnfEqualityChecker(mismatchDescription);
+                if (describingChecker.dnfEqual(expected, item)) {
+                        throw new IllegalStateException("Mismatched Dnf was matching on repeated comparison");
+                }
+                if (!describingChecker.isDescribed()) {
+                        super.describeMismatchSafely(item, mismatchDescription);
+                }
+        }
+
+        @Override
+        public void describeTo(Description description) {
+                description.appendText("structurally equal to ").appendValue(expected);
+        }
+}
diff --git a/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java b/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java
index e4b462f0..8a151d01 100644
--- a/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java
+++ b/subprojects/store/src/main/java/tools/refinery/store/util/CycleDetectingMapper.java
@@ -1,9 +1,6 @@
 package tools.refinery.store.util;
 
-import java.util.HashMap;
-import java.util.LinkedHashSet;
-import java.util.Map;
-import java.util.Set;
+import java.util.*;
 import java.util.function.Function;
 import java.util.stream.Collectors;
 
@@ -45,6 +42,10 @@ public class CycleDetectingMapper<T, R> {
                 return result;
         }
 
+        public List<T> getInProgress() {
+                return List.copyOf(inProgress);
+        }
+
         public R getAlreadyMapped(T input) {
                 return results.get(input);
         }