3 files changed, 387 insertions, 0 deletions
diff --git a/proofsearch/src/infer/resolution.cc b/proofsearch/src/infer/resolution.cc
new file mode 100644
index 0000000..5fb0d4a
--- /dev/null
+++ b/proofsearch/src/infer/resolution.cc
@@ -0,0 +1,176 @@
+/*
+ * 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/infer/resolution.h"
+
+#include "atp/core/clause.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include "atp/infer/substitution.h"
+#include "atp/infer/unification.h"
+
+#include <cstddef>
+#include <cstdint>
+#include <optional>
+#include <string>
+#include <unordered_map>
+#include <utility>
+#include <vector>
+
+namespace atp {
+
+namespace {
+
+/// Recursively collect all variable TermIds appearing in a term.
+void collectVariables(TermId term, const TermBank& bank, std::unordered_map<TermId, bool>& seen) {
+    if (bank.isVariable(term)) {
+        seen[term] = true;
+        return;
+    }
+    // Copy args to avoid dangling ref (bank is const here, but be safe)
+    const Term& t = bank.getTerm(term);
+    for (TermId const arg : t.args_) {
+        collectVariables(arg, bank, seen);
+    }
+}
+
+}  // namespace
+
+Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
+                       uint32_t& next_var_id) {
+    // 1. Collect all variables in the clause
+    std::unordered_map<TermId, bool> var_set;
+    for (const auto& lit : c.literals_) {
+        collectVariables(lit.atom_, bank, var_set);
+    }
+
+    if (var_set.empty()) {
+        return c;  // Ground clause — nothing to rename
+    }
+
+    // 2. Create fresh variables and build a substitution
+    Substitution rename_subst;
+    for (auto& [old_var_id, _] : var_set) {
+        std::string const fresh_name = "_R" + std::to_string(next_var_id++);
+        SymbolId const fresh_sym = symbols.intern(fresh_name, SymbolKind::kVariable);
+        TermId const fresh_var = bank.makeVar(fresh_sym);
+        rename_subst.bind(old_var_id, fresh_var);
+    }
+
+    // 3. Apply the renaming substitution to all literals
+    Clause renamed;
+    renamed.id_ = c.id_;
+    renamed.rule_ = c.rule_;
+    renamed.parent1_ = c.parent1_;
+    renamed.parent2_ = c.parent2_;
+    renamed.depth_ = c.depth_;
+    for (const auto& lit : c.literals_) {
+        TermId const new_atom = applySubstitution(rename_subst, lit.atom_, bank);
+        renamed.literals_.push_back({.atom_ = new_atom, .is_positive_ = lit.is_positive_});
+    }
+    return renamed;
+}
+
+std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, const Clause& c2,
+                              size_t lit_idx2, const UnificationConfig& uconfig) {
+    // Must have opposite polarity
+    if (c1.literals_[lit_idx1].is_positive_ == c2.literals_[lit_idx2].is_positive_) {
+        return std::nullopt;
+    }
+
+    // Rename c2's variables to avoid clashes with c1
+    // Use a static counter — safe for single-threaded prover
+    static uint32_t var_counter = 0;
+    auto& symbols = bank.mutableSymbols();
+    Clause c2r = renameVariables(c2, bank, symbols, var_counter);
+
+    // Unify the complementary atoms
+    Substitution subst;
+    if (!unify(bank, c1.literals_[lit_idx1].atom_, c2r.literals_[lit_idx2].atom_, subst, uconfig)) {
+        return std::nullopt;
+    }
+
+    // Build the resolvent: all literals except the resolved pair, with subst applied
+    Clause resolvent;
+    resolvent.rule_ = InferenceRule::kResolution;
+    resolvent.parent1_ = c1.id_;
+    resolvent.parent2_ = c2.id_;
+
+    for (size_t i = 0; i < c1.literals_.size(); ++i) {
+        if (i != lit_idx1) {
+            TermId const new_atom = applySubstitution(subst, c1.literals_[i].atom_, bank);
+            resolvent.literals_.push_back(
+                {.atom_ = new_atom, .is_positive_ = c1.literals_[i].is_positive_});
+        }
+    }
+    for (size_t i = 0; i < c2r.literals_.size(); ++i) {
+        if (i != lit_idx2) {
+            TermId const new_atom = applySubstitution(subst, c2r.literals_[i].atom_, bank);
+            resolvent.literals_.push_back(
+                {.atom_ = new_atom, .is_positive_ = c2r.literals_[i].is_positive_});
+        }
+    }
+    return resolvent;
+}
+
+std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2,
+                                  const UnificationConfig& uconfig) {
+    std::vector<Clause> results;
+    for (size_t i = 0; i < c1.literals_.size(); ++i) {
+        for (size_t j = 0; j < c2.literals_.size(); ++j) {
+            if (c1.literals_[i].is_positive_ != c2.literals_[j].is_positive_) {
+                if (auto r = resolve(bank, c1, i, c2, j, uconfig)) {
+                    results.push_back(std::move(*r));
+                }
+            }
+        }
+    }
+    return results;
+}
+
+std::vector<Clause> factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig) {
+    std::vector<Clause> results;
+    for (size_t i = 0; i < c.literals_.size(); ++i) {
+        for (size_t j = i + 1; j < c.literals_.size(); ++j) {
+            if (c.literals_[i].is_positive_ != c.literals_[j].is_positive_) {
+                continue;  // Must have same polarity
+            }
+            Substitution subst;
+            if (!unify(bank, c.literals_[i].atom_, c.literals_[j].atom_, subst, uconfig)) {
+                continue;
+            }
+            // Build factored clause: drop literal j, apply subst to all
+            Clause factored;
+            factored.rule_ = InferenceRule::kFactoring;
+            factored.parent1_ = c.id_;
+            for (size_t k = 0; k < c.literals_.size(); ++k) {
+                if (k != j) {
+                    TermId const new_atom = applySubstitution(subst, c.literals_[k].atom_, bank);
+                    factored.literals_.push_back(
+                        {.atom_ = new_atom, .is_positive_ = c.literals_[k].is_positive_});
+                }
+            }
+            results.push_back(std::move(factored));
+        }
+    }
+    return results;
+}
+
+}  // namespace atp
diff --git a/proofsearch/src/infer/substitution.cc b/proofsearch/src/infer/substitution.cc
new file mode 100644
index 0000000..584008b
--- /dev/null
+++ b/proofsearch/src/infer/substitution.cc
@@ -0,0 +1,119 @@
+/*
+ * 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/infer/substitution.h"
+
+#include "atp/core/term.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+
+#include <algorithm>
+#include <vector>
+
+namespace atp {
+
+bool Substitution::bind(TermId var, TermId term) {
+    auto [it, inserted] = bindings_.emplace(var, term);
+    if (!inserted) {
+        // Already bound — succeed only if bound to the same term
+        return it->second == term;
+    }
+    return true;
+}
+
+TermId Substitution::lookup(TermId var) const {
+    auto it = bindings_.find(var);
+    if (it != bindings_.end()) {
+        return it->second;
+    }
+    return kInvalidId;
+}
+
+TermId Substitution::resolve(TermId id, const TermBank& bank) const {
+    // Walk the chain: X → Y → Z → f(a)
+    // Stop when we hit a non-variable or an unbound variable.
+    while (bank.isVariable(id)) {
+        auto it = bindings_.find(id);
+        if (it == bindings_.end()) {
+            break;  // Unbound variable — stop here
+        }
+        id = it->second;
+    }
+    return id;
+}
+
+TermId Substitution::apply(TermId term, TermBank& bank) const {
+    // First, resolve through variable chain
+    term = resolve(term, bank);
+
+    if (bank.isVariable(term)) {
+        // Free variable (unbound) — leave as-is
+        return term;
+    }
+
+    // IMPORTANT: Copy symbol_id and args BEFORE recursing.
+    // Recursive apply() calls may trigger bank.makeTerm() → realloc → dangling ref.
+    const Term& t = bank.getTerm(term);
+    SymbolId const sym = t.symbol_id_;
+    std::vector<TermId> const old_args(t.args_);  // copy!
+
+    if (old_args.empty()) {
+        // Constant or 0-arity — no substitution needed
+        return term;
+    }
+
+    // Recursively apply to all arguments
+    std::vector<TermId> new_args;
+    new_args.reserve(old_args.size());
+    bool changed = false;
+    for (TermId const arg : old_args) {
+        TermId const new_arg = apply(arg, bank);
+        new_args.push_back(new_arg);
+        if (new_arg != arg) {
+            changed = true;
+        }
+    }
+
+    if (!changed) {
+        return term;
+    }
+
+    return bank.makeTerm(sym, new_args);
+}
+
+bool Substitution::occursIn(TermId var, TermId term, const TermBank& bank) const {
+    term = resolve(term, bank);
+
+    if (var == term) {
+        return true;
+    }
+
+    if (bank.isVariable(term)) {
+        return false;  // Different unbound variable
+    }
+
+    const Term& t = bank.getTerm(term);
+    return std::any_of(t.args_.begin(), t.args_.end(),
+                       [&](TermId arg) { return occursIn(var, arg, bank); });
+}
+
+void Substitution::clear() {
+    bindings_.clear();
+}
+
+}  // namespace atp
+\ No newline at end of file
diff --git a/proofsearch/src/infer/unification.cc b/proofsearch/src/infer/unification.cc
new file mode 100644
index 0000000..c42bf67
--- /dev/null
+++ b/proofsearch/src/infer/unification.cc
@@ -0,0 +1,92 @@
+/*
+ * 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/infer/unification.h"
+
+#include "atp/core/term.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include "atp/infer/substitution.h"
+
+#include <cstddef>
+#include <vector>
+
+namespace atp {
+
+bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
+           const UnificationConfig& config) {
+    t1 = subst.resolve(t1, bank);
+    t2 = subst.resolve(t2, bank);
+
+    if (t1 == t2) {
+        return true;
+    }
+
+    if (bank.isVariable(t1)) {
+        if (config.enable_occurs_check_ && subst.occursIn(t1, t2, bank)) {
+            return false;
+        }
+        subst.bind(t1, t2);
+        return true;
+    }
+
+    if (bank.isVariable(t2)) {
+        if (config.enable_occurs_check_ && subst.occursIn(t2, t1, bank)) {
+            return false;
+        }
+        subst.bind(t2, t1);
+        return true;
+    }
+
+    const Term& term1 = bank.getTerm(t1);
+    const Term& term2 = bank.getTerm(t2);
+
+    if (term1.symbol_id_ != term2.symbol_id_ || term1.arity() != term2.arity()) {
+        return false;
+    }
+
+    for (size_t i = 0; i < term1.arity(); ++i) {
+        if (!unify(bank, term1.args_[i], term2.args_[i], subst, config)) {
+            return false;
+        }
+    }
+
+    return true;
+}
+
+TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank) {
+    term = subst.resolve(term, bank);
+    if (bank.isVariable(term)) {
+        return term;
+    }
+
+    // IMPORTANT: Copy args and symbol_id BEFORE recursing.
+    // Recursive calls may call bank.makeTerm() → realloc terms_ → invalidate refs.
+    const Term& t = bank.getTerm(term);
+    SymbolId const sym = t.symbol_id_;
+    std::vector<TermId> const old_args(t.args_);  // copy!
+
+    std::vector<TermId> new_args;
+    new_args.reserve(old_args.size());
+    for (TermId const arg : old_args) {
+        new_args.push_back(applySubstitution(subst, arg, bank));
+    }
+    return bank.makeTerm(sym, new_args);
+}
+
+}  // namespace atp
+\ No newline at end of file