aboutsummaryrefslogtreecommitdiff
path: root/proofsearch/include
Commit message (Collapse)AuthorAgeFilesLines
* feat: implement variable renaming and update resolution logic to prevent ↵Richard Qin2026-04-041-3/+9
| | | | variable collisions
* feat: implement substitution logic and unify/applySubstitution functions for ↵Richard Qin2026-04-032-10/+36
| | | | term resolution
* feat: implement core term, symbol, and clause storage logic with ↵Richard Qin2026-04-034-14/+51
| | | | canonicalization support
* refactor: replace string-based formula representation with interned ↵Richard Qin2026-04-024-24/+117
| | | | SymbolIds and introduce stateful Clausifier for TPTP parsing
* Initial commit: Build project architecture, define interfaces, write ↵Richard Qin2026-04-0226-0/+1451
documentation, with the help of Claude