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
/
tests
Commit message (
Collapse
)
Author
Age
Files
Lines
*
feat: enhance clang-tidy configuration and improve code quality across ↵
HEAD
master
Richard Qin
2026-04-08
1
-0
/
+1
|
|
|
|
multiple files
*
refactor: rename struct members to follow trailing underscore naming ↵
Richard Qin
2026-04-07
7
-519
/
+531
|
|
|
|
convention across core, search, and frontend components
*
style: reformat codebase with consistent indentation
Richard Qin
2026-04-04
9
-71
/
+34
|
*
feat: implement pretty-printing for variables and proof step references in ↵
Richard Qin
2026-04-04
1
-2
/
+2
|
|
|
|
proof trace output
*
feat: implement command-line interface and add end-to-end propositional ↵
Richard Qin
2026-04-04
1
-0
/
+184
|
|
|
|
logic test suite
*
feat: implement proof trace extraction and add proof trace test
Richard Qin
2026-04-04
2
-0
/
+220
|
*
feat: implement saturation-based resolution loop in Prover class
Richard Qin
2026-04-04
1
-0
/
+179
|
*
feat: implement clause subsumption and tautology detection logic with ↵
Richard Qin
2026-04-04
2
-0
/
+190
|
|
|
|
associated unit tests
*
feat: implement variable renaming and update resolution logic to prevent ↵
Richard Qin
2026-04-04
1
-0
/
+238
|
|
|
|
variable collisions
*
feat: implement substitution logic and unify/applySubstitution functions for ↵
Richard Qin
2026-04-03
1
-0
/
+337
|
|
|
|
term resolution
*
feat: implement core term, symbol, and clause storage logic with ↵
Richard Qin
2026-04-03
1
-0
/
+316
|
|
|
|
canonicalization support
*
Initial commit: Build project architecture, define interfaces, write ↵
Richard Qin
2026-04-02
7
-0
/
+141
documentation, with the help of Claude
