' CS 576 (Spring 2015): MPs
CS 576: Topics in Automated Deduction (Spring 2015): MPs
Machine Problems for Spring 2015
MP Date Assigned Due Date Solution
MP 1 (mp1.thy) Thursday, 5 February 2015 Thursday, 12 February 2015, 11:59pm
MP 2 (mp2.thy) Wednesday, 18 February 2015 Wednesday, 25 February 2015, 11:59pm MP 2 Solution(mp2-sol.thy),
MP 3 (mp3.thy) Tuesday, 3 March 2015 Thursday, 12 March 2015, 11:59pm
MP 4 (mp4.thy) Thursday, 12 March 2015 Friday, 20 March 2015, 11:59pm
Instructions for Submitting Assignments
  • In the first part of the semester, there will be a series of weekly machine problems (MPs). Each student is given an svn directory that needs to be checked out at the beginning of the semester to as follows:
    mkdir <working_directory>
    svn co https://subversion.ews.illinois.edu/svn/sp15-cs576/ <your_netid> <working_directory>
  • After the initial checkout, <working_directory> will contain a subdirectory assignments. Once an assignment has been announced, if you do an
    svn up
    you will add a file for the assignment (e.g. mp1.thy). That file will contain a stub and instructions for the theory you are to complete and turn in.
  • Isabelle is available on the EWS Linux machines. You may run it remotely using
    ssh -Y remlnx.ews.illinois.edu
    To use Isabelle on remotely remlnx, execute:
    module load isabelle; isabelle jedit
  • Homeworks will be in the form of theory files to be completed. A completed theory file should have no occurrences of "sorry". Homeworks should be submitted by use of the
    svn commit
    in your svn repository.
  • To do an assignment, you will need to follow the instructions given in the comments in the file for that assignment. Since the mps involve using Isabelle, by default you will need to do them on the ews linux machines. You may find it more convenient to download Isabelle to you own machine should you choose to work on your own machine. Isabelle runs under Linux, Windows and MacOS.
  • To submit an assignment, once you have completed the necessry files as decribed in the assignment instructions, in the assignment directory or the parent directory execute
    svn commit -m "<your comment here>"
    You may restrict svn commit to a specific collection of files and directories by adding a list to the end of the command.
  • You may do multiple commits; the version that is in the repositry at 11:59pm on the due date is that one that will be collected and graded.