15-317: Constructive Logic - About Assignments

Table of Contents
About Assignments Assignment Schedule Software Tutch Proof Checker SML KeYmaera I Prolog Exams

About Assignments

Homeworks may require use of the course software, or a write-up as a PDF.
Machine-checked assignments must be submitted via the course software on the due date.
Written parts of the assignments must be submitted in PDF on the due date.
You are strongly encouraged to typeset your homework solutions. Pdf scans of handwritten homework solutions of a similarly high quality will be accepted. Without exception, messy or confusing or unreadable proofs, however, will be rejected without review, because we cannot give any credit if we cannot read it.
For typesetting deductions in LaTeX, we use proof.sty but you may prefer other LaTeX packages.
[proof.sty | example | mathpartir.sty | example | bussproofs.sty | example]

Assignment Schedule

The Assignment Schedule is tentative!

Software

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]

SML

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 Help | SML base library]

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]

Prolog

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:

  /afs/andrew/course/15/317/bin/gprolog

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:

vim: :setf prolog
Emacs: M-x prolog-mode
enables the Prolog menus and ^C ^L consults the current file with Prolog. If that does not work, install prolog mode for emacs and add it:

(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]

Exams

The course contents are different, so not all questions are applicable. You may benefit from some practice exams regardless, though.

Midterm I [F08 | F15 | F16]
Solutions [F09 | F13 | F14 | F15 | F16]
Midterm II [F08 | F15 | F16]
Solutions [F09 | F13 | F14 | F15 | F16]
Final [F09 | F12 | F14 | F15 | F16]
Solutions [F09 | F15 | F16]

Previous practice exams without solutions (solutions blanked out by Marjorie Carlson)

15-317: Constructive Logic (Sp'21)