Logic 1
Mathematical Logic
Winter Semester 2019
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.
Lectures
- 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: 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.
- Truth table, example of showing equivalence by truth table.
- Homework:
logic-hw-1.pdf,
logic-hw-1.tex.
- Oct. 15: Lecture 2:
- Propositional Logic: Pragmantics.
- The main goals of pragmatics:
prove validity, inconsistency, equivalence, logical consequence.
The relations between the goals.
- Propositional Logic: Rewriting.
- Systematic exploration of interesting equivalences.
- Conjunction applied to sets: syntax, semantics, properties: Conjunctive-Disjunctive-Sets_25-Oct-2019.pdf.
- Proving equivalence by rewriting: normal forms.
- Negation Normal Form (NNF) and demo,
Conjunctive Normal Form (CNF), combinatorial growth.
- Completeness of CNF for proving validity.
- Homework:
logic-hw-2.pdf,
logic-hw-2.tex.
- Oct. 22: 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.
- DPLL efficient implementation: the Chaff algorithm.
- Propositional Logic: Sequent Calculus.
- Homework:
logic-hw-3.pdf,
logic-hw-3.tex.
- Overview of the previous lectures: Overview-of-Propositional-Logic_25-Oct-2019.pdf.
- Oct. 29: Lecture 4
- Propositional Logic: Sequent Calculus.
- The "Not-And" calculus: correctness, completeness.
- Extending the calculus for the other logical connectives.
- Special rules: modus ponens, implied goal, unit resolution, unit subsumption.
- Sequent calculus with unit propagation.
- Homework:
logic-hw-4.pdf,
logic-hw-4.tex.
- Nov. 11: Lecture 5:
- Propositional Logic: Sequent Calculus.
- The rules for truth constants.
- The rules for conjunctive and for disjunctive sets.
- Unique goal sequent calculus.
- Implementation of sequent calculus in Theorema.
- Homework:
logic-hw-5.pdf,
logic-hw-5.tex.
- Nov. 19: Lecture 6
- Propositional Logic: Sequent Calculus.
- First Order Predicate Logic.
- Syntax: term, formula.
- Semantics: interpretation, truth evaluation rules.
- Homework:
logic-hw-6.pdf,
logic-hw-6.tex.
- Nov. 26: No lecture
- Dec. 3: Lecture 7
- First Order Predicate Logic.
Equivalences of quantified formulae.
- Rewriting, normal forms: NNF, prenex, Skolem.
- The resolution method: correctness.
- Homework:
logic-hw-7.pdf,
logic-hw-7.tex.
- Dec. 10: No lecture
- Dec. 17: Lecture 8
- Jan. 7: Lecture 9
- First order logic.
- Completeness of resolution: Herbrand Universe, Herbrand interpretations, the Herbrand Theorem, the semantic tree.
- Sequent calculus: sequent rules for universally quantified formulae.
- Homework:
logic-hw-9.pdf,
logic-hw-9.tex.
Jan. 14: Lecture 10
- First order logic.
- Sequent calculus.
- Reasoning with equality.
- Computing via substitution and replacement.
- Special proof techniques: illustration with an epsilon-delta proof.
- Homework:
logic-hw-10.pdf,
logic-hw-10.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.
T. Jebelean