Proofs and Proof Systems
Due on Thursday, September 25th at 11:59 PM. This is an individual lab. You are to complete this lab on your own, although you may discuss the lab concepts with your classmates. Remember the Academic Integrity Policy: do not show your work to anyone outside of the course staff and do not look at anyone else’s work for this lab. If you need help, please post on Courselore or contact the instructor. If you have any doubts about what is okay and what is not, it’s much safer to ask and learn than it is to guess!
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.
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. You can access your starter repository with a document template via the usual sort of command:
git clone git@github.swarthmore.edu:cs73-f25/lab03-<username>
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 assignment3.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 assignment3.pdf in order to build that document; you can then open assignment3.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. You may use whatever LaTeX editor you find most appropriate to work on your assignment but, if you use an editor external to the CS network (such as Overleaf), please remember that your document is still expected to compile on the CS network computers. As always, please ask if you have difficulties with editing or compiling your document!
The Actual Assignment
The work in this assignment appears in the document template in your repository. Complete each of the questions which appear in assignment3.pdf, writing your answers in answers.tex, and ensure that your final answers.pdf builds properly through make. Make sure to contact your instructor if you encounter any troubles in building your PDF. Submissions which do not compile will not qualify.
Submitting
It is not enough to push your work. In your repository, you will find a Python script called submit.py. In order to submit your lab assignment, it should be sufficient to run that script by typing python3 submit.py in your terminal. For this script to work correctly, you must have committed all uncommitted files in your repository and pushed your work so that your repository is in sync with your GitHub remote repository.
The aforementioned Python script is designed to create a Git tag: a name for a specific commit in your repository. (The script also performs a series of checks to help ensure that the tag you create contains what you likely think it contains.) The tag will be named using the words “submission”, the name of your assignment, and a version number. Your instructor will know that you have submitted your work because this tag will appear in your repository. If you need to resubmit your work to correct changes after receiving a grade, you can simply create new commits and then create another tag (preferrably with submit.py). At any given time, only your most recent outstanding submission will be graded.
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 lets me know whether I’m asking for the right amount of work and helps to ensure that it’s a good use of your time.
If You Have Trouble…
…then please contact your instructor! Courselore is the preferred method, but you can reach out via e-mail as well. Good luck!