Bridging the Gap Between Easy Generation and
Efficient Verification of Unsatisfiability Proofs
Download
The checking tool for proofs in the RUP format:
rup-check.c
The checking tool for proofs in the IORUP format:
iorup-check.c
The tool to converse a proof in DRUP into IORUP:
drup2iorup.c
Files of our ACL2 proof:
acl2-proof