ratp - A saturation-based automated theorem prover for first-order logic.

	Commit message (Expand)	Author	Age	Files	Lines
*	feat: enhance clang-tidy configuration and improve code quality across multip...HEAD master	Richard Qin	2026-04-08	7	-150/+163
*	refactor: rename struct members to follow trailing underscore naming conventi...	Richard Qin	2026-04-07	12	-241/+297
*	style: reformat codebase with consistent indentation	Richard Qin	2026-04-04	17	-177/+186
*	feat: add copyright and license disclaimer to program startup output	Richard Qin	2026-04-04	1	-0/+5
*	feat: implement pretty-printing for variables and proof step references in pr...	Richard Qin	2026-04-04	1	-6/+76
*	feat: implement command-line interface and add end-to-end propositional logic...	Richard Qin	2026-04-04	3	-13/+86
*	feat: implement proof trace extraction and add proof trace test	Richard Qin	2026-04-04	1	-0/+135
*	feat: implement saturation-based resolution loop in Prover class	Richard Qin	2026-04-04	2	-6/+158
*	feat: implement clause subsumption and tautology detection logic with associa...	Richard Qin	2026-04-04	2	-0/+57
*	feat: implement variable renaming and update resolution logic to prevent vari...	Richard Qin	2026-04-04	1	-0/+152
*	feat: implement substitution logic and unify/applySubstitution functions for ...	Richard Qin	2026-04-03	2	-0/+187
*	feat: implement core term, symbol, and clause storage logic with canonicaliza...	Richard Qin	2026-04-03	3	-0/+114
*	refactor: replace string-based formula representation with interned SymbolIds...	Richard Qin	2026-04-02	1	-0/+271
*	Initial commit: Build project architecture, define interfaces, write document...	Richard Qin	2026-04-02	15	-0/+285