Logic 1

326.019, 326.021 - Mathematical Logic 1

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

New Examination

Wednesday, June 1st

theory: 8:30 - 10:00 in room K033 C (Kepler Gebaeude)

exercises: 10:15 - 11:15 in room K001 A (Kepler Gebaeude)

The examination is open to all students who could not come to the first examination, as well as to students who want to improve their previous grade.

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).

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. 7, 8:30 to 13:30 in HS6

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 3rd of November).

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. Therefore the lecture (A) will be a subset of the lecture (B), which complicates a little the organization.

I suggest the following way of organizing the lecture, but the final decision will be taken by discussion with the participants on Oct. 7. Until then I wellcome your comments by e-mail.

• 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. 7: Lecture 1 (10:15 - 11:45 and 12:00 - 12:45)

Oct. 14: Lecture 2 (10:15 - 11:45 and 12:00 - 12:45)

• Propositional Logic (continued)
• Syntax: The definition of language as a set.
• Semantics: The truth evaluation function.
• Validity, consistency, equivalence.
• Proving by truth table.
• Conjunctive normal forms, disjunctive normal forms.
• Proving by normal form.
• Proving by resolution.
• Natural style proving, Theorema demo.
• Sequents as math model of proof situations. Examples of sequent inference rules.
• Homework 2: logic-hw-2.pdf, logic-hw-2.ps, logic-hw-2.dvi, logic-hw-2.tex.

Oct. 21: Lecture 3 (10:15 - 11:45 and 12:00 - 12:45)

• Propositional Logic (continued)
• Sequents as math model of proof situations. Examples of sequent inference rules.
• Definition of a sequent calculus. Example of a short calculus.
• Correctness and complenetness of the short sequent calculus.
• Homework 3: logic-hw-3.pdf, logic-hw-3.ps, logic-hw-3.dvi, logic-hw-3.tex.

Oct. 28: Lecture 4

• Propositional Logic (continued)
• Sequents as math model of proof situations. More examples of sequent inference rules.
• Eliminating (proving correctness of) other inference rules.
• Correctness and complenetness of more complexe versions of sequent calculus.
• Predicate Logic
• Syntax of the language. Examples.
• Semantics. Interpretations.
• Validity, logical consequence, equivalence.
• Homework 4: logic-hw-4.pdf, logic-hw-4.ps, logic-hw-4.dvi, logic-hw-4.tex.

Nov. 04: Lecture 5

• Predicate Logic (continued)
• Some equivalent quantified formulae.
• Normal forms: prenex, Skolem. Proving using normal forms.
• Resolution in predicate logic: the inference rule and the method.
• The Herbrand universe of a formula.
• Homework 5: logic-hw-5.pdf, logic-hw-5.ps, logic-hw-5.dvi, logic-hw-5.tex.

Nov. 11: Lecture 6

• Predicate Logic (continued)
• Herbrand theorem.
• Completeness of the resolution method. Goedel compleneteness theorem.
• Natural deduction. Examples. Sequent calculus.
• Predicate logic with equality. Equality reasoning.
• Rules for definitions in predicate logic: functions and predicates.
• The relation between logic and programming.
• Review of material

### Examination Nov 18, 2004

Nov. 25: There is no lecture on Nov. 25.

Dec. 2: Lecture 7

Demo of the Theorema system. The zip file containing the demo (see first README.txt). During the lecture we covered the first two parts of the demo (Overview of the system, Proving in natural style).

• Homework 6: logic-hw-6.pdf, logic-hw-6.ps, logic-hw-6.dvi, logic-hw-6.tex.

Dec. 9: Lecture 8

Demo of the Theorema system. The zip file containing the demo (see first README.txt). During the lecture we will cover the last part of the demo (Math knowldedge at work).

Discussion on a propositional theory for a Theorema prover: paper.pdf, paper.ps, paper.dvi.

Dec. 16: There is no lecture on Dec. 16.

Jan. 13: Lecture 9

Further discussion on the propositional theory for a Theorema prover, proof of correctness and completeness, examples.

Jan. 20: Lecture 10

The unification algorithm. Construction of the correct algorithm using the principles of logic.

Jan. 27: Examination for the long version of the lecture (326019).

HS6, 8:30.

### ATTENTION!

Each exercise counts as one point in your final examination.