Varol Akman
Ayisigi Sevdik and Emre Sahin
Mon 10:40, 11:40 and Wed 9:40
Also there is this extraordinary book LANGUAGE, PROOF AND LOGIC, by J. Barwise & J. Etchemendy. You can buy it at Meteksan Bookstore. It comes with a CD and maybe a bit on the expensive side but believe me, it is worth every penny you spend.
In the past, I've used THE LANGUAGES OF LOGIC: AN INTRODUCTION TO FORMAL LOGIC, by S. Guttenplan, and LOGIC, LANGUAGE, AND MEANING, by L.T.F. Gamut. The latter consists of 2 volumes and the first volume is especially recommended.
HOMEWORK #1 (assigned Feb 20th, due March 5th)
Implement the basic version of the Davis-Putnam Procedure. ('Basic' means it does not have to be efficient.) There are numerous logic and AI books in our library that you can consult to learn what DPP is all about. A concise yet elegant explanation is given here. Obviously there are several others, e.g. see the AI text of last semester by Russell & Norvig. You must write original code; you should not submit a program that you might find on the Internet. Use any programming language you want. (Here you can find general advice about programming, contributed by your TAs.) Run your program with the following sets of clauses (in other words, these are your minimal test data):
HOMEWORK #2 (assigned Mar 5th, due March 19th)
Read Section 1.5.2 of your textbook carefully. Then write a program which converts any formula phi of propositional logic into an equivalent CNF. [Suggestion: You can do this by calling CNF(NNF(IMPL_FREE(phi ))).] Test your algorithm using the two example formulas given on pages 81 and 82 and the formula given in Exercise 3 (page 84). (Thus a total of three formulas! Note that this is a minimal requirement; obviously you should consider testing your program with other examples.)
HOMEWORK #3 (assigned Mar 31st, due April 9th)
Solve the following 5 exercises (try to be as formal as possible):
2.4.3 2.5.1(e) 2.5.7(d) 2.6.1 2.7.2
You must use a decent document processor to make sure that the logical symbols and formulas have a respectable look. You'll lose points if your solutions do not appear mathematical.
HOMEWORK #4 (assigned Apr 21st, due April 28th)
Familiarize yourself with the Logic Quiz Master that you'll find in this address. Your homework is to solve five problems using this utility. The problems should all belong to "Predicate Logic". Two of the problems should be selected from Chapter Three and three should be selected from Chapter Four (of that book, obviously). They should all be random problems. Give enough screen shots for each problem (i) to make sure that we understand what the problem was and (ii) to prove that you have indeed solved it yourself. Do not login as anonymous. Using your own names would make life easier for us. (Thus, if Ali and Ayse are partners in this homework, they can login as Ali-Ayse.) You may want to visit http://logic.tamu.edu for more info. Reading the introduction http://logic.tamu.edu/Primer may be useful too.
HOMEWORK #5 (assigned May 5th, due May 12th)
Write SMV code for mutual exclusion (assume two processes only). Verify the four properties of safety, liveness, non-blocking and no strict sequencing for both processes. In other words, you have to write eight CTL formulas (four for process #1 and four for process #2) and get them to evaluate to 'true' by SMV. Adopt the second modeling attempt for mutual exclusion (see Fig.3.13). You must provide a snapshot of your SMV run, along with your (commented) code.
SMV can be found at http://www-2.cs.cmu.edu/~modelcheck/smv.html
In this homework I won't be answering any questions in order to see how well you can cope with uncertainty and omitted details. Just attempt to do your best.
HOMEWORK #6 (assigned May 17th, due May 24th)
Solve exercises 4.6.1 (about Copy1) and 4.6.2 (about Mult1). Do not forget to explain how you have discovered an invariant for each program.
