| Table of Contents |
|---|
About Assignments
- Some assignments may offer additional problems for extra credit, which is recorded separately.
- We will use intangibles, such as active participation in class as well as extra credit for those close to grade boundaries.
- Homeworks may require use of the course software, or simply a write-up with pencil and paper.
- Machine-checked assignments must be submitted via the course software before the start of lecture on the due date.
- For typesetting deductions in LaTeX, we use, for example, bussproofs.sty or LKproof/proof.sty
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 at the beginning of lecture on the due date. Machine-checked assignments must be submitted via the course software before the start of lecture 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 beyond the 3 free ones will deduct 25% from an assignment's total possible score. Each late day extends the due date of one assignment by 24 hours. Late theory homework has to be submitted as a physical copy to Sammi DiNardo in GHC 9118 before the extended due date.
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 that users provide.
On the Andrew computers, Tutch is installed in /afs/andrew/course/15/317/bin. The executable files are tutch, submit and status;
they should work under linux.andrew.cmu.edu and directly on the machines in the cluster with Linux. The easiest way to run them is with
/afs/andrew/course/15/317/bin/tutch filename.tutwhere filename.tut contains your proof or proofs.
[ Documentation | Tutch Overview | Examples]
[ Vim syntax | Emacs mode by Evan Cavallo | Arch package using MLton by Rahul Mann]
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.
[SML/NJ
| SML base library
| SML/NJ Libraries]
Prolog
For this course we are using GNU Prolog.
The Andrew installation of GNU Prolog can be run either by running the script:
/afs/andrew/course/15/317/bin/runprologor 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
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
| Newsgroup
]