15-317 Constructive Logic
Assignments
- There are 10 homework assignments, worth a total of 400 points.
- 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 lecture following
the due date.
- For typesetting deductions in LaTeX, we use
proof.sty
| Date |
Assignment |
Due |
Solutions |
|
|
| Sep 2 |
Homework 1 Natural Deduction
(Tutch requirements,
LaTeX)
|
Thu Sep 9 |
Tutch, Written |
| Sep 9 |
Homework 2 Proof Terms, Quanifiers, and
Substitution
(Tutch requirements,
LaTeX)
|
Thu Sep 16 |
Tutch,
Written |
| Sep 16 |
Homework 3 Natural Numbers and Sequent
Calculus
(Tutch requirements,
LaTeX)
|
Thu Sep 23 |
Tutch,
Written |
| Sep 23 |
Homework 4
Sequent Calculus Metatheory
(LaTeX)
|
Thu Sep 30 |
Written |
|
| Oct 8 |
Homework 5
Classical Logic and Inversion
(LaTeX) |
Thu Oct 14 |
Written |
|
| Oct 14 |
Homework 6
Sequent Calculus for Proof Search
(Starter code,
Test harness,
LaTeX) |
Thu Oct 21 |
Written,
Code |
|
| Oct 21 |
Homework 7
Logic Programming in Prolog
(LaTeX) |
Thu Oct 28 |
Written,
Prolog
|
|
| Oct 29 |
Homework 8
Logic Programming in Elf
(LaTeX,
Starter Code) |
Thu Nov 4 |
Elf |
|
| Nov 13 |
Homework 9
Dependent Representations
(LaTeX,
Starter Code) |
Mon Nov 22 |
Elf,
Written |
|
| Nov 19 |
Homework 10
Bracket Abstraction in Twelf
(LaTeX,
Starter Code) |
Thu Dec 2 |
Elf |
|
| Nov 23 |
Homework Twelf
Bracket Abstraction Metatheory
(Starter Code) |
Fri Dec 3 |
Elf |
|
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
]
|