feat: implement clause subsumption and tautology detection logic with associated unit tests

6 files changed, 250 insertions, 0 deletions

diff --git a/CMakeLists.txt b/CMakeLists.txt
index edeb6b7..1b6473e 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -77,6 +77,7 @@ set(ATP_SOURCES
     src/infer/resolution.cc
     src/index/discrim_tree.cc
     src/simplify/subsumption.cc
+    src/simplify/tautology.cc
     src/search/prover.cc
     src/proof/proof_trace.cc
     src/rewrite/ordering.cc
diff --git a/include/atp/simplify/subsumption.h b/include/atp/simplify/subsumption.h
index ee7a83e..c39b586 100644
--- a/include/atp/simplify/subsumption.h
+++ b/include/atp/simplify/subsumption.h
@@ -52,4 +52,6 @@ class SubsumptionEngine {
     // TODO: Phase 5 implementation
 };
 
+bool subsumes(const Clause& general, const Clause& specific);
+
 }  // namespace atp
diff --git a/src/simplify/subsumption.cc b/src/simplify/subsumption.cc
index b62ffd0..cf243c9 100644
--- a/src/simplify/subsumption.cc
+++ b/src/simplify/subsumption.cc
@@ -16,4 +16,27 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
+#include "atp/simplify/subsumption.h"
 
+
+namespace atp {
+
+    bool subsumes(const Clause& general, const Clause& specific) {
+        if (general.size() > specific.size()) {
+            return false;
+        }
+        for (const auto& lit_g : general.literals) {
+            bool found = false;
+            for (const auto& lit_s : specific.literals) {
+                if (lit_g.atom == lit_s.atom && lit_g.is_positive == lit_s.is_positive) {
+                    found = true;
+                    break;
+                }
+            }
+            if (!found) {
+                return false;
+            }
+        }
+        return true;
+    }
+}
diff --git a/src/simplify/tautology.cc b/src/simplify/tautology.cc
new file mode 100644
index 0000000..d41ecd7
--- /dev/null
+++ b/src/simplify/tautology.cc
@@ -0,0 +1,34 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include "atp/simplify/tautology.h"
+#include <cstddef>
+
+ namespace atp {
+    bool isTautology(const Clause& clause) {
+        for (size_t i = 0; i < clause.size(); ++i) {
+            for (size_t j = i + 1; j < clause.size(); ++j) {
+                if (clause.literals[i].atom == clause.literals[j].atom && 
+                    clause.literals[i].is_positive != clause.literals[j].is_positive) {
+                    return true;
+                }
+            }
+        }
+        return false;
+    }
+}
\ No newline at end of file
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
index d841595..864c0ad 100644
--- a/tests/CMakeLists.txt
+++ b/tests/CMakeLists.txt
@@ -25,3 +25,4 @@ atp_add_test(test_clausifier      test_clausifier.cc)
 atp_add_test(test_resolution      test_resolution.cc)
 atp_add_test(test_discrim_tree    test_discrim_tree.cc)
 atp_add_test(test_prover          test_prover.cc)
