index
:
ratp
master
A saturation-based automated theorem prover for first-order logic.
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
include
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
3
-6
/
+16
*
refactor: rename struct members to follow trailing underscore naming conventi...
Richard Qin
2026-04-07
12
-49
/
+49
*
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 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