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.

The script is available in printed copy from me, but you may also download a PDF (scanned).

A transcript by Martin Koehler of the actual lectures is available at http://members.liwest.at/mkoehler/logic/ and as local 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 first lecture will take place

Thursday, Oct. 13, 8:30 to 10:00 in HS6 and continuing from 10:15 to 13:30 in K033 C,

which will be the usual time and place for the lecture. If the lecture does not take place in a certain week, this will be announced on this page.

I asked in through the KUSSS system for on line registration, because I need to have a list of the participating students. However, it is not mandatory to register in order to participate at the first lecture[s]. In fact, I would prefer that you register after you see the first lecture[s] and you take the final decision to participate for the rest of the semester (the deadline for registration is 31st of October for UE and 1st of June for VO).

The lecture (A) 326.111, 326.000 - Mathematical Logic and Logic-Oriented Programming Languages is addressed to the students in Computer Science and has 2 + 1 hours, while the lecture (B) 326.019, 326.021 - Mathematical Logic 1 is addressed to students in Mathematics and 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 first 6 to 7 weeks of the course will cover the number of hours necessary for (A), after which we can organize the examination for theory ("Vorlesung") for the Computer Science students, as well as the examination for exercises ("Uebung") for all the participants.
• The rest of the weeks I will continue the course until (B) is also finished.

Lectures

• Oct. 13: Lecture 1 (8:30 - 10:00 in HS6, 10:15 - 11:45 and 12:00 - 13:30 in K033 C):
  • Mathematics, Logic, Computer Science. (First chapter of script.)
  • Propositional Logic: Syntax. Semantics.
  • Homework 1: logic-hw-1.pdf, logic-hw-1.ps, logic-hw-1.dvi, logic-hw-1.tex.

• Oct. 20: Lecture 2 (8:30 - 10:00 in HS6, 10:15 - 11:45 and 12:00 - 13:30 in K033 C):
  • Propositional Logic (continued):
  • Syntax. Semantics.
  • Simplification of formulae. Normal form.
  • Proof systems: examples, sequent calculus.
  • Homework 2: logic-hw-2.pdf, logic-hw-2.ps, logic-hw-2.dvi, logic-hw-2.tex.

• Oct. 27: Lecture 3 (8:30 - 10:00 in HS6, 10:15 - 11:45 and 12:00 - 13:30 in K033 C):
  • Propositional Logic (continued):
  • Proof systems: sequent calculus.
  • Definitions of: sequent, inference rule, proof-tree.
  • The "short calculus" for not, and, or.
  • Correctness and completeness of the short calculus.
  • Extending the short calculus.
  • Homework 3: logic-hw-3.pdf, logic-hw-3.ps, logic-hw-3.dvi, logic-hw-3.tex.

• Nov. 3: Lecture 4 (8:30 - 10:00 in HS6, 10:15 - 11:45 and 12:00 - 13:30 in K033 C):
  • Propositional Logic (continued):
  • The resolution principle and the resolution method. Correctness and completeness.
  • The Davis-Putman procedure.
  • First Order Predicate Logic.
  • Syntax: variables, constants, function symbols, predicate symbols, quantifiers. Terms and formulae.
  • Semantics: interpretations, truth evaluation.
  • Homework 4: logic-hw-4.pdf, logic-hw-4.ps, logic-hw-4.dvi, logic-hw-4.tex.

• Nov. 10: Lecture 5 (8:30 - 10:00 in HS6, 10:15 - 11:45 and 12:00 - 13:30 in K033 C):
• Homework 5: logic-hw-5.pdf, logic-hw-5.ps, logic-hw-5.dvi, logic-hw-5.tex.

• Nov. 17: There is no lecture on this date!

• Nov. 24: Lecture 6 (8:30 - 10:00 in HS6, 10:15 - 11:45 and 12:00 - 13:30 in K033 C):

  A transcript by Martin Koehler of the actual lectures is available at http://members.liwest.at/mkoehler/logic/ and as local file. (May contain some typos and small errors, but otherwise very good.)

  Consultations: Nov. 29 and Nov. 30, from 16:00 to 19:00 in RISC office (room 416) in Kopfgebaeude.

• Dec. 1: Examination Theory 8:30 - 10:00 in HS6
• Dec. 1: Examination Exercises 10:15 - 11:45 in K033 C.

Examination Results from Dec. 1

• An alternative model for propositional logic paper.pdf.
• Algorithm synthesis using logic principles zip file (see README.txt, and Section 3 of MAIN-TALK_Linz-2004.nb),
• Homework 6: new-hw6.txt.

Consultations: Jan 25, from 16:00 to 19:00 in RISC office (room 416) in Kopfgebaeude.

ATTENTION!

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

TABLE WITH RECEIVED HOMEWORKS (Nov. 29)