Logic 1

326.019, 326.021 - Mathematical Logic 1

Winter Semester 2008

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

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 in HS6.

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. 8: Lecture 1:
  • Examples relating Logic to Mathematics and Computer Science.
  • The role of Mathematics and Logic in science.
  • Demo of the Theorema system: Theorema-Demo-Linz-Jan-2007.tar.gz.

• Oct. 15: Lecture 2:
  • Propositional Logic:
  • Syntax.

• Oct. 23: Lecture 3:
  • Propositional Logic:
  • Semantics.
  • Semantic equivalence, logical consequence.
  • Proof methods: truth table.
  • Homework 1: logic-hw-1.pdf, logic-hw-1.ps, logic-hw-1.dvi, logic-hw-1.tex.

• Nov. 6: Lecture 5:
  • Solutions of homework 1.
  • Propositional Logic:
  • Natural style deduction and its formalization as sequent calculus.
  • Inference rules in sequent calculus.
  • Homework 3: logic-hw-3.pdf, logic-hw-3.ps, logic-hw-3.dvi, logic-hw-3.tex.

• Nov. 13: Lecture 6:
  • Dr. Nikolaj Popov: Logical aspects of program verification.
  • Logic-Slides-13-nov.pdf
  • Logic-Examples-13-nov.pdf

• Nov. 20: Lecture 7:
  • Solutions of homework 2.
  • Propositional Logic:
  • The resolution rule.
  • Sequent calculus.
  • Homework 4: logic-hw-4.pdf, logic-hw-4.ps, logic-hw-4.dvi, logic-hw-4.tex.

• Nov. 27: Lecture 8:
  • Solutions of homework 3.
  • Propositional Logic:
  • Comparison between rewriting of propositional formulae and rewriting of polynomials.
  • Sequent calculus:
  • correctness and completeness of the "small" calculus,
  • adding more rules the "small" calculus.
  • Homework 5: logic-hw-5.pdf, logic-hw-5.ps, logic-hw-5.dvi, logic-hw-5.tex.

• Dec. 4: Lecture 9:
  • Solutions of homework 4.
  • Propositional Logic:
  • Sequent calculus: comparison between different versions.
  • Proof example: sqrt[2] not rational: proof-example.pdf.
  • Unique goal sequent calculus.
  • Homework 6: logic-hw-6.pdf, logic-hw-6.ps, logic-hw-6.dvi, logic-hw-6.tex.

• Dec. 11: Lecture 10:
  • Solutions of homework 5.
  • Predicate Logic:
  • Syntax, semantics, rewrite rules.
  • Homework 7: logic-hw-7.pdf, logic-hw-7.ps, logic-hw-7.dvi, logic-hw-7.tex.

• Dec. 18: Lecture 11:
  • Solutions of homework 6.
  • Predicate Logic:
  • Rewrite rules: classification and use for normalization.
  • CNF, prenex normal form.
  • Additional inference rules for quantified formulae (instantiation, witness).
  • Resolution in predicate logic: correctness.
  • Unification.
  • Homework 8: logic-hw-8.pdf, logic-hw-8.ps, logic-hw-8.dvi, logic-hw-8.tex.

• Jan. 8: Lecture 12:
  • Predicate Logic:
  • Skolem normal form.
  • Resolution: definition, correctness, examples.
  • Herbrand universe, Herbrand interpretation.
  • Homework 9: logic-hw-9.pdf, logic-hw-9.ps, logic-hw-9.dvi, logic-hw-9.tex.

• Jan. 15: Lecture 13:
  • Herbrand theorem.
  • Completeness of resolution.
  • Sequent calculus in first order predicate logic.
  • Homework 9: logic-hw-10.pdf, logic-hw-10.ps, logic-hw-10.dvi, logic-hw-10.tex.

• Jan. 22: Lecture 14 (last lecture):
  Review of the material for the examination.
  • Aspects concerning the relation between logic and programming.

• Jan. 29: Examination
  • Theory: 08:30 - 10:00
  • Exercises: 10:15 - 11:45

Homeworks:

Each exercise counts in your final examination.

In case you send your homeworks by e-mail, please use my address tjebelea@risc.uni-linz.ac.at.

Also please use as name of the file[s] your name and the number of the homework, e. g. like Mayer-3.pdf or Schreiner-J-4.ps. Please do not use Windows Word files (*.doc) because the special symbols are not shown correctly on different systems. If you do not have alternative to Word, then please print the file using the option "Print to file" and send this file too.