Logic 1

326.019, 326.021 - Mathematical Logic 1

326.111, 326.000 - Mathematical Logic and Logic-Oriented Programming Languages

---

New Examination

A new exam for Logic 1 will be organized:

Tuesday May 22

Theory 14:30 - 16:00 - KopfGebaeude 416 (near RISC office)

Exercises 16:15 - 17:45 - KopfGebaeude 416 (near RISC office)

Consultations: Monday May 21 from 17:00 to 18:30 in room KopfGebaeude 416.

The examination is open to students who did not participate at the previous examination and also to students who want to improve their mark.

---

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 the actual lectures is available as pdf file. (May contain some typos and small errors, but otherwise very good.)

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 10:15 in HS9 (both lectures);

10:30 to 11:45 in BA9911 (only "Mathematical Logic");

12:00 to 13:30 in HS6 (both lectures).

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

You may participate at any of the lectures even if you are not registered through KUSSS, however it is better to register as soon as you decide to take the course, because then you will receive announcements via e-mail.

I asked to increase the maximal number of participants to 120, in order to allow new people to register.

The lecture (A) 326.111, 326.000 - Mathematical Logic and Logic-Oriented Programming Languages has 2 + 1 hours, while the lecture (B) 326.019, 326.021 - Mathematical Logic 1 has 4 + 1 hours. Thus the lecture (A) will be a subset of the lecture (B), therefore the organization will be as follows:

• I reserved the lecture hall for an extra 45 min. each week. This 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.

The home page of the lecture in WS 2005 may give you an idea about the contents and the homeworks, although the current lecture will not be exactly the same.

Lectures

• Oct. 5: Lecture 1:
  • Mathematics, Logic, Computer Science. (First chapter of script.)
  • Propositional Logic: Syntax. Semantics.

• Oct. 12: Lecture 2:
  • Propositional Logic (continued):
  • Syntax. Semantics.
  • Semantic equivalence, logical consequence.
  • Homework 1: logic-hw-1.pdf, logic-hw-1.ps, logic-hw-1.dvi, logic-hw-1.tex.
  • Additional Lecture 2 (for Mathematical Logic 1):
  • An alternative model for propositional logic propositional.pdf.
  • Additional Homework 1 (for Mathematical Logic 1): logic-hw-add-1.pdf, logic-hw-add-1.ps, logic-hw-add-1.dvi, logic-hw-add-1.tex.

• Oct. 19: Lecture 3:
  • Propositional Logic (continued):
  • Proof methods: truth table, natural style, sequent calculus.
  • Homework 2: logic-hw-2.pdf, logic-hw-2.ps, logic-hw-2.dvi, logic-hw-2.tex.
  • Additional Lecture 3 (for Mathematical Logic 1):
  • An alternative model for propositional logic (continued).
  • Additional Homework 2 (for Mathematical Logic 1): logic-hw-add-2.pdf, logic-hw-add-2.ps, logic-hw-add-2.dvi, logic-hw-add-2.tex.

• Oct. 26: No lecture. (public holiday)

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

• Nov. 9: Lecture 4.
  • Propositional Logic (continued):
  • Completeness of a "short" sequent calculus for "not" and "and".
  • Homework 3: logic-hw-3.pdf, logic-hw-3.ps, logic-hw-3.dvi, logic-hw-3.tex.
  • Additional Lecture 4 (for Mathematical Logic 1):
  • An alternative model for propositional logic (continued). Correctenss of the calculus.
  • Additional Homework 3 (for Mathematical Logic 1): logic-hw-add-3.pdf, logic-hw-add-3.ps, logic-hw-add-3.dvi, logic-hw-add-3.tex.

• Nov. 16: No lecture. (travelling abroad)

