Course pages 2016–17

Logic and Proof

Course notes (PDF)

Slides (PDF)

A toy theorem-prover coded in ML:

• prover source
• some examples to run

Possibly useful external links:

• MiniSat SAT solver
• SPASS theorem prover
• Z3 theorem prover
• leantap theorem prover