Logic 1
326.019, 326.021 - Mathematical Logic 1
Winter Semester 2010
The course is an introduction to logic for students in
Computer Science and Mathematics.
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 in HS6.
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. 7: 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. 14: Lecture 2:
- Propositional Logic:
- Syntax: the induction principle for propositional formulae.
- Semantics: definition using interpretations.
- Proving using rewriting: the Conjunctive Normal Form.
- Homework 2:
logic-hw-2.pdf,
logic-hw-2.tex.
- Oct. 21: Lecture 3:
- Propositional Logic:
- Rewriting: DNF, CNF, truth constants, partial completeness.
- Resolution: inference rule, proof method, correctness, completeness.
- SAT solving: Davis-Putnam, DPLL.
- Homework 3:
logic-hw-3.pdf,
logic-hw-3.tex.
- Oct. 28: Lecture 4:
- Propositional Logic:
- Sequent calculus as a model of natural style reasoning.
- The sequent calculus for formulae containing only negation and conjunction. Completeness and correctness.
- Homework 4:
logic-hw-4.pdf,
logic-hw-4.tex.
- Nov 4: Lecture 5:
- Propositional Logic:
- Extending the sequent calculus for more logical connectives.
- Modus ponens, modus tollens, resolution, subsumption.
- The "unique-goal" sequent calculus.
- Proof example using the rule for negation in the assumptions:
proof-example.pdf.
- Homework 5:
logic-hw-5.pdf,
logic-hw-5.tex.
- Nov. 11: Lecture 6:
- Predicate Logic.
- Syntax.
- Semantics.
- Rewriting: equivalences of quantified formulae, prenex normal form.
- Homework 6:
logic-hw-6.pdf,
logic-hw-6.tex.
- Nov. 18: Lecture 7:
- Nov. 25: Lecture 8:
- Dec. 2: Lecture 9:
- Dec. 9: No lecture.
- Dec. 16: Lecture 10:
- Predicate Logic.
- Herbrand Universe, semantic tree, Herbrand theorem.
- Completeness of resolution.
- Sequent Calculus.
- Example of natural style proof.
- Homework 10:
logic-hw-10.pdf,
logic-hw-10.tex.
- Jan. 13: Lecture 11:
- Sequent calculus in predicate logic.
- The four rules for quantifiers.
- Further examples.
- Using metavariables for finding witnesses and instatiation terms.
- Jan. 20: Lecture 12:
- 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.
- Jan. 27, 8:30 - 10:00: Examination Theory
Homeworks:
Each exercise counts for your final grade.
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.
T. Jebelean