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

	Commit message (Expand)	Author	Age	Files	Lines
*	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 associa...	Richard Qin	2026-04-04	1	-0/+2
*	feat: implement variable renaming and update resolution logic to prevent vari...	Richard Qin	2026-04-04	1	-3/+9
*	feat: implement substitution logic and unify/applySubstitution functions for ...	Richard Qin	2026-04-03	2	-10/+36
*	feat: implement core term, symbol, and clause storage logic with canonicaliza...	Richard Qin	2026-04-03	4	-14/+51
*	refactor: replace string-based formula representation with interned SymbolIds...	Richard Qin	2026-04-02	4	-24/+117
*	Initial commit: Build project architecture, define interfaces, write document...	Richard Qin	2026-04-02	26	-0/+1451