Fall 2009 Semester
The Yellow Submarine puzzle:

(What does it prove?)

Logical Foundations of Computing

Lectures: MWF 10:30pm, Nichols Hall, room 122

Instructor: David Schmidt (das @ksu.edu, phone: 532-7912), 219A Nichols Hall

Teaching assistant: Rahul Choubey (rchoubey @ksu.edu)

Announcements (last updated 9 December) | Lectures | Assignments

Syllabus | Course Text | Software Support

Office hours:
Dave Schmidt: Tuesday and Thursday afternoons, 1-3pm (Email me to ask about other times.)
Rahul Choubey: Weds. and Fri., 2pm-3pm, Nichols 19, Desk M.

You are also welcome to send email to schedule meetings with the instructors.

Exam 3 is Monday, December 14, 11:50am.

Course Text

Software Support

While we are studying the on-line text, we will develop examples and case studies with the assistance of a program checker tool that I have written:
  • Download this file to your computer: cis301.zip. It holds the checker. Read the installation guide to learn how to install the checker.
  • Next, read the beginner's guide to using the checker. This should be enough to get you started.
  • The checker runs on top of Python. If you do not have Python installed on your computer, you can download and install it from http://www.activestate.com/activepython. (Download version 2.6.)
  • There's more, if you're curious: Here is the README file that is contained in the zip file. There is also a DOC.txt file that defines precisely the language understood by the checker. The DOC file also includes a series of progressively more fiendish examples that the checker will analyze and approve.
  • If it is impossible for you to unzip cis301.zip, here is the link to the cis301 folder. Download from here as a last resort.

Python is a nice complement to Java, C#, etc., because it is a dynamically typed and structured language rather than a static one, and it naturally supports recursive programming rather than iterative. For this reason, we will do a couple of projects using it. When I taught CIS200, I used Python as the delivery vehicle. Here is some tutorial material to read. There is also this nice on-line book, The Python Standard Libary, that shows you how to use Python to do clever systems hacking and gluing, the sort of stuff not normally taught in courses but is hugely useful in practice.

When we study Chapters 5 and 6 of the on-line text, we will use a tool developed in-house by Mr. Brian Mulanda, Dr. Rod Howell, and Mr. James Thompson for checking logic proofs. The tool runs on top of Java. If you have Java installed on your computer (very likely), then you can download the tool to your Desktop and double-click to start it:

At the end of the course, we will take a quick look at the Prolog programming language. There is a good, easy-to-install implementation at www.swi-prolog.org.