Logic 1

326.019, 326.021 - Mathematical Logic 1

Winter Semester 2015

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 schedule of the lecture is shown in KUSSS. The home page of the lecture in WS 2014 may give you an idea about the contents and the homeworks, although the current lecture will not be exactly the same.

Lectures (may change depending on the concrete progress)

• Oct. 8: 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.
    • The role of Mathematics and of Mathematical Logic and their importance.
    • The intelectual problem solving cycle in our profesion, the role computer and of automated reasoning.
    • Applications of logic: verification of systems, semantic web.
  • Propositional Logic: Syntax.
    • The main parts of a logic model: syntax, semantics, pragmatics.
    • The definition of syntax as a language: alphabet, composition rules.
    • The inductive principle in the definition of syntax and its applications: defining functions, proving statements.
  • Homework 1: logic-hw-1.pdf, logic-hw-1.tex.

• Oct. 15: Lecture 2:
  • Propositional Logic: Semantics, Semantics based notions.
    • The main principle of semantics. Interpretations, truth value, truth valuation function.
    • Semantics based notions: validity, consistency, semantical logical consequence, semantic equivalence.
    • Proving semantical logical consequence by: validity of implication, refutation. Semantic equivalence as validity of syntactical equivalence and as double semantic consequence.
    • The use of semantic equivalence for rewriting formulae.
    • Some basic properties of conjunction: idempotence, commutativity, associativity. Embedding these properties at syntactic level by considering conjunctive sets.
  • Homework 2: logic-hw-2.pdf, logic-hw-2.tex.

• Oct. 22: No lecture.

• Oct. 29: Lecture 3:.
  • Propositional Logic: rewriting, normal forms, resolution, sequent calculus.
    • Interesting equivalences, using them as rewrite rules.
    • Negation normal form, conjunctive normal form, disjunctive normal form.
    • Proving equivalence and validity by conjunctive normal form.
    • The resolution method.
    • Sequent calculus - basic notions, the "and-not" sequent calculus and its correctness.
  • Homework 3: logic-hw-3.pdf, logic-hw-3.tex.

• Nov. 5: Lecture 4:.
  • Propositional Logic: sequent calculus.
    • Completeness of "and-not" sequent calculus.
    • Sequent rules for the truth constants.
    • Adding rules for the other logical connectives by "elimination".
    • Sequent rules for conjunction and for disjunction applied to sets.
    • Special rules: modus ponens, modus tollens, subsumption, resolution, implied goal.
    • The use of failed sequent proofs for constructing counterexamples.
    • Unique-goal sequent calculus.
  • Homework 4: logic-hw-4.pdf, logic-hw-4.tex.

• Nov. 12: Lecture 5:.
  • Propositional Logic: sequent calculus.
    • Transforming sequent calculus into "unique-goal" sequent calculus.
    Predicate logic: syntax, semantics, normal forms.
    • Syntax: terms and formulae.
    • Semantics: the elements of an intrerpretation, truth evaluation.
    • Validity, unsatifiability, semantical logical consequence, semantic equivalence.
    • Interesting equivalences, rewriting.
    • Normal forms: NNF, prenex, CNF.
    • The Skolem transformation, the Skolem normal form, the standard normal form.
  • Homework 5: logic-hw-5.pdf, logic-hw-5.tex.

• Nov. 19: Lecture 6:.
  • Predicate Logic: unification
    • The resolution step in predicate logic, correctness.
    • Substitutions and their composition.
    • Unification, most general unifier.
    • Logic based developement of the unification algorithm.
    • Correctness of the algorithm.
  • No homework.

• Nov. 26: Lecture 7:.
  • Predicate Logic: Completeness of the resolution method
    • The Herbrand universe and its universality.
    • The semantic tree, Herbrand theorem.
    • Completeness of resolution, lifting lemma.
  • Predicate Logic: Sequent calculus
    • Example of proof in natural style: sum of convergent sequences.
    • Sequent rules for universal formulae.
    • Simple examples of sequent proofs.
  • Homework 6: logic-hw-6.pdf, logic-hw-6.tex.

• Dec. 3: Lecture 8:.
  • Predicate Logic: Sequent calculus
    • Correctness of the quantifier rules.
  • Predicate Logic: Equality
    • Approaches to equality: as usual predicate, but with special properties; semantic: modeled by the diagonal relation, or by definition of the truth value using meta-level equality.
    • The main inference rules for equality: substitution and replacement. Their role in computation.
  • Logic vs. Programming: basic notions
    • Examples of rule-based computation: GCD, sum, sort: Mma-programs.pdf.
    • Tail recursive programs, example: improving summation.
    • Proofs by induction: example summation.
    • Transformation of pattern programs in to functional and imperative programs. Additional example: reverse.pdf.
    • The logical aspects of LET, example: powerset.
  • Homework 7: logic-hw-7.pdf, logic-hw-7.tex.

• Dec. 10: Lecture 9:.
  • Logic vs. Programming: program verification:
    • Basic principles of program verification.
    • Verification of functional programs: Functional-Program-Verification.pdf.
  • No homework.

• Dec. 17: Lecture 10:.
  • Logic vs. Programming: program verification:
    • Verification of primitive recursive programs: soundness of verfication conditions.
    • Verification of imperative programs: symbolic-execution-presentation.pdf, symbolic-execution-paper.pdf.
  • No homework.

• Jan. 14: Lecture 11: program verification.

• Jan. 21: Lecture 12: Review of material.

• Jan. 28: Examination cancelled for health reasons .

• Jan. 29: Examination at 16:00 in HS6 .

Homeworks:

Each exercise counts for your final grade. In particular the grade for exercises is based on the homework and on your activity in the class room.

In case you send your homeworks by e-mail, please use my address Tudor.Jebelean@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.