15-815 Automated Theorem Proving
Assignment 2: A Certifying Decision Procedure

The assignment is worth 80 pts, due Thu Feb 5

For this assignment you may work by yourself or with a partner.

We explore an implementation of Dyckhoff's contraction free sequent calculus as a certifying decision procedure for intuitionistic propositional logic.