
15317 Constructive Logic

Date  Assignment  Due  Solutions  



Sep 6  Homework 1: Natural Deduction (Tutch requirements, LaTeX)  Thu Sep 13  Tutch, Written  
Sep 13  Homework 2: Proof Terms and Substitution (Tutch requirements, LaTeX)  Thu Sep 20  Tutch, Written  
Sep 20  Homework 3: Quantifiers and Metatheorems (Tutch requirements, LaTeX)  Thu Sep 27  Tutch, Written  
Sep 27  Homework 4: Sequent Calculus and Natural Numbers (LaTeX)  Thu Oct 4  Written  
Oct 12  Homework 5: Classical Logic (LaTeX)  Thu Oct 18  Written  
Oct 18  Homework 6: Sequent Calculus for Proof Search (Starter code, Test harness)  Thu Oct 25  SML  
Oct 26  Homework 7: Logic Programming in Prolog (Starter code)  Thu Nov 1  Prolog  
Nov 1  Homework 8: Logic Programming in Elf (Starter Code)  Thu Nov 8  Elf  
Nov 20  Homework 9: Dependent Representations (LaTeX, Starter Code)  Thu Nov 29  Elf, Written  
Nov 29  Homework 10: Bracket Abstraction in Twelf (Starter Code)  Thu Dec 6  
Nov 29  Homework Twelf: Bracket Abstraction Metatheory (Starter Code)  Fri Dec 7 
All assignments in this course are individual assignments. The work must be your own. Do not copy any parts of the solution from anyone, and do not look at other students solutions. Do not make any parts of your solutions available to anyone and make sure no one else can read your files. We will rigorously apply the university policy on cheating and plagiarism.
We may modify this policy on some specific assignments. If so, it will be clearly stated in the assignment.
It is always permissible to clarify vague points in assignments, discuss course material from notes or lectures, and to give help or receive help in using the course software such as proof checkers, compilers, or model checkers.