Preliminary Webpage
CS313K Logic, Sets, and Functions
Spring, 2010

Basics

• Catalog Description: Propositional and predicate logic; proof techniques, including induction, sets, relations, and functions.

• Unique Id: 54095 – 54120

• Lecture Meets: TT 3:30 – 5:00, WEL 2.246

• Section Meetings:
  • 54095: Friday, 9:00 – 10:00a, WRW 113
  • 54100: Friday, 10:00 – 11:00a, JES A218A
  • 54105: Friday, 10:00 – 11:00a, SZB 416
  • 54110: Friday, 12:00 – 1:00p, RLM 5.122
  • 54115: Friday, 1:00 – 2:00p, CBA 4.344
  • 54120: Friday, 1:00 – 2:00p, JES A209A

• Supplemental Material Used in Lectures: To Be Determined (wait until the first posting)

• Instructor: J Strother Moore

• Office: TAY 4.140A

• Email: < moore at cs dot utexas dot edu >

• Office Hours: Wednesday 2 pm – 3 pm, Thursday 2 pm – 3 pm, or by appointment

• TAs and Their Office Hours: To Be Determined

• Tutors: For best results, contact tutors in advance to insure that they will be available. To Be Determined

• Important Class Dates:
  • Midterm 1: Thursday, Feb 11, 3:30 – 5:00 pm, Room: To Be Determined
  • Midterm 2: Thursday, Apr 1, 3:30 – 5:00 pm, Room: To Be Determined
  • Final Exam: To Be Determined (at whatever time the University sets for a TT3:30-5:00 class)

Objectives

Textbook

The second lecture will start with a quiz, so you must accomplish all three of the following tasks before class on Thursday, Jan 21! Do not procrastinate.

• Purchase CS313K Notes — Spring, 2010, by J Strother Moore, about $12. When I deliver the master copy to the UT Copy Center, I will put a link to the pdf file here. I strongly recommend you buy a hardcopy to bring to class and mark-up, even though the link above will give you a searchable pdf copy for free.

  UT Copy Center
  Welch Hall, WEL 2.228 (across the hall from the lecture room)
  Hours: 7:30 am – 4:30 pm

  Note: Mistakes in the notes will be corrected in class. You will be expected to be there to hear the corrections and mark your books accordingly.

• Purchase an iClicker (a remote control device) from the Co-op bookstore, about $36

  Beware: There may be several incompatible brands of remote control devices on sale. Be sure you get the “iClicker” brand. To find out more about iClickers, see the company's web site. The Co-op will buy back the iClicker for about half the current price. I recommend that you put a piece of transparent tape across the serial number on the back of your iClicker to prevent it from being rubbed off with use. That serial number is important when you register the iClicker (see the next step) and you want it intact when/if you re-sell the iClicker.

• Register your iClicker (even if you think you already have!) at http://www.iclicker.com/registration/ by providing:
  • your first name
  • your last name
  • your UT EID (which they call your “student ID”)
  • your clicker's ID (the serial number under the bar code on the back of the device)
  If you already have a iClicker and registered it to your EID in the past, you should be aware that iClicker registrations do expire (each July, I believe). It doesn't hurt to re-register each term. If you cannot read the serial number on your iClicker, see me.

Bring your notes, iClicker, some scratch paper, and a pen or pencil to every lecture.

Reading Assignments

This is college. You must read ahead to know what is going on in the lectures. The reading schedule is implicit in the notes. Each section is marked with the date of the lecture at which that section will be discussed.

Every lecture — including the second — will start with an iClicker quiz over the assigned reading and you will be graded on the quizzes. I cannot stress enough the importance of your taking responsibility for the reading.

We're going to cover roughly 240 pages of the notes. The course marches on relentlessly, every lecture covering new material. Keep up!

I will not remind you of the reading from week to week. That is your responsibility! It will sometimes take a day or two or read the material, so I recommend that after every class you look ahead to see what the next reading assignment is and plan your time accordingly before the next class. Do not wait until an hour before class! That won't be enough time.

I may have to change pace of the reading assignments. Changes will be announced in class. Pay attention.

When you read the material, work some of the problems. Program up small examples to test your understanding. Do not study passively! Just reading — without thinking through the consequences of what you're reading — is usually a waste of time.

