Skip to content

Home

Jump to bottom
areivaX edited this page Apr 2, 2017 · 5 revisions

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.

Clone this wiki locally