Logic 1

Mathematical Logic 1

Winter Semester 2018

The course is an introduction to logic for students in Computer Science and Mathematics.

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 2017 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. 9: 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.

• Oct. 16: Lecture 2: :
  • 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.
  • Homework: logic-hw-1.pdf, logic-hw-1.tex.

• Oct. 23: Lecture 3: :
  • Propositional Logic: Pragmantics.
    • The main goals of pragmatics: prove validity, inconsistency, equivalence, logical consequence. The relations between the goals.
    • Systematic exploration of interesting equivalences.
    • Conjunction applied to sets: syntax, semantics, properties.
    • Proving equivalence by rewriting: normal forms.
    • Negation Normal Form (NNF) and demo.
    • Homework: logic-hw-2.pdf, logic-hw-2.tex.

• Nov. 6: Lecture 4: :
  • Propositional Logic: Rewriting.
    • Disjunctive sets.
    • Using CNF, DNF for proving equivalences, combinatorial growth, incompleteness.
    • Completeness of CNF for validity.
    • Resolution: correctness, completeness.
    • The DPLL method, efficient implementation (Chaff).
  • Homework 3: logic-hw-3.pdf, logic-hw-3.tex.

• Nov. 13: Lecture 5: :
  • Propositional Logic: Sequent calculus.
    • Proving in natural style.
    • Sequent calculus: sequent, inference rule, proof tree.
    • The "Not-And" calculus, correctness.
  • Homework 4: logic-hw-4.pdf, logic-hw-4.tex.

• Nov. 20: Lecture 6: :
  • Propositional Logic: Sequent calculus.
    • Extending the sequent calculus with rules for new logical connectives.
    • The sequent rules for Modus Ponens, subsumption, and unit resolution.
  • First Order Predicate Logic: Syntax.
    • Examples of formulae in predicate logic.
    • Syntax: alphabet, terms, formulae.
  • Homework 5: logic-hw-5.pdf, logic-hw-5.tex.

• Dec. 4: Lecture 7: :
  • Propositional Logic: Sequent calculus.
    • Unique-goal sequent calculus.
    • Sequent calculus with unit propagation.
  • First order predicate logic.
    • Quantifiers, bound variables, free variables.
    • Semantics: interpretation with domain, truth evaluation using assigments.
    • Validity, satisfiability, logical consequence, equivalence.
    • Rewriting using equivalence, special equivalences for quantifiers.
  • Homework 6: logic-hw-6.pdf, logic-hw-6.tex.

• Dec. 11: Lecture 8 :
  • First order predicate logic.
    • Normal forms: CNF, prenex, Skolem, standard.
    • The resolution method in first order predicate logic.
    • Unification, the unification algorithm.
    • Herbrand universe, Herbrand interpretations and their universality.
    • The Herbrand Theorem, the Herbrand proving procedure - partial completeness.
    • Semantic tree, partial completeness of the resolution method in first order predicate logic.
  • Homework 7: logic-hw-7.pdf, logic-hw-7.tex.

• Jan. 7: Lecture 9 :
  • First order predicate logic.
    • Resolution example.
    • Sequent calculus in first order predicate logic.
    • The rules for quantifiers and their correctness.
  • Reasoning with equality.
    • Equality as a predicate with special properties.
    • First order logic with equality defined at semantic level.
    • Substitution and replacement, computation using logic formulae.
  • Homework 8: logic-hw-8.pdf, logic-hw-8.tex.

• Jan. 14: Lecture 10 :
  • Relations between logic and computation.
    • Tail recursive functions, program transformation, additional example reverse.pdf.
    • Prolog versus resolution.
    • Programming paradigms: pattern matching, functional programming, imperative programming.
    • Verification of imperative programs program-verification-2012.pdf.
  • Homework 9: logic-hw-9.pdf, logic-hw-9.tex.

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.