ratp/include/atp/infer/resolution.h, branch master
A saturation-based automated theorem prover for first-order logic.
https://git.richardqin.org/ratp/atom?h=master
2026-04-03T21:21:26Z
style: reformat codebase with consistent indentation
2026-04-03T21:21:26Z
Richard Qin
richard.qin.x@gmail.com
2026-04-03T21:21:26Z
urn:sha1:bf4f464cec8b6515d9e5131d43847ef9b2fd21d1
feat: implement saturation-based resolution loop in Prover class
2026-04-03T20:52:36Z
Richard Qin
richard.qin.x@gmail.com
2026-04-03T20:52:36Z
urn:sha1:ae88efa5d8e100c05dcba1f9a7bb9ff840b47d66
feat: implement variable renaming and update resolution logic to prevent variable collisions
2026-04-03T18:33:26Z
Richard Qin
richard.qin.x@gmail.com
2026-04-03T18:33:26Z
urn:sha1:3c1582035a2acf1b2406e62eccacb1d07429de15
Initial commit: Build project architecture, define interfaces, write documentation, with the help of Claude
2026-04-01T20:10:53Z
Richard Qin
richard.qin.x@gmail.com
2026-04-01T20:10:53Z
urn:sha1:26da267b732e28e4d9697278e735b410e50e5e08