diff options
Diffstat (limited to 'proofsearch/include/atp')
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__) |