15-317 Constructive Logic

  • There are 10 homework assignments
  • Some assignments may offer additional problems for extra credit, which is recorded separately.
  • Extra credit will be considered when determining midterm and final grades for borderline cases.
  • Assignments generally are posted Thursday after lecture and are due the following Thursday.
  • Homeworks may require use of the course software, or simply a write-up with pencil and paper.
  • Machine-checked assignment must be submitted via the course software before the start of lecture on the due date.
  • Written homeworks are to be handed in at the beginning of lecture on the due date.
  • We will try our best to return graded homework during the section following the due date.
  • For typesetting deductions in LaTeX, we use proof.sty
Date Assignment Due Solutions

Sep 4 Homework 1: Natural Deduction (Tutch requirements, LaTeX)   Sep 11 Tutch, Written
Sep 11 Homework 2: Proof Terms and Substitution (Tutch requirements, LaTeX)   Sep 18 Tutch, Written
Sep 18 Homework 3: Quantifiers and Metatheorems (Tutch requirements, LaTeX)   Sep 25 Tutch, Written
Sep 25 Homework 4: Sequent Calculus and Natural Numbers (LaTeX)   Oct 2 Written
Oct 9 Homework 5: Double-Negation Translation (LaTeX)   Oct 16 Written  
Oct 16 Homework 6: Sequent Calculus for Proof Search (Starter code, Test harness)   Oct 23 Written, SML  
Oct 23 Homework 7: Logic Programming in Prolog (Starter code)   Oct 30 Prolog  
Oct 30 Homework 8: Logic Programming in Elf (Starter Code)   Nov 6 Elf  
Nov 13 Homework 9: Modal Logic and Lax Logic (LaTeX)   Nov 27 Written  
Nov 26 Homework 10: Linear Logic (LaTeX)   Dec 4 Written  

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.

[ Home | Schedule | Assignments | Software ]