| MPs for CS 576: Topics in
Automated Deduction (Spring 2010) |
Isabelle is available on the CSIL Linux machines. You may run it
remotely using ssh -Y. To use Isabelle on
csil-linux-ts1.cs.uiuc.edu execute:
/home/class/sp10/cs576/public_html/bin/isabelle emacs -p /home/class/sp10/cs576/public_html/bin/emacs
|
|---|
|
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 to me by email:
egunter@illinois.edu
|
|---|
|
The MPs for the semester have been posted, but they are subject to
modification, or even complete replacement, until officially asigned. In particular, unassigned MPs may be for a previous version of Isabelle.
|
|---|
| MP |
Date Assigned |
Due Date |
Solution |
| MP 0 (mp0.thy) |
Wednesday, 20 January 2010 | Friday, 22 January 2010, 12:01pm
|
| MP 1 (mp1.thy) |
Friday, 22 January 2010 |
Friday, 29 January 2010, 11:59pm |
MP 1 Solution(mp1-sol.thy),
Isar style(mp1-isar-sol.thy) |
| MP 2 (mp2.thy) |
Friday, 29 January 2010 |
Friday, 5 February 2010, 11:59pm |
MP 2 Solution(mp2-sol.thy) |
| MP 3 (mp3.thy) |
Friday, 5 February 2010 |
Friday, 12 February 2010, 11:59pm |
MP 3 Solution(mp3-sol.thy) |
| MP 4 (mp4.thy) |
Friday, 12 February 2010 |
Friday, 19 February 2010, 11:59pm |
MP 4 Solution(mp4-sol.thy) |
| MP 5 (mp5.thy) |
Friday, 19 February 2010 |
informal proof, Friday 26 February Friday,
mp5.thy, 5 March 2010, 11:59pm |
MP 5 Solution(mp5-sol.thy) |
MP 6 (mp6.thy) |
Monday, 8 March 2010 |
Friday, 19 March 2010, 11:59pm |
<MP 6 Solution(mp6-sol.thy) |
|
|