Proofs and Proof Systems
Due on Monday, September 20th at 11:59 PM. This is a team lab. You may work alone or you may work with a partner. If you’d like to work with a partner, make sure to indicate your preferred partner using Teammaker and be familiar with the Partner Etiquette guidelines. You may discuss the concepts of this lab with other classmates, but you may not share your code with anyone other than course staff and your lab partner(s). Do not look at solutions written by students other than your team. If your team needs help, please post on Slack or contact the instructor. If you have any doubts about what is okay and what is not, it’s much safer to ask than to risk violating the Academic Integrity Policy.
Overview
In this lab, we will practice with inference rules and proof systems. You will use inference rules to construct proofs; you will also construct some inference rules of your own. We will also use inference rules to define some relations.
Teams and Repositories
We will be using Teammaker to form groups to work on this assignment. When you log in to that system, you’ll have the opportunity to select someone to work with on each assignment in the course. (Assignments will be added to the list incrementally as the course proceeds.)
As with previous assignments, you will submit your work by committing and pushing to a Git repository. The URL for that repository will appear in Teammaker once you a team has been formed. If you have any trouble getting access to your Git repository or questions about how this process works, please contact your instructor.
LaTeX
We will use LaTeX throughout this course to typeset our written work. LaTeX is a peculiar sort of programming language designed to produce consistent, easy-to-read documents. The LaTeX you will need for this course is minimal and is covered in the LaTeX Guide.
If you need to experiment with LaTeX, a file called sandbox.tex has been provided so that you can try some things out and see how they work. There is also a LearningLaTeX.tex file that contains a small tutorial document for you to use for examples. To make either of these files into a PDF, you simply give the name of the PDF to the Makefile (e.g make LearningLaTeX.pdf).
Developing Your Document
Your starting repository has a document assignment2.tex which contains the questions for this assignment. As this document is written in LaTeX, it must be compiled into a PDF for you to read it. For this reason, a Makefile is provided which will build your document for you (provided that you have no errors in your sources). Run make assignment2.pdf in order to build that document; you can then open assignment2.pdf to read the questions.
Your starting repository contains an outline for the document answers.tex you will be creating to complete this assignment. If you run make, a file named answers.pdf will appear in your directory. Make sure to put your answers in answers.tex so that you’ll still be able to read the assignment even if your answers contain LaTeX errors.
Probably the best way to work on this assignment is to run make, open answers.pdf, and then make edits and re-run make as you go. Most PDF viewers (such as evince on the CS network systems) will notice when the PDF has changed and reload it for you, allowing you to see the effects of each of your changes. As always, please ask if you have difficulties with this!
The Actual Assignment
The work in this assignment is expressed in the document template that you will receive when Teammaker creates your repository. Complete each of the questions which appear in assignment2.pdf and ensure that your final PDF builds properly through make. Make sure to contact your instructor if you encounter any troubles in building your PDF. You will not receive full credit if your submission does not compile.
Submitting
To submit your lab, just commit and push your work. The most recent pushed commit as of the due date will be graded. For more information on when assignments are due, see the Policies page.
Lab Questionnaire
In addition to completing the lab itself, you’ll also need to complete a questionnaire describing your experience in the lab. Under most circumstances, this questionnaire will take only about a minute to complete and is part of your participation grade. Please make sure to do this; the information is useful to develop the course and the credit you get is basically free!
If You Have Trouble…
…then please contact your instructor! Slack is the preferred method, but you can reach out via e-mail as well. Good luck!