15-317: Constructive Logic (Sp'20)

  1. Home
  2. >>
  3. Courses
  4. >>
  5. ConstLog. Sp20
  6. >>
  7. Assignments
Table of Contents
  1. About Assignments
    1. Assignment Schedule
    2. Collaboration and Academic Integrity
    3. Due Dates
  2. Software
    1. Tutch Proof Checker
    2. SML
    3. KeYmaera I
    4. Prolog

About Assignments

Assignment Schedule

The Assignment Schedule is tentative!

Collaboration and Academic Integrity

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. The university policies and procedures on academic integrity will be applied rigorously.

We may modify this policy on some specific assignments. If so, it will be clearly stated in that particular 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.

Due Dates

Assignments generally are posted Tuesday after lecture and are due the following Tuesday. Written homeworks are to be handed in to Gradescope on the due date. Machine-checked assignments must be submitted via Autolab on the due date. We will try our best to return graded homework during the recitations in the following week.

3 late days can be used throughout the semester. Each late day extends the due date of one assignment by 24 hours. Each late day beyond the 3 free ones will deduct 25% from an assignment's total possible score.


Tutch Proof Checker

In the first part of this course you will be using a proof checker called Tutch (short for Tutorial Proof Checker). As the name indicates, it checks the validity of formal proofs (in constructive logic) that users provide in natural deduction.

The easiest way to run Tutch is on linux.andrew.cmu.edu or the Linux cluster machines by typing

  /afs/andrew/course/15/317/bin/tutch -r hw2.req hw2.tut
where hw2.req is the file of required conjectures that we provide and the file hw2.tut contains your proof or proofs of those conjectures.
[ Documentation | Tutch Overview | Examples]
[ Vim syntax | Emacs mode | Arch package using MLton]


For this course we continue to use Standard ML of New Jersey (SML/NJ) that you are familiar with from 15-150 Functional Programming. If you are a masters student and have not taken 15-150 before, you are expected to have acquired a background in functional programming and pick up sufficient proficiency in SML along the way. Run the SML/NJ compiler, e.g., as

  smlnj -m sources.cm
[SML/NJ | SML base library | SML/NJ Libraries]

KeYmaera I

For sequent proofs, you will be using the KeYmaera I theorem prover for constructive logic, which is a sibling of the KeYmaera X theorem prover. KeYmaera I helps you learn how to do intuitionistic sequent calculus proofs. Kudos to Di Wang and Stefan Mitsch for implementing KeYmaera I on top of KeYmaera X.
[KeYmaera I | Cheat Sheet]


For this course we are using GNU Prolog.

The Andrew Linux cluster installation of GNU Prolog on linux.andrew.cmu.edu can be run either by running the script:

or by adding the directory /afs/andrew/course/15/317/bin to your PATH and running gprolog. You can also download a distribution, e.g., from the GNU Prolog web site or directly from your operating system and install it on your own machine.

Most installations of vim and emacs have editing modes for Prolog code, but the default is to treat .pl files as Perl code. Switching files to Prolog mode works as follows:

(setq load-path (cons "~/.emacs.d/prolog.el" load-path))
(autoload 'run-prolog "prolog" "Start Prolog interpreter." t)
(autoload 'prolog-mode "prolog" "Major mode for Prolog." t)
(autoload 'mercury-mode "prolog" "Major mode for Mercury." t)
(setq prolog-system 'gnu)
(add-to-list 'auto-mode-alist '("\\.pl\\'" . prolog-mode))

[GNU Prolog | Documentation | Newsgroup ]