Logic 1

Logic 1

326.019, 326.021 - Mathematical Logic 1

326.I02 - Mathematical Logic 1

Winter Semester 2012

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 in HS6. The first lecture was on Thu Oct 4.

If the lecture does not take place in a certain week, this will be announced on this page. The home page of the lecture in WS 2011 may give you an idea about the contents and the homeworks, although the current lecture will not be exactly the same.

Lectures

Oct. 4: Lecture 1: Introduction:
- Examples relating Logic to Mathematics and Computer Science:
  - simple law text;
  - Russel's paradox;
  - sorting by pattern matching;
  - Pattern based matching using Mathematica: GCD, Sum, Sorting Mma-programs.pdf.
  - 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.
Oct. 11: Lecture 2:
- Propositional Logic: Syntax, Semantics
  - Logic-2012-10-11.pdf.
Oct. 17: Lecture 3:
- Propositional Logic: Syntax, Semantics, Semantics based notions
  - main parts of a logic model: syntax, semantics, pragmatics;
  - the inductive principle in defining syntax;
  - the main principle of semantics;
  - semantics based notions: validity, consistency, semantical logical consequence, semantic equivalence.
- Homework 1: logic-hw-1.pdf, logic-hw-1.tex.
Oct. 25: Lecture 4:
- Propositional Logic: Pragmatics
  - Purpose of pragmatics: proving validity, sematic equivalence, semantical logical consequence.
  - Interesting semantic equivalences.
  - Conjunction and disjunction applied to sets.
  - Proving by rewriting: CNF, DNF.
  - Equivalences involving truth constants.
  - Resolution: method, correctness, completeness.
- Homework 2: logic-hw-2.pdf, logic-hw-2.tex.
Nov 2: No lecture:
Nov 8: Lecture 5:
- The DPLL Algorithm for the SAT problem.
- First Order Predicate Logic.
  - Introduction to predicate logic as the language of Mathematics.
  - Syntax of first order predicate logic: inductive definition of terms and of formulae.
  - Semantics of first order predicate logic: interpretations.
  - Truth evaluation of formulae, object evaluation of terms.
- Homework 3: logic-hw-3.pdf, logic-hw-3.tex.
Nov 15: Lecture 6:
- First Order Predicate Logic
  - Truth evaluation: the treatment of quantifiers using partial assignments.
  - Semantical based notions: valid, satisfiable, consistent, semantical logical consequence, semantical equivalence.
  - Rewriting: interesting equivalences over quantified formulae.
  - Prenex normal form, CNF (conjunctive normal form), Skolemization.
  - Proving by refutation, CNF, and resolution.
  - Correctness of resolution.
  - Completeness of resolution: Herbrand universe, Herbrand interpretations, semantic tree, the Herbrand Theorem.
- Homework 4: logic-hw-4.pdf, logic-hw-4.tex.
Nov 22: Lecture 7:
- Relation between logic and programming
  - Computability.
Nov 29: Lecture 8 (last lecture for short version):
- First order predicate logic
  - Discussion of homeworks.
  - Completeness of resolution.
  - Sequent calculus.
  - Review of the material for the examination.
Dec 6: Lecture 9 (first lecture for long version):
- Fundamentals of program verification
  - Verification-01.pdf
  - Verification-02.pdf
Dec 13: Examination for the short version:
- 8:30 - 10:00 Consultations, review of the material.
- 10:15 - 11:45 Examination Theory
- 12:00 - 13:30 Discussion of solutions
Dec 20, 27, Jan 3: No lecture:
Jan 10: Lecture 10:
- Sequent calculus
  - Extending the sequent calculus in propositional logic for handling all logical connectives.
  - Unique goal sequent calculus.
  - Examples of natural style proofs in predicate logic.
  - Short demo of the Theorema system Theorema-Demo-Oct-2009.zip.
  - Sequent calculus in first order predicate logic: the 4 rules for quantifiers and their correctness.
- Homework 5: logic-hw-5.pdf, logic-hw-5.tex.
Jan 17: Lecture 11:
- Interesting proof examples
  - Multiple witness: there exist X, Y irrational such that X^Y is rational.
  - Using the inference rule for negation in the assumptions: square root of 2 is irrational proof-example.tex, proof-example.pdf.
- An alternative propositional logic
  - Using conjunction and disjunction as connectives for sets of formulae.
  - propositional.pdf.
- Logic vs. programming
  - Computing by rewriting (substitution and replacement): GCD, set of subsets, sum of numbers Mma-programs.pdf.
  - Designing algorithms by "check and repair": sorting.
- Homework 6: logic-hw-6.pdf, logic-hw-6.tex.
Jan 24: Logic vs. programming:
- Exercises with sequent calculus.
- Computing by rewriting, tail recursion: reverse of a list reverse.pdf.
- Program verification by symbolic execution: symbolic-execution-presentation.pdf, symbolic-execution-paper.pdf.
Jan 31: Examination for long version:
- 8:30 - 10:00 Review of the material
- 10:15 - 11:45 Examination theory second part
- 12:00 - 12:45 Examination exercises
- 12:45 - 13:30 Discussion of solutions

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