Logic 1

326.019, 326.021 - Mathematical Logic 1, 326.090 Special Topics.

Winter Semester 2017

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 and the place of the lecture is shown in KUSSS. The home page of the lecture in WS 2016 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. 5: 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: Mathematica programs.
    • Termination of programs.
  • Introduction: 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.
  • 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.
    • Semantic equivalence as validity of syntactical equivalence, and as double semantic consequence.
    • Proving semantical logical consequence by refutation.
  • Propositional Logic: Rewriting.
    • 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-1.pdf, logic-hw-1.tex.

• Oct. 12: No Lecture

• Oct. 19: Lecture 2
  • Propositional Logic: Proof Methods.
    • Systematic exploration of interesting equivalences.
    • Using equivalences for transforming formulae: Negation Normal Form, Conjunctive Normal Form, Disjunctive Normal Form.
    • Proving equivalences by reduction to CNF - incompleteness.
    • Proving validity by reduction to CNF - completeness.
  • Homework: logic-hw-2.pdf, logic-hw-2.tex.

• Nov. 9: Lecture 3
  • Propositional Logic: Resolution.
    • The resolution principle: the inference rule, the proof method.
    • Correctness of the proof method.
    • Definition of completeness of resolution.
    • Unit resolution and unit subsumption.
    • The Davis-Putnam-Logemann-Loveland (DPLL) algorithm.
  • Propositional Logic: Sequent Calculus.
    • Sequents, proof trees, axioms, seequent rules as models of elements from natural-style proving.
    • Completeness and correctness of a sequent calculus.
    • Construction of a correct and complete calculus for formulae containing only negation and conjunction.
    • Example of natural-style proof which uses the rule for negation in the assumptions: proof-example.pdf.
    • Construction of the rules for other logical connectives using the previous calculus.
  • Homework: logic-hw-3.pdf, logic-hw-3.tex.

• Nov. 16: Lecture 4: First Order Predicate Logic
  • Basic Notions.
    • Syntax: the language of terms, the language of formulae.
    • Semantics: interpretations, truth evaluation.
    • Quantified equivalences.
    • Normal forms: prenex, CNF.
    • Skolem normal form.
  • Homework: logic-hw-4.pdf, logic-hw-4.tex.

• Nov. 23: Lecture 5: First Order Predicate Logic
  • Resolution.
    • The resolution method in first order predicate logic.
    • Unification.
    • The Herbrand universe.
  • Homework: logic-hw-5.pdf, logic-hw-5.tex.

• Nov. 30: Lecture 6: Completeness of Resolution in First Order Logic
  • Resolution.
    • The universality of Herbrand interpretations.
    • Semantic tree and the Herbrand Theorem.
    • Resolution is complete.
  • Homework: logic-hw-6.pdf, logic-hw-6.tex.

• Dec. 7: Lecture 7: Equality, Computing, Programming
  • Modelling and reasoning about equality.
  • Substitution and replacement as universal computing operations.
  • Conditional rewrite rules as universal programming language. Examples of conditional rewrite programs in Mathematica Mma-programs.pdf.
  • An example of logical-based program development reverse.pdf.
  • A logical based approach to verification of imperative programs symbolic-execution-presentation.pdf, symbolic-execution-paper.pdf.

• Dec. 14: Lecture 8: Program Verification
  • Continuation of presentation of verification of imperative programs.
  • Termination of imperative programs Imperative-Program-Termination.pdf.

• Dec. 11: Lecture 9: Definitions, Algorithm Synthesis
  • Logical rules for correct definitions of functions.
  • Synthesis of sorting algorithms for lists and for binary trees: Sorting-Trees.pdf, Sorting-Tuples.pdf.

• Jan. 18: Lecture 10: Conclusions
  • Review of the material for the examination.

• Jan. 25: Examination
  • Written examination from 8:30 to 10:00.

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.