Home

Trace Checker

Checkers is a program for certifying formal proofs using logic programming.

Trace is a SAT proof format.

In this project, we aim at writing a certifier for the Trace format based on a minimal and trusted kernel, following the ideas of the ProofCert project.

Resources

The following describes the steps we plan to take: Roadmap

Online resources

• A short paper about propositional sequent calculus and proof search.
• SWI-prolog reference manual
• this UCSD course introduces the principles of SAT solvers in a few lessons.
• this series of workshops on SAT isn't directly helpful to my project, but has interesting news and further resources on advances in SAT research and applications. When I have some time I'll come back and read some of the articles.