Logic 1
326.019, 326.021 - Mathematical Logic 1
326.I02 - Mathematical Logic 1
Winter Semester 2011
The course is an introduction to logic for students in
Computer Science and Mathematics.
The lecture has a short version (326.I02) and a long version
(326.019, 326.021).
Students from Computer Science and Mathematics may take any of the versions,
you may decide to take the long version after the end of the short version (approx. beginning of December).
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. The first lecture is on Thu Oct 13.
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.
The home page of the lecture in WS 2009 may give you an idea about the contents
and the homeworks, although the current lecture will not be exactly the same.
Lectures
- Oct. 13: Lecture 1:
- Examples relating Logic to Mathematics and Computer Science:
- simple law text;
- Russel's paradox;
- sorting by pattern matching;
- termination of programs.
- The role of Mathematics and Logic in science:
- intelectual problem solving: observe - solve - apply;
- applications of logic: verification of systems, semantic web.
- Propositional Logic:
- Homework 1:
logic-hw-1.pdf,
logic-hw-1.tex.
- Oct. 20: Lecture 2:
- Propositional Logic:
- semantic based notions (valid, unsatisfiable, semantic equivalence, semantical logical consequence, etc.),
- simple equivalences and proving by rewriting and normal forms.
- Homework 2:
logic-hw-2.pdf,
logic-hw-2.tex.
- Oct. 27: Lecture 3:
- Propositional Logic:
- the resolution method, the DPLL method;
- sequent calculus as a model for natural style proving.
- Homework 3:
logic-hw-3.pdf,
logic-hw-3.tex.
- Nov. 3: Lecture 4:
- Nov. 10: Lecture 5:
- Predicate Logic:
- The syntax of first order predicate logic: terms and formulae.
- The semantics of first order predicate logic: interpretations, computing the truth value (partial).
- Homework 5:
logic-hw-5.pdf,
logic-hw-5.tex.
- Nov. 17: Lecture 6:
- Predicate Logic:
- The semantics of first order predicate logic: interpretations, computing the truth value (continued).
- Equivalences of quantified formulae.
- Homework 6:
logic-hw-6.pdf,
logic-hw-6.tex.
- Nov. 24: Lecture 7:
- Predicate Logic:
- Equivalences of quantified formulae.
- Normal forms: prenex, Skolem, standard.
- Resolution in predicate logic, correctness.
- Herbrand universe, Herbrand interpretations, semantic tree, Herbrand theorem.
- Completeness of resolution in predicate logic.
- Sequent calculus: the 4 new rules for quantifiers.
- Homework 7:
logic-hw-7.pdf,
logic-hw-7.tex.
- Dec. 1: Lecture 8:
- Summary of the material before the examination
- Logic vs. Programming.
- Programming using conditional equalities: GCD, Sum.
- Transformation of a program into a tail recursive one.
- Additional example: the reverse of a list reverse.pdf.
- Pattern based matching using Mathematica: GCD, Sum, Sorting
Mma-programs.pdf.
- Prolog: logic programming. Sample interpreter in Mathematica
Mma-prolog.pdf.
- Dec. 8: No lecture (public holiday):
- Dec. 15: Examination:
Theory (8:30 - 10:00), Exercises (10:15 - 11:45)
- Jan. 12: Lecture 9:
- Presentation and discussion of the results of the examination in theory.
- Two interesting proofs:
irrationality of Sqrt[2] proof-example.pdf
and an existence proof with multiple witness.
- A model of propositional logic based on multiple arity conjunction and disjunction propositional.pdf.
- Jan. 19: Lecture 10:
- Presentation and discussion of the results of the examination in exercises.
- Logical based development of the unification algorithm.
- Basic principles of program verification using symbolic execution
presentation.pdf and
article.pdf.
- Jan. 26: Lecture 11 and Examination:
- Special logics (Hoare logic, temporal logic) and their applications to program verification.
- Review of the material for the examination.
- 12:00 - 12:45 Examination.
Mar. 26: Consultations
- Hagenberg 11:00 - 12:30 Room UFO in RISC Castle.
- Linz 17:00 - 18:30 Room S2 327 (RISC office in Science Park building 2).
Mar. 27: Examination:
- Theory short: 8:30 - 10:00 Room S2 059 (the usual lecture room),
- Exercises: 10:15 - 11:45 Room S2 059,
- Theory long: 12:00 - 12:45 Room S2 046 (attention, different room!)
Homeworks:
Each exercise counts for your final grade.
In case you send your homeworks by e-mail, please use my address
tjebelea@risc.jku.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.
The list of received homeworks.
T. Jebelean