• Nov. 23: Lecture 5.
  • Propositional Logic (continued):
  • Adding new logical connectives and new rules to the sequent calculus.
  • Answering questions about efficiency and correctness.
  • An alternative calculus for sequents containing only one goal: new rules for disjunction in the conclusion and for negation in the assumptions, additional definition for axioms. Correctness and completeness.
  • Homework 4: logic-hw-4.pdf, logic-hw-4.ps, logic-hw-4.dvi, logic-hw-4.tex.
  • Additional Lecture 5 (for Mathematical Logic 1):
  • An alternative model for propositional logic (continued). Correctness of the calculus, terminal rules.
  • Additional Homework 4 (for Mathematical Logic 1): logic-hw-add-4.pdf, logic-hw-add-4.ps, logic-hw-add-4.dvi, logic-hw-add-4.tex.

• Nov. 30: Lecture 6.
  • Propositional Logic (continued):
  • The conjunctive normal form of a propositional theorem.
  • The resolution principle: correctness, completeness.
  • The Davis-Putnam method.
  • Predicate Logic: syntax.
  • Homework 5: logic-hw-5.pdf, logic-hw-5.ps, logic-hw-5.dvi, logic-hw-5.tex.
  • Additional Lecture 6 (for Mathematical Logic 1):
  • An alternative model for propositional logic (continued). Completeness of the calculus.
  • Additional Homework 5 (for Mathematical Logic 1): logic-hw-add-5.pdf, logic-hw-add-5.ps, logic-hw-add-5.dvi, logic-hw-add-5.tex.

• Dec. 7: Lecture 7.
  • Predicate Logic (continued):
  • Semantics: interpretations, truth evaluation, validity.
  • Equivalences between quantified formulae.
  • Normal form, resolution, unification.
  • Homework 6: logic-hw-6.pdf, logic-hw-6.ps, logic-hw-6.dvi, logic-hw-6.tex.
  • Additional Lecture 6 (for Mathematical Logic 1):
  • The method of meta-variables for proving in predicate logic.

• Dec. 14: Lecture 8: Final lecture.
  • Herbrand universe, atom set.
  • The resolution principle: completeness.
  • Sequent calculus for quantified formulae.
  • The equality relation: proving by rewriting, computing.
  • The relation between logic and programming: logic programming, functional programming.
  • Summary of the whole material and preparation for the examination.
  • Proof example which uses the rule for negation in the assumptions, which was requested by a student during the last lecture: proof-example.pdf, proof-example.ps, proof-example.dvi, proof-example.tex.

• Consultations in room Kopfgebaeude 416 (RISC office):
  • Tuesday Jan 9 from 16:00 to 19:00,
  • Wednesday Jan 10 from 16:00 to 19:00,

• Thursday Jan 11: Examination
  • Theory: 8:30 - 10:00 in HS9.
  • Exercises: 12:00 - 13:30 in HS6.

• Jan. 18: Lecture 9 (Final lecture for Mathematical Logic 1).
  • Program verification: generation of verification conditions: Program-Verification.pdf
  • Example of sequent calculus in predicate logic.
  • Induction.
  • Demo of the Theorema system: Theorema-Demo-Linz-Jan-2007.tar.gz.
  • The relationship between logic, computing, and programming.

• Consultations in room Kopfgebaeude 416 (RISC office):
  • Wednesday Jan 24 from 16:00 to 19:00,

• Thursday Jan 25: Additional examination
  • Theory: 8:30 - 10:00 in HS9.

Homeworks:

Each exercise counts in your final examination.

In case you send your homeworks by e-mail, please use the address logic@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.

Please use this e-mail address only for homeworks. For any other matters please use my personal address Tudor.Jebelean@jku.at

Received homeworks

are listed in this table together with the number of correctly solved subjects.

The total number of points for the homeworks is 23, which will be added to the 85 points at the subjects in each examination. From this total of 108, you must obtain minimum 93 for grade (1), 78 for (2), 64 for (3), and 51 for (4).

Results of the examination on 11 Jan

table

---

T. Jebelean