Final Exam. The final exam will take place this week. Time: Thursday 14 December 2017 from 12:15 - 3:15 pm. Locations: Gates B01 (last names starting with letter A through letter M) and STLC111 (last names starting with letter N through letter Z) or at your home institutions (for those of you taking the course through SCPD who cannot make it to campus). Closed book, closed notes, closed laptop, etc. Pens and brains only.
The first hour of the period will be devoted to the alternate midterm (which will be focussed on Propositional Logic). The last two hours will be devoted to the actual final (which will be focussed on Relational Logic and Herbrand Logic). If you are not planning to take the alternate midterm, you do not need to show up until 1:15.
Online Exercises. HEADS UP!! You must get your online work done before the final exam. We will take a snapshot of your scores at at that time and use the results in computing your final grade. Any work you do after then will not count toward your grade. No exceptions.
Your overall grade for the course will be based 25% on your performance on the online exercises, 25% on your midterm grade, and 50% on your final grade. For your midterm grade, we will use the higher of your score on the original midterm and your score on the alternate midterm. So, if you aced the first midterm, there is no need to take the alternate. Unless you really love taking exams.
Last week of the quarter. No class this Tuesday. On Thursday, there will be a review session in Gates B01 covering all of the material in the course.
Reminder: The final exam will take place next week. Time: Thursday 14 December 2017 from 12:15 - 3:15 pm. Recall that the first hour of the exam will be devoted to a make-up midterm and the second two hours will be devoted to the final. You can skip the first hour if you have already taken the midterm and are satisfied with your grade (in which case you can show up at 1:15), but you must be there for the final.
Welcome back. Our primary job this week is to look at resolution theorem proving for Herbrand Logic. Herbrand Resolution is a streamlined proof system analogous to Propositional Resolution. It is easier to use than Fitch, and it is ideal for automation. However, the proofs are not always as intuitive as with Fitch. That tradeoff between simplicity and intuitiveness of the resulting proofs is why we still use both systems.
This week, we are also releasing the final puzzle of the course - Enlightenment. For those of you who have managed to do the others, this one should be a snap.
Thanksgiving week. Time to step back and think about all of the good things in life - the things for which we are grateful and the things we can do to help others in return. Real significance - no work on the course this week. Unless, of course, you want to spend some time working on more proofs. Great way to have fun with friends and family! We will be back again next week with a look at resolution for Herbrand Logic and some extra material. Happy Thanksgiving.
The language of Herbrand Logic is almost the same as for Relational Logic. The only difference is the addition of functional terms. This may seem like a small change, but those functional terms make all the difference in the world. They make the language more expressive, but they also destroy some of the nice logical and computational properties of Propositional Logic and Relational Logic.
This week, we start our look at proofs for Herband Logic. As we shall see, all of the rules of inference of Relational Logic work for Herbrand Logic as well. However, they alone are not sufficient. We need some additional rules to deal with functional terms. To this end, we look at a new rule of inference this week, viz. induction.
A cautionary note. As we have seen, there is a sound and complete proof procedure for Relational Logic (i.e. Fitch). Unfortunately, this proof procedure, while sound for Herbrand Logic, is not complete. Moreover, even if we add in induction, the procedure is still not complete. In fact, it is possible to show that there is no such sound and complete proof procedure for Herbrand Logic. As so often happens, increases in expressiveness leads to decreases in completeness and computability.
Next week is Thanksgiving week, and we all get to take a break. When we return, we will look at an extension of resolution that works for Herbrand Logic. We will also look at the notion of equality and the relationship between Herbrand Logic and the popular First-Order Logic. And then we will be done.
Meanwhile, in case you need something to do, there is another new puzzle - Chessboard. This puzzle has some elements in common with the Cards puzzle and Safecracking. However, this one is much more difficult, so don't be worried if you don't get it right away. (Some people have reported spending months on the problem.) The good news is that there is a simple and elegant solution (simple once you find it, that is). Good luck.
Relational Logic allows us to axiomatize worlds with varying numbers of objects. The main restriction is that the worlds must be finite (since we have only finitely many constants to refer to these objects).
Often, we want to describe worlds with infinitely many objects. For example, it would be nice to axiomatize arithmetic over the integers or to talk about sequences of objects of varying lengths. Unfortunately, this is not possible due to the finiteness restriction of Relational Logic.
One way to get infinitely many terms is to allow our vocabulary to have infinitely many object constants. While there is nothing wrong with this in principle, it makes the job of axiomatizing things effectively impossible, as we would have to write out infinitely many sentences in many cases.
Starting this week, we explore an alternative to Relational Logic, called Herbrand Logic, in which we can name infinitely many objects with a finite vocabulary. The trick is to expand our language to include not just object constants but also complex terms that can be built from object constants in infinitely many ways. By constructing terms in this way, we can get infinitely many names for objects; and, because our vocabulary is still finite, we can finitely axiomatize some things in a way that would not be possible with infinitely many object constants.
In dealing with Herbrand Logic, we proceed through the same stages as in Propositional Logic and Relational Logic. We start with syntax and semantics. We then discuss evaluation and satisfaction. We see Fitch and Resolution Proof systems for Herbrand Logic, including a new type of rule of inference - mathematical induction.
New puzzle this week - Safecracking. Learn a practical skill in case your other career plans fail. Also, good preparation for the much more difficult puzzle to come next week.
We have finally begun our discussion of Relational Logic. Relational Logic is definitely more complex than Propositional Logic, but it is also more useful. Useful in thinking and communicating and interacting with logic-enabled Computer Systems (some of which as we shall see in the weeks to come).
This week, we begin our look at proofs in Relational Logic. Based on our discussion sessions on Propositional Logic proofs, I think I can say with confidence that at least some of you have found that generating proofs is not easy. Exactly so. Proving things, even very simple things, can be difficult. It depends on the proof system. What is easy in one system is often difficult in another and vice versa. There is no best proof system for all problems. One thing you should take away from these proof exercises is that finding proofs is a process of search in a space of possibilities. Another is a growing sense of confidence that everything that is true *can* be proved (albeit with some difficulty). And perhaps a belief that this search process can be automated (which by and large is correct).
If you just cannot get enough of proofs, take heart. At the end of the course, we will tell you about a website for finding and recording proofs. Stay tuned for more information on this website - on how you can use it and how you can contribute.
As usual, there is a new puzzle this week, entitled Prisoners. Think logically and save as many of your fellow prisoners as possible.
The first part of the course is now done. And the midterm is out of the way. More or less. First of all, we will be going over the questions on the midterm during the discussion session on Tuesday of this week. Second, for those of you who did not do as well on the exam as expected, take heart - you will get another chance. During the first hour of the final exam, there will be another quiz on the same material as the midterm. That part of the final exam is optional. However, if you choose to take that second "midterm", we will use the higher of your score on that exam and your score on the first midterm in computing your final grade. Of course, the second and third hours of the final are required for all.
With those details out of the way, let's move on. At this point, we have reached the end of our treatment of Propositional Logic. Propositional Logic is simple and elegant. It has limitations, but it also has many applications. It is pedagogically valuable in that it provides us with a simple setting in which to look at the main concepts of Logic - syntax and semantics, validity and contingency and unsatisfiability, logical equivalence and entailment and consistency, and proofs. In the weeks ahead, we will be revisiting these concepts in the context of a more complicated logic, and it will be good that we have already examined these concepts in this simpler setting.
This coming week, we begin our look at Relational Logic. This logic is more natural than Propositional Logic, and it has more practical uses. For some, the material may be a bit more difficult. Start early; don't wait till the end of the week. Read the notes. Do the exercises. Come to the discussion sessions to talk about things you find confusing.
You should try to get through the sections and exercises of Lessons 6 and 7 this week. There is some optional material in the lessons (e.g. the Logicians cartoon, Sorority Life, Minefinder and Minefield and Mineplanner, and Pelican Hunters), and we highly recommend that you take a look. Also, there are those puzzles to look at. This week, you should try to solve the Cards puzzle.
Next week, we will look at extending the Fitch system to deal with Relational Logic. And after that we will look at the third and final logic of the course - Herbrand Logic.
Phew. Last week was not an easy week. Especially for those of you seeing formal proofs for the first time. The good news is that, once you get the hang of it, doing proofs becomes a lot easier. Moreover, you can take comfort in knowing that our proof methods are sound and complete. If you manage to find a formal proof of a conclusion, the conclusion *must* be logically entailed; there can be no mistake. Also, if a set of premises logically entails a conclusion, it is always possible to find a formal proof of that conclusion.
A word about the Fitch system used in the course. The rules in this system are easy to use (though it is not always easy to know which ones to use to get a particular result). This contrasts with other systems where just figuring what the rules do is difficult. We chose this version because we thought it would help you learn about the methods, the difficulties, and the joys of doing proofs (when you finally succeed). The system can easily be elaborated with lots of additional rules of inference, making it a lot easier to use on practical problems. There is even a version that supports user-generated rules and meta-theorems, which make it possible to re-use earlier proofs when trying to prove more complicated results. But, before giving you these power tools, we want you to understand the basics.
If you want more practice with proofs, you might show the following results. Those in the first group are trivial. Those in the second group are not trivial but still relatively easy; just be sure you are comfortable with them. Those in the last group are difficult.
This week, we look at another proof system - Propositional Resolution. Like Fitch, Propositional Resolution is sound and complete for Propositional Logic, i.e. everything that is provable is logically entailed and everything that is logically entailed is provable. However, Propositional Resolution is much simpler to use than these other proof systems, and proofs are frequently shorter than proofs in Fitch. For example, given p|q and ~p, it takes multiple steps or so to prove q in Fitch, whereas this can be done in 1 step in Propositional Resolution. That said, some people criticize Propositional Resolution because the proofs are sometimes less intuitive than Fitch proofs. Chacun a son gout. You will either love it or hate it. In any case, it is particularly useful for automating theorem proving - computers love it! And, by the way, it is equivalent to the simple rule of inference we looked at in the Introduction.
Don't forget that the midterm examination will be take place this week. To be clear, it will cover material on chapters 1-5 (inclusive) of the notes. Closed book. No computers. Brains and pens or pencils only. 12:00 to 1:20 this Thursday in Gates B01. Be there or be square.
No puzzle this week. Spend your time preparing for the midterm. After the quiz, we will have some weekly puzzles that are significantly more difficult than any of those you have seen thus far.
By this point, you should have mastered the material in Lessons 1 through 3. From the Introduction, you should be familiar with the main topics of the course - logical languages, logical entailment and logical reasoning, formalization, and automation. From Lesson 2, you should understand the syntax and semantics of Propositional Logic and the notions of evaluation and satisfaction. From Lesson 3, you should understand the concepts of validity, contingency, and unsatisfiability as well as logical equivalence and entailment and consistency.
In fact, you should be more than familiar with this material - ideally, you should be saying to yourself (and others) that, when all is said and done, this stuff is pretty easy. In fact, it *is* easy. There is more difficult material to come; but hopefully, after we have gone through it all, you will think that that is easy too!
This week, we finally get to logical reasoning - rules of inference, linear proofs, hypothetical proofs, and the Fitch system. By the time you are done this week, you should be comfortable doing Fitch proofs; and you should be ready to opine about its strengths and weaknesses.
All of the exercises this week require that you do formal proofs, and many of you will find these exercises to be more challenging that the exercises in preceding weeks. Just remember, when you are doing a proof, first formulate a plan for the proof. Often, this means starting at the end and thinking about how to derive the desired conclusion and then figuring out how to prove the intermediate results you need to prove the final result. If you are having trouble, don't forget to stop by the discussion sessions on Tuesday and/or Thursday.
In case you need a break from proofs, there is a new puzzle for you to work on this week - Nations. This one is relatively easy like the last few puzzles, but there are some more challenging ones coming.
Sharpen your pencils and get out your copybooks; the course begins in earnest now. This week, your goal is to master the material in lessons 2 and 3.
Lesson 2 introduces the syntax and semantics of Propositional Logic as well as the essentials concepts of evaluation and satisfaction. You should get comfortable with the language and you should get comfortable evaluating sentences and finding truth assignments that satisfy those sentences.
Lesson 3 deals with the logical properties of sentences, e.g. validity and satisfiability. And it introduces and distinguishes the central notions of logical equivalence and logical entailment and logical consistency. These ideas are all fairly simple in the context of Propositional Logic; they are more subtle in the context Relational Logic and Herbrand Logic. It is a good idea to ensure you understand them thoroughly before we get to those more complicated logics later in the course.
Note that there are some useful tools available under the Tools tab, notably Babbage (for generating simple truth tables) and Boole (for generating multicolumn truth tables).
Puzzle of the week - Logicians. This one is probably the easiest of the course. Red hats and black hats. Who is wearing which?
Okay. We are on our way! The course begins now. On Tuesday, we will have an introductory lecture on the subject matter of the course and course logistics. On Thursday, we will have our first in-class discussion session.
Your goal this week is to read through the first lesson. This is just an overview, and it is a very easy read. That said, you should not shortchange the material. The lesson talks about the main ideas of Logic and how they relate to each other, and it provides a framework for organizing the rest of the material in the course. After this week, things get more challenging and increase in difficulty as the course goes on, so do not fall behind.
Be sure to do the exercises. This week's exercises are extremely easy. They are there mostly for you to get experience with the technology so that you will be ready to deal with the increasingly substantive exercises to come.
You should also drop by Piazza to check out what others in the class are saying. There are some subtleties in Logic that you can miss and that can lead to confusion. Engaging in discussion on the Piazza forum is a good way to deal with thee subtleties. And, even if you think you understand you, you might consider using Piazza to help others and thus consolidate your understanding of the issues.
Finally, you might want to check out the puzzles. There are eight of these in all, and we will release then one per week. This week's puzzle is Coins. Some of the puzzles are easy; others are more difficult. They are not directly tied to the course material, but there is a strong relationship and solving them does require the techniques discussed in the course. The puzzles are not a required part of the course, but in the past students have found them worthwhile and enjoyable.
CS 157 is a rigorous introduction to Logic from a computational perspective. It shows how to encode information in the form of logical sentences; it shows how to reason with information in this form; and it provides an overview of logic technology and its applications - in mathematics, science, engineering, business, law, and so forth. Topics include the syntax and semantics of Propositional Logic, Relational Logic, and Herbrand Logic, validity, contingency, unsatisfiability, logical equivalence, entailment, consistency, natural deduction (Fitch), mathematical induction, resolution, compactness, soundness, completeness.
This year, we are continuing our experiment with a "flipped classroom" approach to teaching the course. You are expected to go through the online course materials on your own time. There will be no traditional lectures during class time. Instead, we will use that time for review, problem solving, and general discussion.
All of the materials for the course are accessible via "Intrologic" tab at the top of this page. There are links to lessons, interactive exercises, a glossary, logic puzzles, and some logic tools. In order to access this material, you will need to sign up on the site. Please use your Stanford email address, as we will use this correlate your work there with our class lists.
Note that, as you proceed through the online materials, you may occasionally encounter technical problems. Apologies in advance if this happens to you. We are still working on the course. You may get extra credit for reporting such problems (especially if your reports are more constructive than irate).
Collaboration with your fellow students is encouraged. Feel free to discuss the subject matter and the problems either in person or using Piazza. Our experience has shown that it is useful for students to work together to understand the material of the course and to do exercises. Such activity is both acceptable and encouraged. That said, you are expected to submit your own work in this course; and you are responsible for understanding and being able to explain any solutions you submit.
Your grade for the course will be based on your online results, an in-class midterm (during class on October 19 in Gates B01), and an in-class final exam (12:15 - 3:15 on Thursday December 14). The online results will count for 25% of your grade; the midterm, 25%; and the final, 50%. As preparation for the in-class exams, we highly recommend that you review the online exercises, as the problems on the in-class exams closely resemble these exercises.
© Copyright 2017 by Michael Genesereth. All rights reserved.