Logic 1

326.019, 326.021 - Mathematical Logic 1

Winter Semester 2013

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 HS11. The first lecture is on Thu Oct 10.

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 2012 may give you an idea about the contents and the homeworks, although the current lecture will not be exactly the same.

Lectures

• Oct. 10: Lecture 1: Introduction:
• Examples relating Logic to Mathematics and Computer Science:
• Simple law text.
• 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.
• Homework : logic-hw-1.pdf, logic-hw-1.tex.

• Oct. 17: Lecture 2:
• Propositional Logic: Syntax, Semantics, Semantics based notions
• The inductive principle in defining syntax and its applications for function definition and proving.
• 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 : logic-hw-2.pdf, logic-hw-2.tex.

• Nov. 7: Lecture 3:
• Propositional Logic: Rewriting, resolution
• Simplification of truth constants by rewriting.
• Normal forms: NNF, CNF, DNF. The general principle of proving equivalences by rewriting to normal form.
• Proving equivalence by CNF: incompleteness.
• Proving validity by CNF: completeness.
• The resolution principle in propositional logic.
• Correctness and completeness of propositional resolution.
• Homework : logic-hw-3.pdf, logic-hw-3.tex.

• Nov. 14: Lecture 4:
• Propositional Logic: DPLL, natural style proving, sequent calculus
• The DPLL method for SAT solving. The Chaff improvement.
• Natural style propositional proving.
• Sequent calculus: sequent, inference rule, axiom, calculus.
• Homework : logic-hw-4.pdf, logic-hw-4.tex.

• Nov. 21: Lecture 5:

• Nov. 28: Lecture 6:
• Propositional Logic: Sequent calculus
• The "Not-And" calculus. Correctness, completeness.
• Adding "Or" by using the replacement rules.
• The calculus for set based "And", "Or" - propositional.pdf.
• The treatment of truth constants.
• Special rules: modus ponens, subsumption, resolution, implied goal.
• The use of failed sequent proofs.
• Unique-goal sequent calculus.
• Homework : logic-hw-6.pdf, logic-hw-6.tex.

• Dec. 5: Lecture 7:
• Propositional Logic: Sequent calculus
• The cut rule for equivalence.
• Unique-goal calculus: implication and equivalence.
• Proof of completeness revisited.
• First Order Predicate Logic
• Summary of syntax, semantics, rewriting, normal forms, substitution.
• Skolem normal form.
• Herbrand Universe.
• Homework : logic-hw-7.pdf, logic-hw-7.tex.

• Dec. 12: Lecture 8:
• First Order Predicate Logic: The Herbrand Theorem
• Herbrand interpretations and their universality.
• Semantic tree, Herbrand theorem.
• Unification, resolution: correctness, completeness.
• Homework : logic-hw-8.pdf, logic-hw-8.tex.

• Jan. 9: Lecture 9:
• First Order Predicate Logic: Sequent Calculus
• Examples of predicate logic proofs in natural style.
• The quantifier rules, correctness.
• Examples of predicate logic sequent proofs.
• Logic verification of imperative programs
• Syntax of an universal programming language.
• Semantics: translation into a functional program by symbolic execution.
• Slides: program-verification-2012.pdf.
• Homework : logic-hw-9.pdf, logic-hw-9.tex.

• Jan. 16: Lecture 10:
• Review of the homeworks
• Logic verification of imperative programs
• Partial correctness: generation of verification conditions by symbolic execution.
• Termination and total correctness.
• Slides: program-verification-2012.pdf.

• Jan. 23: Lecture 11:
• Review of the material and of the exercises
• Reasoning with equality
• Programming and computing using predicate logic
• Examples using substitution and replacement.
• The role of induction in computation and proving.
• Loop invariants.
• Examples: sum of a sequence, reverse of a list: reverse.pdf.
• Reasoning with equality
• Logic programming: Prolog

• Jan. 30: Examination
• Written examination 8:30 -- 10:00 in HS11.