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

	Commit message (Collapse)	Author	Age	Files	Lines
*	feat: enhance clang-tidy configuration and improve code quality across ↵HEAD master	Richard Qin	2026-04-08	3	-6/+16
\| \| \| \|	multiple files
*	refactor: rename struct members to follow trailing underscore naming ↵	Richard Qin	2026-04-07	12	-49/+49
\| \| \| \|	convention across core, search, and frontend components
*	style: reformat codebase with consistent indentation	Richard Qin	2026-04-04	23	-106/+74
\|
*	feat: implement proof trace extraction and add proof trace test	Richard Qin	2026-04-04	1	-9/+10
\|
*	feat: implement saturation-based resolution loop in Prover class	Richard Qin	2026-04-04	2	-4/+12
\|
*	feat: implement clause subsumption and tautology detection logic with ↵	Richard Qin	2026-04-04	1	-0/+2
\| \| \| \|	associated unit tests
*	feat: implement variable renaming and update resolution logic to prevent ↵	Richard Qin	2026-04-04	1	-3/+9
\| \| \| \|	variable collisions
*	feat: implement substitution logic and unify/applySubstitution functions for ↵	Richard Qin	2026-04-03	2	-10/+36
\| \| \| \|	term resolution
*	feat: implement core term, symbol, and clause storage logic with ↵	Richard Qin	2026-04-03	4	-14/+51
\| \| \| \|	canonicalization support
*	refactor: replace string-based formula representation with interned ↵	Richard Qin	2026-04-02	4	-24/+117
\| \| \| \|	SymbolIds and introduce stateful Clausifier for TPTP parsing
*	Initial commit: Build project architecture, define interfaces, write ↵	Richard Qin	2026-04-02	26	-0/+1451
	documentation, with the help of Claude