+atp_add_test(test_simplify        test_simplify.cc)
diff --git a/tests/test_simplify.cc b/tests/test_simplify.cc
new file mode 100644
index 0000000..07875de
--- /dev/null
+++ b/tests/test_simplify.cc
@@ -0,0 +1,189 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+#include <gtest/gtest.h>
+
+#include "atp/core/clause.h"
+#include "atp/core/literal.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include "atp/simplify/subsumption.h"
+#include "atp/simplify/tautology.h"
+
+namespace atp {
+namespace {
+
+class SimplifyTest : public ::testing::Test {
+  protected:
+    SymbolTable symbols;
+    TermBank bank{symbols};
+
+    SymbolId sym_a{}, sym_b{}, sym_c{};
+    SymbolId sym_P{}, sym_Q{}, sym_R{};
+    SymbolId sym_X{};
+
+    TermId a{}, b{}, c{}, X{};
+
+    void SetUp() override {
+        sym_a = symbols.intern("a", SymbolKind::kConstant);
+        sym_b = symbols.intern("b", SymbolKind::kConstant);
+        sym_c = symbols.intern("c", SymbolKind::kConstant);
+        sym_P = symbols.intern("P", SymbolKind::kPredicate, 1);
+        sym_Q = symbols.intern("Q", SymbolKind::kPredicate, 1);
+        sym_R = symbols.intern("R", SymbolKind::kPredicate, 2);
+        sym_X = symbols.intern("X", SymbolKind::kVariable);
+
+        a = bank.makeTerm(sym_a, {});
+        b = bank.makeTerm(sym_b, {});
+        c = bank.makeTerm(sym_c, {});
+        X = bank.makeVar(sym_X);
+    }
+
+    TermId P(TermId arg) { return bank.makeTerm(sym_P, {{arg}}); }
+    TermId Q(TermId arg) { return bank.makeTerm(sym_Q, {{arg}}); }
+    TermId R(TermId a1, TermId a2) { return bank.makeTerm(sym_R, {{a1, a2}}); }
+
+    Literal pos(TermId atom) { return {.atom = atom, .is_positive = true}; }
+    Literal neg(TermId atom) { return {.atom = atom, .is_positive = false}; }
+
+    Clause makeClause(std::vector<Literal> lits) {
+        Clause cl;
+        cl.literals = std::move(lits);
+        return cl;
+    }
+};
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Tautology Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(SimplifyTest, TautologyComplementaryLiterals) {
+    // {P(a), ¬P(a)} → tautology
+    Clause cl = makeClause({pos(P(a)), neg(P(a))});
+    EXPECT_TRUE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, TautologyWithExtraLiterals) {
+    // {Q(b), P(a), ¬P(a)} → tautology
+    Clause cl = makeClause({pos(Q(b)), pos(P(a)), neg(P(a))});
+    EXPECT_TRUE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, NotTautologySamePolarity) {
+    // {P(a), P(a)} → NOT tautology (same polarity)
+    Clause cl = makeClause({pos(P(a)), pos(P(a))});
+    EXPECT_FALSE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, NotTautologyDifferentAtoms) {
+    // {P(a), ¬P(b)} → NOT tautology (different atoms)
+    Clause cl = makeClause({pos(P(a)), neg(P(b))});
+    EXPECT_FALSE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, NotTautologyDifferentPredicates) {
+    // {P(a), ¬Q(a)} → NOT tautology (different predicates)
+    Clause cl = makeClause({pos(P(a)), neg(Q(a))});
+    EXPECT_FALSE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, NotTautologyEmptyClause) {
+    Clause cl = makeClause({});
+    EXPECT_FALSE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, NotTautologySingleLiteral) {
+    Clause cl = makeClause({pos(P(a))});
+    EXPECT_FALSE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, TautologyVariableAtom) {
+    // {P(X), ¬P(X)} → tautology (same variable term)
+    Clause cl = makeClause({pos(P(X)), neg(P(X))});
+    EXPECT_TRUE(isTautology(cl));
+}
+
+TEST_F(SimplifyTest, NotTautologyVarVsConst) {
+    // {P(X), ¬P(a)} → NOT tautology (syntactically different)
+    Clause cl = makeClause({pos(P(X)), neg(P(a))});
+    EXPECT_FALSE(isTautology(cl));
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Subsumption Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(SimplifyTest, SubsumesSubset) {
+    // {P(a)} subsumes {P(a), Q(b)}
+    Clause gen = makeClause({pos(P(a))});
+    Clause spec = makeClause({pos(P(a)), pos(Q(b))});
+    EXPECT_TRUE(subsumes(gen, spec));
+}
+
+TEST_F(SimplifyTest, SubsumesIdentical) {
+    // {P(a), Q(b)} subsumes {P(a), Q(b)}
+    Clause c1 = makeClause({pos(P(a)), pos(Q(b))});
+    Clause c2 = makeClause({pos(P(a)), pos(Q(b))});
+    EXPECT_TRUE(subsumes(c1, c2));
+}
+
+TEST_F(SimplifyTest, SubsumesEmptyClause) {
+    // {} subsumes everything
+    Clause empty = makeClause({});
+    Clause cl = makeClause({pos(P(a)), neg(Q(b))});
+    EXPECT_TRUE(subsumes(empty, cl));
+}
+
+TEST_F(SimplifyTest, SubsumesNotLarger) {
+    // {P(a), Q(b)} does NOT subsume {P(a)}
+    Clause gen = makeClause({pos(P(a)), pos(Q(b))});
+    Clause spec = makeClause({pos(P(a))});
+    EXPECT_FALSE(subsumes(gen, spec));
+}
+
+TEST_F(SimplifyTest, SubsumesRequiresSamePolarity) {
+    // {P(a)} does NOT subsume {¬P(a)}
+    Clause gen = makeClause({pos(P(a))});
+    Clause spec = makeClause({neg(P(a))});
+    EXPECT_FALSE(subsumes(gen, spec));
+}
+
+TEST_F(SimplifyTest, SubsumesRequiresSameAtom) {
+    // {P(a)} does NOT subsume {P(b)}
+    Clause gen = makeClause({pos(P(a))});
+    Clause spec = makeClause({pos(P(b))});
+    EXPECT_FALSE(subsumes(gen, spec));
+}
+
+TEST_F(SimplifyTest, SubsumesNegativeLiterals) {
+    // {¬P(a)} subsumes {¬P(a), Q(b)}
+    Clause gen = makeClause({neg(P(a))});
+    Clause spec = makeClause({neg(P(a)), pos(Q(b))});
+    EXPECT_TRUE(subsumes(gen, spec));
+}
+
+TEST_F(SimplifyTest, SubsumesOrderIndependent) {
+    // {Q(b), P(a)} subsumes {P(a), Q(b), R(a,b)} regardless of order
+    Clause gen = makeClause({pos(Q(b)), pos(P(a))});
+    Clause spec = makeClause({pos(P(a)), pos(Q(b)), pos(R(a, b))});
+    EXPECT_TRUE(subsumes(gen, spec));
+}
+
+}  // namespace
+}  // namespace atp