aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* feat: enhance clang-tidy configuration and improve code quality across ↵HEADmasterRichard Qin2026-04-0813-159/+198
| | | | multiple files
* refactor: rename struct members to follow trailing underscore naming ↵Richard Qin2026-04-0731-809/+877
| | | | convention across core, search, and frontend components
* style: reformat codebase with consistent indentationRichard Qin2026-04-0449-354/+294
|
* feat: add copyright and license disclaimer to program startup outputRichard Qin2026-04-041-0/+5
|
* feat: implement pretty-printing for variables and proof step references in ↵Richard Qin2026-04-042-8/+78
| | | | proof trace output
* feat: implement command-line interface and add end-to-end propositional ↵Richard Qin2026-04-045-13/+275
| | | | logic test suite
* feat: implement proof trace extraction and add proof trace testRichard Qin2026-04-044-9/+365
|
* feat: implement saturation-based resolution loop in Prover classRichard Qin2026-04-045-10/+349
|
* feat: implement clause subsumption and tautology detection logic with ↵Richard Qin2026-04-046-0/+250
| | | | associated unit tests
* feat: implement variable renaming and update resolution logic to prevent ↵Richard Qin2026-04-043-3/+399
| | | | variable collisions
* feat: implement substitution logic and unify/applySubstitution functions for ↵Richard Qin2026-04-036-10/+561
| | | | term resolution
* feat: implement core term, symbol, and clause storage logic with ↵Richard Qin2026-04-038-14/+481
| | | | canonicalization support
* fix: remove files that should be ignoredRichard Qin2026-04-0317-0/+0
|
* refactor: replace string-based formula representation with interned ↵Richard Qin2026-04-027-24/+416
| | | | SymbolIds and introduce stateful Clausifier for TPTP parsing
* Initial commit: Build project architecture, define interfaces, write ↵Richard Qin2026-04-0274-0/+3476
documentation, with the help of Claude
generated by cgit v1.2.3 (git 2.46.0) at 2026-10-28 22:29:14 +0000