Logic for computer science

To Ricardo Caferra, my teacher at Ensimag.

One chapter and one exercise sheet per week. The chapter can be read on its own; the sheet is prepared before the tutorial session, where we go through it together.

The first six chapters deal with propositional calculus; the last four, with first-order logic.

Lecture notes

1. The language of propositions : What a formula is, how to read it, and how to write it with as few parentheses as possible without changing its meaning.
2. Truth, models, consequence : Giving a formula a truth value, classifying formulas according to whether they can be true or always are, and saying when a formula follows from others.
3. Normal forms : Bringing any formula to a standard form, a conjunction of clauses or a disjunction of conjunctions, and what it costs.
4. Modelling and solving: SAT and puzzles : Translating a problem into formulas, asking whether they are consistent and what they imply, and letting an algorithm look for the answer.
5. Resolution : A single rule, applied to clauses, that is enough to show that a set of formulas is contradictory, and therefore that a formula follows from others.
6. Natural deduction : Proving a formula through a sequence of small steps, each justified by a rule, the way one reasons by hand, and why these proofs tell the truth.
7. First order: the language : Talking about objects and their properties with terms, predicates and quantifiers, and knowing which variable depends on which quantifier.
8. First order: semantics and modelling : Giving formulas a meaning in a structure, showing with a counterexample that one formula does not entail another, and translating natural language without picking the wrong quantifier.
9. Prenex normal form and Skolemisation : Moving all the quantifiers to the front, replacing the “there exists” by functions, and arriving at clauses, ready for resolution.
10. Unification and first-order resolution : Finding the most general substitution that makes two terms equal, using it to resolve clauses with variables, and what the machine can, or cannot, decide.

Exercise sheets

1. Reading and writing formulas : Parentheses, precedence, syntax trees, and the boundary between formulas and statements about formulas. Chapter 1.
2. Truth, models, consequence : Truth tables, models, classifying a formula, and proving properties of logical consequence. Chapter 2.
3. Normal forms : Putting formulas into CNF and DNF, by computation and by truth table, and expressing constraints with only three connectives. Chapter 3.
4. Modelling and solving: investigations and puzzles : Translating facts into formulas, testing their consistency, running DPLL by hand, and sorting out the inhabitants of two islands. Chapter 4.
5. Resolution : Computing resolvents, refuting to prove a consequence, and saturating to show that a set is satisfiable. Chapter 5.
6. Natural deduction : Write Fitch-style proofs, from the most direct ones to those that need proof by contradiction, and relate proof and truth. Chapter 6.
7. First-order logic: the language : Terms and formulas, free and bound variables, renaming and capture-avoiding substitution. Chapter 7.
8. First-order logic: semantics and modelling : Evaluate a formula in a structure, build countermodels, translate natural language without ambiguity, and assess syllogisms. Chapter 8.
9. Prenex normal form and Skolemisation : Pull the quantifiers out, replace them with Skolem functions, and move to clauses. Chapter 9.
10. First-order unification and resolution : Compute most general unifiers, refute with variables, and follow what Prolog does. Chapter 10.