Logic 1

326.019, 326.021 - Mathematical Logic 1

Winter Semester 2007 - 2008

The course is an introduction to logic for students in Computer Science and Mathematics. It is largelly based on the script:

Bruno Buchberger: Logic for Computer Science. A scanned copy of the script is available as 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.

A transcript by Martin Koehler of previous lectures is available as pdf file. (May contain some typos and small errors.)

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 11:45 in BA9911;

12:00 to 13:30 in P004.

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

• The extra 45 min. each week will cover up for the possible weeks (one or two) when I may have to travel abroad and I cannot hold the lecture.
• The exercises will not be scheduled separately, but will be interspersed within the lecture at the appropriate places.

Lectures

• Oct. 4: Lecture 1:
  • Examples relating Logic to Mathematics and Computer Science (one example is proof-example.pdf).
  • The role of Mathematics and Logic in science.
  • Demo of the Theorema system: Theorema-Demo-Linz-Jan-2007.tar.gz.

• Oct. 11: Lecture 2:
  • Propositional Logic:
  • Syntax. Semantics.
  • Semantic equivalence, logical consequence.
  • Proof methods: truth table, resolution, natural style, sequent calculus.
  • Homework 1: logic-hw-1.pdf, logic-hw-1.ps, logic-hw-1.dvi, logic-hw-1.tex.

• Oct. 18: Lecture 3:
  • Propositional Logic (continued):
  • a small sequent calculus for formulae containing negation and conjunction;
  • correctness and completeness;
  • extending the sequent calculus to formulae containing disjunction (the Watt calculus);
  • extending to implication and equivalence;
  • unique-goal sequent calculus.
  • First order predicate logic:
  • syntax, semantics - interpretations, truth evaluation.
  • Homework 2: logic-hw-2.pdf, logic-hw-2.ps, logic-hw-2.dvi, logic-hw-2.tex.

• Oct. 25: Lecture 4:
  • Propositional Logic: treatment of truth constants in sequent calculus.
  • Predicate Logic:
  • equivalences between quantified formulae;
  • prenex normal form, conjunctive normal form, Skolem normal form,
  • the Herbrand universe.
  • Homework 3: logic-hw-3.pdf, logic-hw-3.ps, logic-hw-3.dvi, logic-hw-3.tex.

• Nov. 1: No lecture. (public holiday)

• Nov. 8: Lecture 5:
  • Predicate Logic:
  • example of a predicate logic proof in natural style (sum of limits),
  • analysis of the proof and identification of the inference rules,
  • sequent calculus for first order predicate logic, correctness,
  • Herbrand interpretations, the universality of the Herbrand universe,
  • the Herbrand theorem.
  • Homework 4: logic-hw-4.pdf, logic-hw-4.ps, logic-hw-4.dvi, logic-hw-4.tex.

• Nov. 15: Lecture 6:
  • Solutions to HomeWorks 1, 2, 3.
  • Introduction to verification of functional programs presentation.

• Nov. 22: Lecture 7:
  • Predicate Logic:
  • Sequent calculus: examples and comparison with Herbrand method.
  • Introduction to resolution and unification.
  • Homework 5: logic-hw-5.pdf, logic-hw-5.ps, logic-hw-5.dvi, logic-hw-5.tex.

• Nov. 29: Lecture 8: Introduction to the theory of computability Logic-Computability.pdf.

• Dec. 6:
  • The completeness of the resolution principle.
  • The equality relation: explicit properties.
  • Using the properties of equality: substitution and replacement.
  • Programming in predicate logic by conditional equalities.
  • Homework 6: logic-hw-6.pdf, logic-hw-6.ps, logic-hw-6.dvi, logic-hw-6.tex.

• Dec. 13:
  • Definitions in predicate logic.
  • Verification conditions for functional programs.
  • Homework 7: logic-hw-7.pdf, logic-hw-7.ps, logic-hw-7.dvi, logic-hw-7.tex.

• Jan 10: Final review of the material and solution to homeworks.
  Subjects from previous examinations exercises.pdf, theory-1.pdf, theory-2.pdf.

• Jan 17: Examination

  Theory: 8:30 to 10:00 in BA9911;

  Exercises: 10:15 to 11:45 in BA9911.

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.