The quizzes will often refer to the notes and I'll expect you to answer my questions with your clickers. You will be graded on the answers. So be sure you

• read the assigned material before class,
• bring your notes,
• bring your clickers, and
• bring paper and something to write with so you can work out your answers!

Last year (Spring, 2009) I had a rule that if more than half the students answered a quiz question incorrectly, I did not count the question. I've decided that is a bad rule that punishes the best students. This year (Spring, 2010), every question I ask will count.

Attendance

Show up! And bring your clicker! Please sit in the front.

Homework

I reserve the right to change the homework assignments. Changes will be announced in class.

Homework is always due on the Tuesday before class. All homework solutions must be typed in plain ASCII and submitted via the turnin facility. Your solution to the first homework should be named hw1.txt, the second hw2.txt, etc. The text file should start with your name, EID, and a title (e.g. “CS313K Spring 10 Homework i”).

Some symbols we use in class and in the notes are not ASCII, e.g., ∧, ∨, ¬, →, ↔, ∀, ∃, ∈, ⊆, ∩, ∪. There is a table of ASCII substitutes in Appendix D of the notes. For example, you're told there to type “p --> q” for “p→q”, and “(all v p)” for “(∀ v : p)”.

Warning: You will get a 0 for any answer that violates the following rules. Every “formula” must be syntactically well-formed. Nothing should extend beyond the 80th column -- lines should not be truncated or wrap around when viewed in a window 80 characters wide. Finally, if the grader feels that insufficient effort has been made to display a formula sensibly, he or she is free to assign a 0 for that answer even if it is correct! The book discusses this at length in “Syntax” section of Chapter 4.

You may work on your homework in groups, but each person must prepare and turn in his or her own write-up. Working in groups is an excellent way to learn new material, but writing it down yourself is an great way to make sure you understand it. Don't think that you understand because someone in your group understands! And remember, you will work alone during the exams and the only way to do well in the class is to master the material.

It is considered cheating to turn in somebody else's homework as your own. In the CS department, cheating and facilitating cheating by others results in a course grade of F.

Just to be clear:

• You can work together in groups or teams on homework.
• One person might take the lead and write out a proof, debugged by all the participants.
• You might take notes on how the team solved each problem.
• But then sit down by yourself and type your own homework solutions.
• If you realize you don't understand a step in your notes, feel free to ask somebody.
• But what you must not do is copy somebody else's homework file or turn in somebody else's work as your own.

Tools

The first homework assignment contains explicit instructions to get you started with the ACL2 system. It introduces an Eclipse interface to ACL2, called ACL2s, written and maintained by Peter Dillinger, Pete Manolios and Harsh Chamarthi, of Northeastern University, Boston. ACL2s is available on all the CS department's public machines. You may wish to install it on your own laptop but that is not necessary.

Do not be nervous about learning a new programming language. In your careers as CS students and then as computer scientists you will learn new languages regularly! Get used to it!

Note: ACL2 can be run under Emacs and directly from Windows or Unix. You may see me using it that way in class from time to time. But the preferred interface for novices is ACL2s, The ACL2 Sedan for Eclipse. It's called the “sedan” for good reason. Driving full ACL2 is like driving a race car: one mistake and you're in the ditch.

Exams and Scheduled Quizzes

There will be a scheduled quiz in every lecture except the first one and the two lecture periods devoted to the midterms.

Email and Discussion Forum

All students should become familiar with the University's official e-mail student notification policy. I may occasionally use email to communicate with the students in the class and it is your responsibility to keep your UT Direct email address current and to check it frequently and regularly.

