Logic 1

326.019, 326.021 - Mathematical Logic 1

326.I02 - Mathematical Logic 1

Winter Semester 2011

The course is an introduction to logic for students in Computer Science and Mathematics.

The lecture has a short version (326.I02) and a long version (326.019, 326.021). Students from Computer Science and Mathematics may take any of the versions, you may decide to take the long version after the end of the short version (approx. beginning of December).

The contents of the lecture is very similar to the transcript by Martin Koehler of previous lectures: pdf file. (May contain some typos and small errors.)

For more details (some of which are not covered in the lecture) I recommend: Bruno Buchberger: Logic for Computer Science pdf file. This material is copyrighted and is available only for the students of this lecture and only for the purpose of study related to it.

Purpose

Understand the principles of Mathematical Logic and its mathematical models, aquire the skills for using it in Mathematics and Computer Science.

Contents

The principles of Mathematical Logic and its role in human activity.

Main models: propositional logic, first-order predicate logic, higher-order logic. Proof systems: correctness, completeness.

Practical use of Mathematical Logic in Mathematics (building theories, proving), and in Computer Science (automatic reasoning, programming, describing and proving properties of programs).

Organization

The lecture takes place on Thursdays:

8:30 to 12:45. The first lecture is on Thu Oct 13.

If the lecture does not take place in a certain week, this will be announced on this page.

• The exercises will not be scheduled separately, but will be interspersed within the lecture at the appropriate places.

Lectures

• Oct. 13: Lecture 1:
  • Examples relating Logic to Mathematics and Computer Science:
    • simple law text;
    • Russel's paradox;
    • sorting by pattern matching;
    • termination of programs.
  • The role of Mathematics and Logic in science:
    • intelectual problem solving: observe - solve - apply;
    • applications of logic: verification of systems, semantic web.
  • Propositional Logic:
    • syntax,
    • semantics.
  • Homework 1: logic-hw-1.pdf, logic-hw-1.tex.

• Oct. 20: Lecture 2:
  • Propositional Logic:
    • semantic based notions (valid, unsatisfiable, semantic equivalence, semantical logical consequence, etc.),
    • simple equivalences and proving by rewriting and normal forms.
  • Homework 2: logic-hw-2.pdf, logic-hw-2.tex.

• Oct. 27: Lecture 3:
  • Propositional Logic:
    • the resolution method, the DPLL method;
    • sequent calculus as a model for natural style proving.
  • Homework 3: logic-hw-3.pdf, logic-hw-3.tex.

• Nov. 3: Lecture 4:
  • Propositional Logic:
    • different versions of sequent calculus.
  • Homework 4: logic-hw-4.pdf, logic-hw-4.tex.

• Nov. 10: Lecture 5:
  • Predicate Logic:
    • The syntax of first order predicate logic: terms and formulae.
    • The semantics of first order predicate logic: interpretations, computing the truth value (partial).
  • Homework 5: logic-hw-5.pdf, logic-hw-5.tex.

• Nov. 17: Lecture 6:
  • Predicate Logic:
    • The semantics of first order predicate logic: interpretations, computing the truth value (continued).
    • Equivalences of quantified formulae.
  • Homework 6: logic-hw-6.pdf, logic-hw-6.tex.

• Nov. 24: Lecture 7:
  • Predicate Logic:
    • Equivalences of quantified formulae.
    • Normal forms: prenex, Skolem, standard.
    • Resolution in predicate logic, correctness.
    • Herbrand universe, Herbrand interpretations, semantic tree, Herbrand theorem.
    • Completeness of resolution in predicate logic.
    • Sequent calculus: the 4 new rules for quantifiers.
  • Homework 7: logic-hw-7.pdf, logic-hw-7.tex.

• Dec. 1: Lecture 8:
  • Summary of the material before the examination
  • Logic vs. Programming.
    • Programming using conditional equalities: GCD, Sum.
    • Transformation of a program into a tail recursive one.
    • Additional example: the reverse of a list reverse.pdf.
    • Pattern based matching using Mathematica: GCD, Sum, Sorting Mma-programs.pdf.
    • Prolog: logic programming. Sample interpreter in Mathematica Mma-prolog.pdf.

• Dec. 8: No lecture (public holiday):

• Dec. 15: Examination: Theory (8:30 - 10:00), Exercises (10:15 - 11:45)

• Jan. 12: Lecture 9:
  • Presentation and discussion of the results of the examination in theory.
  • Two interesting proofs: irrationality of Sqrt[2] proof-example.pdf and an existence proof with multiple witness.
  • A model of propositional logic based on multiple arity conjunction and disjunction propositional.pdf.

• Jan. 19: Lecture 10:
  • Presentation and discussion of the results of the examination in exercises.
  • Logical based development of the unification algorithm.
  • Basic principles of program verification using symbolic execution presentation.pdf and article.pdf.

• Jan. 26: Lecture 11 and Examination:
  • Special logics (Hoare logic, temporal logic) and their applications to program verification.
  • Review of the material for the examination.
  • 12:00 - 12:45 Examination.