Merge remote-tracking branch 'proofsearch-import/master'

26 files changed, 1602 insertions, 0 deletions

diff --git a/proofsearch/include/atp/core/clause.h b/proofsearch/include/atp/core/clause.h
new file mode 100644
index 0000000..6387adf
--- /dev/null
+++ b/proofsearch/include/atp/core/clause.h
@@ -0,0 +1,52 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file clause.h
+/// @brief A clause is a disjunction of literals, with provenance tracking.
+///
+/// NOTE: V1 uses std::vector<Literal> for simplicity.
+/// Future optimization: migrate to a Clause Arena with contiguous storage.
+
+#include "atp/core/literal.h"
+#include "atp/core/types.h"
+
+#include <vector>
+
+namespace atp {
+
+/// A clause: a disjunction of literals plus provenance for proof reconstruction.
+struct Clause {
+    ClauseId id_ = kInvalidId;
+    std::vector<Literal> literals_;
+
+    // Provenance (for proof trace)
+    InferenceRule rule_ = InferenceRule::kInput;
+    ClauseId parent1_ = kInvalidId;
+    ClauseId parent2_ = kInvalidId;
+    uint16_t depth_ = 0;  ///< Derivation depth (for BFS scheduling)
+
+    /// True if the clause has no literals (contradiction).
+    [[nodiscard]] bool isEmpty() const { return literals_.empty(); }
+
+    /// Number of literals.
+    [[nodiscard]] size_t size() const { return literals_.size(); }
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/core/clause_store.h b/proofsearch/include/atp/core/clause_store.h
new file mode 100644
index 0000000..5d6562a
--- /dev/null
+++ b/proofsearch/include/atp/core/clause_store.h
@@ -0,0 +1,64 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file clause_store.h
+/// @brief Central clause storage — owns all clauses, assigns ClauseIds.
+///
+/// Extracted from Prover to separate storage responsibility from search logic.
+/// This enables swapping search strategies (OTTER loop / DISCOUNT loop)
+/// without touching clause lifecycle management.
+
+#include "atp/core/clause.h"
+#include "atp/core/types.h"
+
+#include <functional>
+#include <vector>
+
+namespace atp {
+
+/// Central clause store. Owns all clauses and assigns unique ClauseIds.
+/// All modules access clauses through this store via ClauseId references.
+class ClauseStore {
+  public:
+    ClauseStore() = default;
+
+    /// Add a clause, assign it a ClauseId, and return the ID.
+    ClauseId addClause(Clause clause);
+
+    /// Access a clause by its ID. UB if id is out of range.
+    [[nodiscard]] const Clause& getClause(ClauseId id) const;
+
+    /// Mutable access (for marking clauses as deleted, etc.)
+    [[nodiscard]] Clause& getMutableClause(ClauseId id);
+
+    /// Total number of stored clauses.
+    [[nodiscard]] size_t size() const;
+
+    /// Iterate over all clauses with a visitor.
+    void forEach(const std::function<void(const Clause&)>& visitor) const;
+    // function may have type erasure overhead, consider using a template
+    // template <typename Visitor>
+    // void forEach(Visitor&& visitor) const;
+
+  private:
+    std::vector<Clause> clauses_;
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/core/literal.h b/proofsearch/include/atp/core/literal.h
new file mode 100644
index 0000000..e58b185
--- /dev/null
+++ b/proofsearch/include/atp/core/literal.h
@@ -0,0 +1,39 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file literal.h
+/// @brief A literal is a (possibly negated) atomic formula.
+
+#include "atp/core/types.h"
+
+namespace atp {
+
+/// A literal: a polarity flag plus the TermId of the atom.
+struct Literal {
+    TermId atom_;       ///< TermId of the predicate application
+    bool is_positive_;  ///< true = positive, false = negated
+
+    /// Complement: flip polarity, same atom.
+    [[nodiscard]] Literal complement() const { return {.atom_ = atom_, .is_positive_ = !is_positive_}; }
+
+    bool operator==(const Literal& other) const = default;
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/core/symbol_table.h b/proofsearch/include/atp/core/symbol_table.h
new file mode 100644
index 0000000..a646f78
--- /dev/null
+++ b/proofsearch/include/atp/core/symbol_table.h
@@ -0,0 +1,71 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file symbol_table.h
+/// @brief Bidirectional mapping between symbol names and SymbolIds,
+///        with kind and sort metadata.
+
+#include "atp/core/types.h"
+
+#include <deque>
+#include <string>
+#include <string_view>
+#include <unordered_map>
+
+namespace atp {
+
+/// Metadata associated with an interned symbol.
+struct SymbolInfo {
+    std::string name_;
+    SymbolKind kind_ = SymbolKind::kFunction;
+    uint16_t arity_ = 0;
+    SortId sort_ = kUnsorted;  ///< Result sort (for sorted logic)
+};
+
+/// Interns symbol names so that each unique string is stored exactly once.
+/// Also tracks symbol metadata (kind, arity, sort).
+/// Thread-safety: NOT thread-safe (single-threaded prover design).
+class SymbolTable {
+  public:
+    SymbolTable() = default;
+
+    /// Intern a symbol name with metadata. Returns existing ID if already present.
+    SymbolId intern(std::string_view name, SymbolKind kind, uint16_t arity = 0,
+                    SortId sort = kUnsorted);
+
+    /// Look up the name for a given SymbolId. UB if id is out of range.
+    [[nodiscard]] std::string_view getName(SymbolId id) const;
+
+    /// Look up full metadata for a SymbolId.
+    [[nodiscard]] const SymbolInfo& getInfo(SymbolId id) const;
+
+    /// Check if a symbol is a variable.
+    [[nodiscard]] bool isVariable(SymbolId id) const;
+
+    /// Number of interned symbols.
+    [[nodiscard]] size_t size() const;
+
+  private:
+    // TODO: Phase 1 implementation
+    std::deque<SymbolInfo> infos_;
+    std::unordered_map<std::string_view, SymbolId> name_to_id_;
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/core/term.h b/proofsearch/include/atp/core/term.h
new file mode 100644
index 0000000..d35c753
--- /dev/null
+++ b/proofsearch/include/atp/core/term.h
@@ -0,0 +1,43 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file term.h
+/// @brief Core Term data structure — hash-consed, immutable.
+///
+/// V1 uses vector<TermId> for args.
+/// Future: flat arena with contiguous arg storage for cache locality.
+
+#include "atp/core/types.h"
+
+#include <vector>
+
+namespace atp {
+
+/// A term is a function/predicate application: f(t1, t2, ..., tn).
+/// Variables are 0-arity terms whose symbol has SymbolKind::kVariable.
+struct Term {
+    SymbolId symbol_id_;        ///< Index into the SymbolTable
+    std::vector<TermId> args_;  ///< Argument sub-term IDs
+
+    /// Number of arguments.
+    [[nodiscard]] uint16_t arity() const { return static_cast<uint16_t>(args_.size()); }
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/core/term_bank.h b/proofsearch/include/atp/core/term_bank.h
new file mode 100644
index 0000000..ca12759
--- /dev/null
+++ b/proofsearch/include/atp/core/term_bank.h
@@ -0,0 +1,86 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file term_bank.h
+/// @brief Hash-consing term pool — guarantees structural sharing.
+
+#include "atp/core/symbol_table.h"
+#include "atp/core/term.h"
+#include "atp/core/types.h"
+
+#include <span>
+#include <unordered_map>
+#include <vector>
+
+namespace atp {
+
+/// Global term pool with hash-consing.
+/// Every structurally identical term maps to the same TermId.
+///
+/// Holds a reference to SymbolTable for variable detection.
+class TermBank {
+  public:
+    /// TermBank needs the SymbolTable to distinguish variables from constants
+    /// (both have 0 args, but SymbolKind differs).
+        explicit TermBank(SymbolTable& symbols) : symbols_(&symbols) {}
+
+    /// Create or retrieve a term. Returns the canonical TermId.
+    TermId makeTerm(SymbolId symbol, std::span<const TermId> args);
+
+    /// Create a variable term. Convenience for makeTerm(var, {}).
+    TermId makeVar(SymbolId var_symbol);
+
+    /// Look up a term by its ID.
+    [[nodiscard]] const Term& getTerm(TermId id) const;
+
+    /// Check if a TermId represents a variable (delegates to SymbolTable).
+    [[nodiscard]] bool isVariable(TermId id) const;
+
+    /// Total number of unique terms stored.
+    [[nodiscard]] size_t size() const;
+
+    /// Access the underlying SymbolTable.
+    [[nodiscard]] const SymbolTable& symbols() const { return *symbols_; }
+    [[nodiscard]] SymbolTable& mutableSymbols() { return *symbols_; }
+
+  private:
+    struct TermKey {
+        SymbolId symbol_;
+        std::vector<TermId> args_;
+
+        bool operator==(const TermKey& other) const = default;
+    };
+
+    struct TermKeyHash {
+        size_t operator()(const TermKey& key) const {
+            size_t seed = std::hash<uint32_t>{}(key.symbol_);
+            for (const TermId arg : key.args_) {
+                seed ^= std::hash<TermId>{}(arg) + 0x9e3779b9 + (seed << 6) + (seed >> 2);
+            }
+            return seed;
+        }
+    };
+
+    SymbolTable* symbols_;
+    std::vector<Term> terms_;
+    std::unordered_map<TermKey, TermId, TermKeyHash> term_to_id_;
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/core/types.h b/proofsearch/include/atp/core/types.h
new file mode 100644
index 0000000..23f2322
--- /dev/null
+++ b/proofsearch/include/atp/core/types.h
@@ -0,0 +1,79 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file types.h
+/// @brief Core type aliases for the ATP engine.
+
+#include <cstdint>
+
+namespace atp {
+
+/// Unique identifier for an interned symbol (predicate/function/constant name).
+using SymbolId = uint32_t;
+
+/// Unique identifier for a term in the Term Bank (hash-consed).
+using TermId = uint32_t;
+
+/// Unique identifier for a clause in the Clause Store.
+using ClauseId = uint32_t;
+
+/// Unique identifier for a sort/type (for sorted logic).
+using SortId = uint16_t;
+
+/// Sentinel value indicating an invalid / unassigned ID.
+inline constexpr uint32_t kInvalidId = UINT32_MAX;
+
+/// Default sort (unsorted logic).
+inline constexpr SortId kUnsorted = 0;
+
+/// Symbol kind — distinguishes variables from function/predicate symbols.
+enum class SymbolKind : uint8_t {
+    kVariable,   ///< Universally quantified variable
+    kConstant,   ///< 0-arity function symbol (constant)
+    kFunction,   ///< Function symbol (arity >= 1)
+    kPredicate,  ///< Predicate symbol (returns bool)
+    kSkolem,     ///< Skolem function/constant (introduced by Skolemization)
+};
+
+/// Inference rule that produced a clause.
+/// Deliberately uses uint16_t for extensibility toward algebra/analysis rules.
+enum class InferenceRule : uint16_t {
+    // ── Core resolution rules ──
+    kInput = 0,       ///< Original input clause (axiom / negated conjecture)
+    kResolution = 1,  ///< Binary resolution
+    kFactoring = 2,   ///< Factoring
+
+    // ── Equality rules (algebra) ──
+    kParamodulation = 100,      ///< Paramodulation (equality resolution)
+    kDemodulation = 101,        ///< Demodulation (simplification by rewriting)
+    kEqualityResolution = 102,  ///< s != t resolved with unifier
+    kEqualityFactoring = 103,   ///< Factoring with equality
+
+    // ── Simplification rules ──
+    kSubsumption = 200,      ///< Removed by subsumption
+    kTautologyElim = 201,    ///< Removed as tautology
+    kPureLiteralElim = 202,  ///< Pure literal elimination
+
+    // ── Theory rules (analysis, arithmetic) ──
+    kTheoryResolution = 300,  ///< Theory-specific resolution
+    kTheoryRewrite = 301,     ///< Theory-driven rewriting
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/frontend/tptp_parser.h b/proofsearch/include/atp/frontend/tptp_parser.h
new file mode 100644
index 0000000..68a5564
--- /dev/null
+++ b/proofsearch/include/atp/frontend/tptp_parser.h
@@ -0,0 +1,99 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file tptp_parser.h
+/// @brief TPTP format parser — converts .p files to internal representations.
+///
+/// The parser interns all symbols (predicates, functions, variables) into the
+/// SymbolTable and builds terms in the TermBank during parsing. This is the
+/// E Prover approach: parse and intern simultaneously, avoiding a separate
+/// resolution pass.
+///
+/// V1: Hand-written recursive descent for TPTP CNF/FOF subset.
+///     (ANTLR4 integration deferred — avoids build complexity for V1.)
+
+#include "atp/core/clause.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/normalize/formula.h"
+
+#include <string>
+#include <vector>
+
+namespace atp {
+
+/// Role of a TPTP formula.
+/// See TPTP spec: https://www.tptp.org/TPTP/SyntaxBNF.html
+enum class FormulaRole : uint8_t {
+    kAxiom,              ///< Background truth
+    kHypothesis,         ///< Problem-specific assumption
+    kDefinition,         ///< Symbol definition (can be unfolded)
+    kAssumption,         ///< Assumed for this proof attempt
+    kLemma,              ///< Derived intermediate result
+    kTheorem,            ///< Previously proved statement (used as axiom)
+    kConjecture,         ///< The statement to prove
+    kNegatedConjecture,  ///< Already negated conjecture (input was cnf)
+    kPlain,              ///< No semantic role specified
+};
+
+/// Map a TPTP role string to enum. Returns kPlain for unknown roles.
+FormulaRole parseRole(std::string_view role_str);
+
+/// A parsed TPTP formula with its name and role.
+struct AnnotatedFormula {
+    std::string name_;                  ///< Formula name (e.g., "axiom1")
+    FormulaRole role_ = FormulaRole::kPlain;  ///< Semantic role
+    std::unique_ptr<Formula> formula_;  ///< The FOL formula (for fof(...))
+    std::vector<Clause> clauses_;       ///< Direct clauses (for cnf(...))
+    bool is_cnf_ = false;               ///< true if input was cnf(), false if fof()
+};
+
+/// A complete parsed TPTP problem.
+struct ParsedProblem {
+    std::vector<AnnotatedFormula> formulas_;
+
+    /// Does any formula contain an equality predicate?
+    bool has_equality_ = false;
+
+    /// Original file path (for error messages).
+    std::string source_file_;
+};
+
+/// Parse a TPTP file.
+///
+/// For `cnf(...)` entries: clauses are built directly (no clausification needed).
+/// For `fof(...)` entries: Formula AST is built (clausification happens later).
+///
+/// All symbols are interned into `symbols` and terms into `bank` during parsing.
+ParsedProblem parseTptpFile(const std::string& filename, TermBank& bank, SymbolTable& symbols);
+
+/// Parse a TPTP string (for testing).
+ParsedProblem parseTptpString(const std::string& input, TermBank& bank, SymbolTable& symbols);
+
+/// Prepare a parsed problem for proving:
+///   1. Negate conjecture formulas.
+///   2. Clausify all fof() formulas.
+///   3. Collect all cnf() clauses directly.
+///   4. Assign ClauseIds and set provenance to kInput.
+///
+/// Returns the final clause set ready for the Prover.
+std::vector<Clause> prepareForProving(ParsedProblem& problem, TermBank& bank, SymbolTable& symbols);
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/index/discrim_tree.h b/proofsearch/include/atp/index/discrim_tree.h
new file mode 100644
index 0000000..5f8a206
--- /dev/null
+++ b/proofsearch/include/atp/index/discrim_tree.h
@@ -0,0 +1,76 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file discrim_tree.h
+/// @brief Perfect Discrimination Tree for fast term indexing.
+///
+/// Used by subsumption and resolution to quickly find candidate clauses
+/// whose literals unify with a query term. Supports three query modes:
+///   - Unifiable:       find terms that can be unified with the query
+///   - Instances:       find terms that are instances of the query (more specific)
+///   - Generalizations: find terms that are generalizations of the query (more general)
+
+#include "atp/core/clause.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+
+#include <vector>
+
+namespace atp {
+
+/// A match result from the discrimination tree.
+struct IndexMatch {
+    ClauseId clause_id_;
+    size_t lit_index_;
+};
+
+/// A discrimination tree index over terms.
+/// Supports insertion and three types of retrieval queries.
+class DiscrimTree {
+  public:
+    explicit DiscrimTree(const TermBank& bank);
+
+    /// Insert a term (identified by its TermId) with an associated clause/literal ref.
+    void insert(TermId term, ClauseId clause_id, size_t lit_index);
+
+    /// Retrieve all entries whose indexed term is unifiable with `query`.
+    [[nodiscard]] std::vector<IndexMatch> queryUnifiable(TermId query) const;
+
+    /// Retrieve all entries whose indexed term is an instance of `query`.
+    /// (query is more general, indexed term is more specific)
+    [[nodiscard]] std::vector<IndexMatch> queryInstances(TermId query) const;
+
+    /// Retrieve all entries whose indexed term is a generalization of `query`.
+    /// (indexed term is more general, query is more specific)
+    /// This is the key operation for forward subsumption.
+    [[nodiscard]] std::vector<IndexMatch> queryGeneralizations(TermId query) const;
+
+    /// Remove all entries for a given clause.
+    void removeClause(ClauseId clause_id);
+
+    /// Number of indexed entries.
+    [[nodiscard]] size_t size() const;
+
+  private:
+    const TermBank& bank_;
+    // TODO: Phase 3 implementation — trie node arena
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/infer/resolution.h b/proofsearch/include/atp/infer/resolution.h
new file mode 100644
index 0000000..6e2954d
--- /dev/null
+++ b/proofsearch/include/atp/infer/resolution.h
@@ -0,0 +1,50 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file resolution.h
+/// @brief Binary resolution and factoring inference rules.
+
+#include "atp/core/clause.h"
+#include "atp/core/term_bank.h"
+#include "atp/infer/unification.h"
+
+#include <optional>
+#include <vector>
+
+namespace atp {
+
+/// Attempt binary resolution between two clauses on the specified literal indices.
+/// @return The resolvent clause if resolution succeeds, std::nullopt otherwise.
+std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, const Clause& c2,
+                              size_t lit_idx2, const UnificationConfig& uconfig = {});
+
+/// Generate all possible resolvents between two clauses.
+std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2,
+                                  const UnificationConfig& uconfig = {});
+
+/// Attempt factoring on a single clause (merge two unifiable literals).
+std::vector<Clause> factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig = {});
+
+/// Rename all variables in a clause to fresh ones, avoiding conflicts
+/// with variables already in the bank.
+Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
+                       uint32_t& next_var_id);
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/infer/substitution.h b/proofsearch/include/atp/infer/substitution.h
new file mode 100644
index 0000000..671f6d7
--- /dev/null
+++ b/proofsearch/include/atp/infer/substitution.h
@@ -0,0 +1,76 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file substitution.h
+/// @brief Variable binding map: Var -> Term.
+///
+/// Short-lived object created during unification, applied to build resolvents,
+/// then discarded. Never stored long-term.
+
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+
+#include <unordered_map>
+
+namespace atp {
+
+/// A substitution σ maps variable TermIds to their bound TermIds.
+///
+/// Example: σ = { X → f(a), Y → Z }
+///   lookup(X) = f(a)     (direct binding)
+///   resolve(X) = f(a)    (same — f(a) is not a variable)
+///   resolve(Y) = Z       (if Z is unbound, stops at Z)
+///   resolve(Y) = f(b)    (if Z → f(b) also in σ, walks the chain)
+class Substitution {
+  public:
+    Substitution() = default;
+
+    /// Bind a variable to a term. Returns false if already bound to a different term.
+    bool bind(TermId var, TermId term);
+
+    /// Look up what a variable is directly bound to. Returns kInvalidId if unbound.
+    [[nodiscard]] TermId lookup(TermId var) const;
+
+    /// Walk the binding chain to the final value.
+    /// If var → Y → f(a), returns f(a).
+    /// Requires TermBank to check whether intermediate values are variables.
+    [[nodiscard]] TermId resolve(TermId id, const TermBank& bank) const;
+
+    /// Apply this substitution to a term recursively, creating new terms in the bank.
+    /// Free (unbound) variables are left as-is.
+    [[nodiscard]] TermId apply(TermId term, TermBank& bank) const;
+
+    /// Check if a variable occurs anywhere inside a term (for occurs check).
+    [[nodiscard]] bool occursIn(TermId var, TermId term, const TermBank& bank) const;
+
+    /// Clear all bindings.
+    void clear();
+
+    /// Number of bindings.
+    [[nodiscard]] size_t size() const { return bindings_.size(); }
+
+    /// Check if empty.
+    [[nodiscard]] bool empty() const { return bindings_.empty(); }
+
+  private:
+    std::unordered_map<TermId, TermId> bindings_;
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/infer/unification.h b/proofsearch/include/atp/infer/unification.h
new file mode 100644
index 0000000..870be66
--- /dev/null
+++ b/proofsearch/include/atp/infer/unification.h
@@ -0,0 +1,43 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file unification.h
+/// @brief Most General Unifier (MGU) computation.
+
+#include "atp/core/term_bank.h"
+#include "atp/infer/substitution.h"
+
+namespace atp {
+
+/// Configuration for the unification algorithm.
+struct UnificationConfig {
+    bool enable_occurs_check_ = false;  ///< Set true for sound but slower unification
+};
+
+/// Attempt to unify two terms, producing a most general unifier.
+/// @return true if unification succeeds, with the MGU in `subst`.
+bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
+           const UnificationConfig& config = {});
+
+/// Apply a substitution to a term recursively, creating new terms in the bank.
+/// Free (unbound) variables are left unchanged.
+TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank);
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/normalize/clausifier.h b/proofsearch/include/atp/normalize/clausifier.h
new file mode 100644
index 0000000..61d2505
--- /dev/null
+++ b/proofsearch/include/atp/normalize/clausifier.h
@@ -0,0 +1,69 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file clausifier.h
+/// @brief Converts FOL formulas to Clause Normal Form (CNF).
+///
+/// Clausifier is a stateful object because:
+///   1. Skolem function counter must be shared across all formulas in a problem
+///      (otherwise different formulas generate conflicting Skolem names).
+///   2. Variable renaming counter must be shared for the same reason.
+///
+/// Pipeline: eliminate ↔/→  →  NNF  →  Skolemize  →  distribute ∨ over ∧  →  flatten.
+
+#include "atp/core/clause.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/normalize/formula.h"
+
+#include <vector>
+
+namespace atp {
+
+/// Stateful clausifier. Create one per proof problem.
+///
+/// Usage:
+///   Clausifier clausifier(bank, symbols);
+///   auto clauses1 = clausifier.clausify(formula1);
+///   auto clauses2 = clausifier.clausify(formula2);
+///   // Skolem IDs are unique across both calls.
+class Clausifier {
+  public:
+    Clausifier(TermBank& bank, SymbolTable& symbols);
+
+    /// Convert a single formula to CNF clauses.
+    /// Skolem functions generated here are globally unique (counter persists).
+    [[nodiscard]] std::vector<Clause> clausify(const Formula& formula);
+
+    /// Negate a formula: wraps it in ¬(...)
+    /// Used to negate the conjecture before clausification.
+    [[nodiscard]] static std::unique_ptr<Formula> negate(std::unique_ptr<Formula> formula);
+
+    /// Number of Skolem functions generated so far.
+    [[nodiscard]] uint32_t skolemCount() const { return next_skolem_id_; }
+
+  private:
+    TermBank& bank_;
+    SymbolTable& symbols_;
+    uint32_t next_skolem_id_ = 0;
+    uint32_t next_var_id_ = 0;  ///< For variable standardization apart
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/normalize/formula.h b/proofsearch/include/atp/normalize/formula.h
new file mode 100644
index 0000000..5ee9b94
--- /dev/null
+++ b/proofsearch/include/atp/normalize/formula.h
@@ -0,0 +1,84 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file formula.h
+/// @brief First-order logic formula AST (pre-clausification).
+///
+/// Design decision: atoms use TermId (interned), quantifier variables use
+/// SymbolId (interned). The parser interns all symbols during parsing.
+/// This avoids string→ID lookups during clausification and ensures
+/// consistent variable identity across quantifier scopes.
+
+#include "atp/core/types.h"
+
+#include <memory>
+#include <vector>
+
+namespace atp {
+
+/// AST node types for first-order logic formulas.
+enum class FormulaKind : uint8_t {
+    kAtom,      ///< Predicate application: P(t1, ..., tn)
+    kEquality,  ///< Equality atom: t1 = t2 (distinguished for equality reasoning)
+    kNot,       ///< Negation: ¬F
+    kAnd,       ///< Conjunction: F ∧ G
+    kOr,        ///< Disjunction: F ∨ G
+    kImplies,   ///< Implication: F → G
+    kIff,       ///< Biconditional: F ↔ G
+    kForall,    ///< Universal: ∀x. F
+    kExists,    ///< Existential: ∃x. F
+};
+
+/// A first-order logic formula node.
+///
+/// All identifiers are interned: atoms as TermIds, quantifier variables as
+/// SymbolIds. No raw strings survive past the parser.
+struct Formula {
+    FormulaKind kind_;
+
+    /// For kAtom / kEquality: the predicate/equality term, already interned.
+    TermId atom_ = kInvalidId;
+
+    /// For kForall / kExists: the bound variable, as an interned SymbolId.
+    /// Using SymbolId (not string) so the clausifier can map bound variables
+    /// back to term-bank variables without string lookups.
+    SymbolId bound_var_ = kInvalidId;
+
+    /// Sub-formulas (1 for Not/Quantifiers, 2 for binary connectives).
+    std::vector<std::unique_ptr<Formula>> children_;
+
+    // ── Factory methods ──
+
+    static std::unique_ptr<Formula> makeAtom(TermId atom);
+    static std::unique_ptr<Formula> makeEquality(TermId lhs, TermId rhs, TermId eq_atom);
+    static std::unique_ptr<Formula> makeNot(std::unique_ptr<Formula> child);
+    static std::unique_ptr<Formula> makeAnd(std::unique_ptr<Formula> lhs,
+                                            std::unique_ptr<Formula> rhs);
+    static std::unique_ptr<Formula> makeOr(std::unique_ptr<Formula> lhs,
+                                           std::unique_ptr<Formula> rhs);
+    static std::unique_ptr<Formula> makeImplies(std::unique_ptr<Formula> lhs,
+                                                std::unique_ptr<Formula> rhs);
+    static std::unique_ptr<Formula> makeIff(std::unique_ptr<Formula> lhs,
+                                            std::unique_ptr<Formula> rhs);
+    static std::unique_ptr<Formula> makeForall(SymbolId var, std::unique_ptr<Formula> body);
+    static std::unique_ptr<Formula> makeExists(SymbolId var, std::unique_ptr<Formula> body);
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/proof/proof_trace.h b/proofsearch/include/atp/proof/proof_trace.h
new file mode 100644
index 0000000..4ea7aa1
--- /dev/null
+++ b/proofsearch/include/atp/proof/proof_trace.h
@@ -0,0 +1,55 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file proof_trace.h
+/// @brief Proof reconstruction from the empty clause back to axioms.
+
+#include "atp/core/clause.h"
+#include "atp/core/clause_store.h"
+#include "atp/core/term_bank.h"
+
+#include <string>
+#include <vector>
+
+namespace atp {
+
+/// A single step in a reconstructed proof.
+struct ProofStep {
+    ClauseId clause_id_;
+    InferenceRule rule_;
+    ClauseId parent1_;
+    ClauseId parent2_;
+};
+
+/// Reconstruct the proof trace from the empty clause.
+/// Returns steps in topological order: axioms first, empty clause last.
+std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_clause_id);
+
+/// Convert a TermId back to a human-readable string.
+std::string termToString(TermId id, const TermBank& bank);
+
+/// Convert a Clause to a human-readable string.
+std::string clauseToString(const Clause& clause, const TermBank& bank);
+
+/// Format a proof as a human-readable string.
+std::string formatProof(const std::vector<ProofStep>& proof, const ClauseStore& store,
+                        const TermBank& bank);
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/rewrite/ordering.h b/proofsearch/include/atp/rewrite/ordering.h
new file mode 100644
index 0000000..195c3c6
--- /dev/null
+++ b/proofsearch/include/atp/rewrite/ordering.h
@@ -0,0 +1,52 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file ordering.h
+/// @brief Term orderings for equality reasoning (KBO, LPO).
+///
+/// Term orderings are the foundation of equality-based theorem proving.
+/// They ensure that rewriting always terminates by enforcing a well-founded
+/// ordering on terms. Required by paramodulation, demodulation, and
+/// ordered resolution.
+
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+
+namespace atp {
+
+/// Ordering comparison result.
+enum class OrderResult : uint8_t {
+    kLessThan,      ///< t1 < t2
+    kEqual,         ///< t1 = t2
+    kGreaterThan,   ///< t1 > t2
+    kIncomparable,  ///< t1 and t2 are incomparable
+};
+
+/// Abstract base for term orderings.
+/// Concrete implementations: KBO (Knuth-Bendix), LPO (Lexicographic Path).
+class TermOrdering {
+  public:
+    virtual ~TermOrdering() = default;
+
+    /// Compare two terms under the ordering.
+    [[nodiscard]] virtual OrderResult compare(const TermBank& bank, TermId t1, TermId t2) const = 0;
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/rewrite/paramodulation.h b/proofsearch/include/atp/rewrite/paramodulation.h
new file mode 100644
index 0000000..9dfbd66
--- /dev/null
+++ b/proofsearch/include/atp/rewrite/paramodulation.h
@@ -0,0 +1,47 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file paramodulation.h
+/// @brief Paramodulation inference rule for equality reasoning.
+///
+/// Paramodulation replaces a subterm in one clause with an equal term
+/// from an equation in another clause. Combined with term orderings,
+/// this gives a complete calculus for first-order logic with equality
+/// (the Superposition calculus).
+
+#include "atp/core/clause.h"
+#include "atp/core/term_bank.h"
+#include "atp/rewrite/ordering.h"
+
+#include <vector>
+
+namespace atp {
+
+/// Generate all paramodulants between two clauses.
+/// Uses the term ordering to restrict to ordered paramodulation (superposition).
+std::vector<Clause> paramodulate(const TermBank& bank, const Clause& c1, const Clause& c2,
+                                 const TermOrdering& ordering);
+
+/// Simplify a clause by demodulation (rewriting with unit equalities).
+/// Returns true if the clause was modified.
+bool demodulate(TermBank& bank, Clause& clause, const Clause& unit_eq,
+                const TermOrdering& ordering);
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/search/clause_queue.h b/proofsearch/include/atp/search/clause_queue.h
new file mode 100644
index 0000000..dfb575c
--- /dev/null
+++ b/proofsearch/include/atp/search/clause_queue.h
@@ -0,0 +1,43 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file clause_queue.h
+/// @brief Priority queue for the Given Clause Loop.
+
+#include "atp/core/clause.h"
+
+#include <functional>
+
+namespace atp {
+
+/// Comparison function type for clause ordering.
+using ClauseComparator = std::function<bool(const Clause& a, const Clause& b)>;
+
+/// BFS comparator: prioritize shallower derivation depth.
+inline bool bfsCompare(const Clause& a, const Clause& b) {
+    return a.depth_ > b.depth_;  // min-heap by depth
+}
+
+/// Weight comparator: prioritize shorter (fewer literals) clauses.
+inline bool weightCompare(const Clause& a, const Clause& b) {
+    return a.literals_.size() > b.literals_.size();  // min-heap by literal count
+}
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/search/prover.h b/proofsearch/include/atp/search/prover.h
new file mode 100644
index 0000000..65ec7f0
--- /dev/null
+++ b/proofsearch/include/atp/search/prover.h
@@ -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/>.
+ */
+
+#pragma once
+
+/// @file prover.h
+/// @brief The Given Clause Loop — main saturation-based proof search.
+///
+/// V1: Uses a simple ProverConfig with hardcoded resolution + factoring.
+/// V2: Will be refactored to accept a Calculus object from strategy/ module
+///     for dynamic algorithm loading per problem type.
+
+#include "atp/core/clause.h"
+#include "atp/core/clause_store.h"
+#include "atp/core/term_bank.h"
+#include "atp/search/clause_queue.h"
+
+#include <optional>
+#include <queue>
+#include <vector>
+
+namespace atp {
+
+/// Result of a proof attempt.
+enum class ProverResult : uint8_t {
+    kTheorem,     ///< Empty clause derived — conjecture is a theorem
+    kSaturation,  ///< Search space saturated — cannot prove
+    kTimeout,     ///< Resource limit exceeded
+};
+
+/// V1 configuration — simple and direct.
+/// Future: replaced by strategy::Calculus for dynamic rule loading.
+struct ProverConfig {
+    ClauseComparator comparator_ = bfsCompare;
+    size_t max_clauses_ = 100000;     ///< Safety limit
+    size_t max_iterations_ = 500000;  ///< Safety limit
+    bool enable_occurs_check_ = false;
+};
+
+/// Main prover class implementing the Given Clause Loop.
+/// V1: hardcodes resolution + factoring + subsumption.
+/// V2: will accept a Calculus object for pluggable inference rules.
+class Prover {
+  public:
+    Prover(TermBank& bank, ClauseStore& store, ProverConfig config = {});
+
+    /// Add initial clauses (axioms + negated conjecture).
+    void addClauses(std::vector<Clause> clauses);
+
+    /// Run the proof search.
+    ProverResult prove();
+
+    /// After a successful proof, retrieve the empty clause ID.
+    [[nodiscard]] std::optional<ClauseId> getEmptyClauseId() const;
+
+    /// Access the underlying clause store.
+    [[nodiscard]] const ClauseStore& clauseStore() const { return store_; }
+
+  private:
+    [[nodiscard]] bool hitResourceLimit(size_t iterations) const;
+    [[nodiscard]] Clause popGivenClause();
+    [[nodiscard]] bool isForwardSubsumedByProcessed(const Clause& clause) const;
+    [[nodiscard]] bool shouldSkipGiven(const Clause& given) const;
+    void applyBackwardSubsumption(const Clause& given);
+    [[nodiscard]] std::vector<Clause> generateNewClauses(const Clause& given) const;
+    [[nodiscard]] uint16_t computeDepth(const Clause& clause) const;
+    [[nodiscard]] std::optional<ClauseId> processNewClauses(std::vector<Clause> new_clauses);
+
+    TermBank& bank_;
+    ClauseStore& store_;
+    ProverConfig config_;
+    std::priority_queue<Clause, std::vector<Clause>, ClauseComparator> unprocessed_;
+    std::vector<ClauseId> processed_;
+    std::optional<ClauseId> empty_clause_id_;
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/simplify/subsumption.h b/proofsearch/include/atp/simplify/subsumption.h
new file mode 100644
index 0000000..970b6d8
--- /dev/null
+++ b/proofsearch/include/atp/simplify/subsumption.h
@@ -0,0 +1,56 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file subsumption.h
+/// @brief Forward and backward subsumption checks (backed by discrimination tree).
+
+#include "atp/core/clause.h"
+#include "atp/index/discrim_tree.h"
+
+#include <vector>
+
+namespace atp {
+
+/// Subsumption engine: checks if a new clause is subsumed by existing ones
+/// (forward) or subsumes existing ones (backward).
+class SubsumptionEngine {
+  public:
+    explicit SubsumptionEngine(const TermBank& bank);
+
+    /// Returns true if `candidate` is subsumed by any existing clause.
+    [[nodiscard]] bool isForwardSubsumed(const Clause& candidate) const;
+
+    /// Returns IDs of existing clauses that are subsumed by `new_clause`.
+    [[nodiscard]] std::vector<ClauseId> backwardSubsumed(const Clause& new_clause) const;
+
+    /// Add a clause to the subsumption index.
+    void addClause(const Clause& clause);
+
+    /// Remove a clause from the subsumption index.
+    void removeClause(ClauseId id);
+
+  private:
+    DiscrimTree index_;
+    // TODO: Phase 5 implementation
+};
+
+bool subsumes(const Clause& general, const Clause& specific);
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/simplify/tautology.h b/proofsearch/include/atp/simplify/tautology.h
new file mode 100644
index 0000000..f17f0c7
--- /dev/null
+++ b/proofsearch/include/atp/simplify/tautology.h
@@ -0,0 +1,31 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file tautology.h
+/// @brief Tautology detection for clauses.
+
+#include "atp/core/clause.h"
+
+namespace atp {
+
+/// Returns true if the clause is a tautology (contains complementary literals).
+[[nodiscard]] bool isTautology(const Clause& clause);
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/strategy/calculus.h b/proofsearch/include/atp/strategy/calculus.h
new file mode 100644
index 0000000..e06988e
--- /dev/null
+++ b/proofsearch/include/atp/strategy/calculus.h
@@ -0,0 +1,67 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file calculus.h
+/// @brief A Calculus bundles the exact set of inference rules + heuristics
+///        to use for a specific problem class.
+///
+/// Think of it as the "algorithm profile" that the Prover loads.
+/// Different problems get different calculi:
+///   - Pure propositional:  resolution + factoring only
+///   - FOL without equality: + full unification
+///   - FOL with equality:   + paramodulation + KBO ordering
+///   - Arithmetic:          + theory solver integration
+///
+/// This is the single point where search space control happens.
+
+#include "atp/rewrite/ordering.h"
+#include "atp/search/clause_queue.h"
+#include "atp/strategy/inference_rule.h"
+
+#include <memory>
+#include <string_view>
+#include <vector>
+
+namespace atp {
+
+/// A Calculus = a complete specification of how to search for a proof.
+/// The Prover is parameterized by this — it never hardcodes which rules to use.
+struct Calculus {
+    /// Name for logging (e.g., "superposition", "pure_resolution").
+    std::string name;
+
+    /// Generating rules (executed in order during the main loop).
+    std::vector<std::unique_ptr<GeneratingRule>> generating_rules;
+
+    /// Simplifying rules (applied to each new clause before enqueuing).
+    std::vector<std::unique_ptr<SimplifyingRule>> simplifying_rules;
+
+    /// Clause selection heuristic.
+    ClauseComparator comparator = bfsCompare;
+
+    /// Term ordering (nullptr if equality reasoning is disabled).
+    std::unique_ptr<TermOrdering> ordering = nullptr;
+
+    /// Resource limits.
+    size_t max_clauses = 100000;
+    size_t max_iterations = 500000;
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/strategy/inference_rule.h b/proofsearch/include/atp/strategy/inference_rule.h
new file mode 100644
index 0000000..88b6fe0
--- /dev/null
+++ b/proofsearch/include/atp/strategy/inference_rule.h
@@ -0,0 +1,80 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file inference_rule.h
+/// @brief Abstract interface for pluggable inference rules.
+///
+/// Each inference rule (resolution, factoring, paramodulation, etc.)
+/// is a self-contained object that the Prover can selectively load.
+/// This prevents search space explosion by only enabling rules relevant
+/// to the problem at hand.
+
+#include "atp/core/clause.h"
+#include "atp/core/clause_store.h"
+#include "atp/core/term_bank.h"
+
+#include <string_view>
+#include <vector>
+
+namespace atp {
+
+/// Abstract base class for all inference rules.
+/// The Prover invokes only the rules present in its active calculus.
+class InferenceRuleBase {
+  public:
+    virtual ~InferenceRuleBase() = default;
+
+    /// Human-readable name for logging and proof output.
+    [[nodiscard]] virtual std::string_view name() const = 0;
+
+    /// Is this a generating rule (produces new clauses) or simplifying rule
+    /// (rewrites/deletes existing clauses)?
+    enum class Kind : uint8_t { kGenerating, kSimplifying };
+    [[nodiscard]] virtual Kind kind() const = 0;
+};
+
+/// Generating inference rule: given a "given clause" and the set of processed
+/// clauses, produce new clauses.
+class GeneratingRule : public InferenceRuleBase {
+  public:
+    [[nodiscard]] Kind kind() const final { return Kind::kGenerating; }
+
+    /// Generate new clauses from the given clause against all processed clauses.
+    /// @param given     The selected clause from the Unprocessed queue.
+    /// @param processed All previously processed clauses (accessed via store).
+    /// @param bank      The global term bank.
+    /// @return Newly generated clauses (not yet added to the store).
+    [[nodiscard]] virtual std::vector<Clause> generate(const Clause& given,
+                                                       const std::vector<ClauseId>& processed,
+                                                       const ClauseStore& store,
+                                                       TermBank& bank) const = 0;
+};
+
+/// Simplifying inference rule: rewrite or delete a clause in-place.
+class SimplifyingRule : public InferenceRuleBase {
+  public:
+    [[nodiscard]] Kind kind() const final { return Kind::kSimplifying; }
+
+    /// Attempt to simplify a clause. Returns true if the clause was modified.
+    /// If the clause should be deleted entirely, clear its literals.
+    virtual bool simplify(Clause& clause, const ClauseStore& store, TermBank& bank) const = 0;
+};
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/strategy/problem_analyzer.h b/proofsearch/include/atp/strategy/problem_analyzer.h
new file mode 100644
index 0000000..5e6c5cf
--- /dev/null
+++ b/proofsearch/include/atp/strategy/problem_analyzer.h
@@ -0,0 +1,61 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file problem_analyzer.h
+/// @brief Analyzes input clauses and selects the optimal Calculus.
+///
+/// Before the Prover starts its main loop, the ProblemAnalyzer inspects
+/// the input clause set to determine problem characteristics:
+///   - Contains equality?             → enable paramodulation
+///   - Pure Horn clauses?             → use SLD resolution
+///   - Contains arithmetic literals?  → enable theory solver
+///   - Problem size / clause density  → tune resource limits
+///
+/// This is the "auto mode" that mature ATPs use to avoid loading
+/// unnecessary inference rules that would explode the search space.
+
+#include "atp/core/clause.h"
+#include "atp/strategy/calculus.h"
+
+#include <vector>
+
+namespace atp {
+
+/// Features detected in the input problem.
+struct ProblemFeatures {
+    bool has_equality = false;             ///< Contains '=' predicate
+    bool is_purely_propositional = false;  ///< No function symbols, no variables
+    bool is_horn = false;                  ///< All clauses are Horn clauses
+    bool has_existential = false;          ///< Had existential quantifiers (Skolemized)
+    size_t num_clauses = 0;
+    size_t num_predicates = 0;
+    size_t num_functions = 0;
+    size_t max_clause_size = 0;
+    size_t max_term_depth = 0;
+};
+
+/// Analyze the input clauses and extract problem features.
+ProblemFeatures analyzeFeatures(const std::vector<Clause>& clauses, const TermBank& bank);
+
+/// Select the optimal calculus based on detected features.
+/// This is the core strategy dispatch logic.
+std::unique_ptr<Calculus> selectCalculus(const ProblemFeatures& features);
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/utils/hash_utils.h b/proofsearch/include/atp/utils/hash_utils.h
new file mode 100644
index 0000000..ae31f43
--- /dev/null
+++ b/proofsearch/include/atp/utils/hash_utils.h
@@ -0,0 +1,46 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file hash_utils.h
+/// @brief Hash combination utilities.
+
+#include <cstddef>
+#include <cstdint>
+#include <functional>
+
+namespace atp {
+
+/// Combine a hash with a new value (boost::hash_combine style).
+inline void hashCombine(size_t& seed, size_t value) {
+    seed ^= value + 0x9e3779b9 + (seed << 6) + (seed >> 2);
+}
+
+/// Hash a span of values.
+template <typename T>
+size_t hashRange(const T* data, size_t count) {
+    size_t seed = 0;
+    std::hash<T> hasher;
+    for (size_t i = 0; i < count; ++i) {
+        hashCombine(seed, hasher(data[i]));
+    }
+    return seed;
+}
+
+}  // namespace atp
diff --git a/proofsearch/include/atp/utils/logger.h b/proofsearch/include/atp/utils/logger.h
new file mode 100644
index 0000000..de77c54
--- /dev/null
+++ b/proofsearch/include/atp/utils/logger.h
@@ -0,0 +1,41 @@
+/*
+ * 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/>.
+ */
+
+#pragma once
+
+/// @file logger.h
+/// @brief Minimal high-performance logging macros.
+
+#include <cstdio>
+
+#ifndef ATP_LOG_LEVEL
+#define ATP_LOG_LEVEL 2  // 0=TRACE, 1=DEBUG, 2=INFO, 3=WARN, 4=ERROR
+#endif
+
+#define ATP_LOG(level, level_str, fmt, ...)                                   \
+    do {                                                                      \
+        if constexpr (level >= ATP_LOG_LEVEL) {                               \
+            std::fprintf(stderr, "[%s] " fmt "\n", level_str, ##__VA_ARGS__); \
+        }                                                                     \
+    } while (0)
+
+#define ATP_TRACE(fmt, ...) ATP_LOG(0, "TRACE", fmt, ##__VA_ARGS__)
+#define ATP_DEBUG(fmt, ...) ATP_LOG(1, "DEBUG", fmt, ##__VA_ARGS__)
+#define ATP_INFO(fmt, ...) ATP_LOG(2, "INFO", fmt, ##__VA_ARGS__)
+#define ATP_WARN(fmt, ...) ATP_LOG(3, "WARN", fmt, ##__VA_ARGS__)
+#define ATP_ERROR(fmt, ...) ATP_LOG(4, "ERROR", fmt, ##__VA_ARGS__)