Discussion Forum To Be Determined (In Spring, 2009, online discussion forums were organized. If that happens this time, I'll announce it here and in class.)

Grading

Your final score will be the total number of points earned divided by 12.60 and rounded up to an integer. This gives an integer between 0 and 100.

Letter grades will be assigned in the conventional way:

Important Notes

Quiz, homework, and test scores are kept as integers between 0 and 10. When computed from fractions, they are rounded up. For example if you answer 5 questions correctly on a quiz with 6 questions, you will receive ceiling(10 × 5/6) = 9 points, not 8.3 points. Midterm and final exam scores are kept as integers in the range 0 to 100.

Partial credit is not given on quiz answers.

Quiz scores are not curved.

If any student in a lecture is discovered with more than one clicker, the clickers will be confiscated until the situation is sorted out by the instructor. If it is determined that one student was taking quizzes for another it will be considered cheating. The CS department penalty for cheating is a course grade of F and referral to the Dean of Students.

While discussion of the homework problems among students is encouraged, each student must prepare his or her own homework submissions. Turning in somebody else's work as your own is an example of cheating. The CS department penalty for cheating is a course grade of F and referral to the Dean of Students.

If you ever wonder whether some behavior you're contemplating would be considered cheating, don't do it! If it's in this course, ask me. If it's in another course, ask the professor in charge.

Partial credit is not given on homework.

Failure to be in your TA session when attendance is taken, for any reason other than an excused absence, results in a 0 that day. No partial credit is given for late arrivals.

Failure to turn in a homework on time, for any reason other than an excused absence, results in a 0 on that homework. No partial credit is given for late homeworks.

Failure to take a midterm or the final exam will result in a score of 0. Except for excused absences, make up exams will not be scheduled.

No “slip points” are provided. However, it is possible to make an A without perfect performance. See Effects of Various Coping Strategies.

If you are dissatisfied with a grade you receive on an assignment or test, you must submit your complaint via email, along with supporting evidence or arguments, to your TA within one week of the date the teaching staff first attempted to return the assignment or test to you.

Questions about your homework grades are to be sent to your TA.

There are no opportunities for extra credit in this course.

Course grades may be adjusted with pluses and minuses at the instructor's discretion.

(defun score (tax qzx qzv hwx hwv mt1 mt2 fin)

 (declare 
   (xargs
    :guard (and (and (natp tax) (<= tax 15))
                (and (natp qzx) (<= qzx 27))
                (and (rationalp qzv) (<= 0 qzv) (<= qzv 1))
                (and (natp hwx) (<= hwx 14))
                (and (rationalp hwv) (<= 0 hwv) (<= hwv 1))
                (and (rationalp mt1) (<= 0 mt1) (<= mt1 1))
                (and (rationalp mt2) (<= 0 mt2) (<= mt2 1))
                (and (rationalp fin) (<= 0 fin) (<= fin 1)))))

; Returns the final score, between 0 and 100, of a student with
; the indicated performance, where the types of the arguments
; are as given above.  Their meanings are:

; tax = number of TA sessions missed
; qzx = number of Quizzes missed
; qzv = average grade on quizzes taken
; hwx = number of Homeworks missed
; hwv = average grade on homeworks turned in
; mt1 = grade on midterm 1
; mt2 = grade on midterm 2
; fin = grade on final exam

; Note that the function requires fractional inputs between 0 and 1
; to represent the average scores on the quizzes, homeworks, and
; tests. I multiply those by the total number of points available 
; for each category.  In actual grading, we will just sum the number
; of points earned on the quizzes, the homeworks, and the tests.

  (let ((TA 10)
        (QZ 10)
        (HW 10)
        (M1 200)
        (M2 200)
        (FN 300))
  (ceiling
   (* 100
      (/ (+ (* (- 15 tax) TA)
            (* (- 27 qzx) (* qzv QZ))
            (* (- 14 hwx) (* hwv HW))
            (ceiling (* mt1 M1) 1)
            (ceiling (* mt2 M2) 1)
            (ceiling (* fin FN) 1))
         (+ (* 15 TA) (* 27 QZ) (* 14 HW) M1 M2 FN)))
   1)))

(score 2 1 73/100 0 95/100 78/100 85/100 80/100)

Acknowledgements

Mathematical logic, set theory, and function theory are deep intellectual subjects. Some of the greatest minds in computing — Godel, Turing, von Neumann, Minsky, McCarthy, Dijkstra, Knuth, Newell, Rabin, Hoare, Cook, Karp, Emerson, etc., — have made fundamental contributions that can only be expressed in these terms. Some of the deepest insights mankind has had about the nature of truth and the power of computation stem from these subjects. Many of the basic ideas of programming languages and of system design — variables, objects, methods, macros, modularity, recursion, types, interpreters, representation, abstraction — were first explored in the context of mathematical logic.

How to Succeed in CS313K