Automated Theorem Proving
Timisoara, Summer Semester 2018
Organization
The first 9 lectures took place in May.
The next lectures are:
- 10 June: 2 lectures 16:20 - 19:30
- 11 June: 2 lectures 16:20 - 19:30
- 13 June: consultations 17:50 - 19:30
- 14 June: examination 17:00 in A02
Homeworks
There are 36 exercises in homeworks.pdf.
For the admission to the examination it is necessary to solve at least 18 exercises before the lectures on 10th of June.
Every additional 9 exercises counts as an additional point at the final mark
of 1 to 10.
(For exercises 32 and 35-36 use the definitions and examples from the lecture notes.)
You can bring the solution to the next lecture or you can send it by e-mail in advance.
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
Popescu-I-3.pdf or Ionescu-P-4.jpg.
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.
Contents
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. The relationship between logic and programming,
see also reverse.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.
- Semantics, Semantics based notions.
- The main principle of semantics:
interpretations, truth value, truth valuation function.
- The truth table.
- 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.
- Using the truth table for proving: validity, semantical equivalence,
semantical logical consequence.
- Sequent Calculus
- Examples of natural style proofs, see also nat-style-proof-and-method.pdf.
- Sequents, proof trees, axioms, sequent rules as models of elements from
natural-style proving.
- 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.
- Completeness and correctness of the "not-and" sequent calculus.
- Construction of the rules for other logical connectives
using the previous calculus.
- Syntax and Semantics Revisited
- Some basic properties of conjunction and disjunction:
idempotence, commutativity, associativity.
- Embedding these properties at syntactic level by considering
conjunctive and disjunctive sets.
- Rewriting to Normal Form
- The use of semantic equivalence for rewriting formulae.
- 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.
- Resolution in Propositional Logic
- 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.
- First Order Predicate Logic:
Syntax, semantics, equivalent transformations, normal forms:
presentation and exercises, and
answers to exercises
Additional Material
Lecture notes: Introduction-to-ATP-Jebelean-5-Jun-2018.pdf.
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.
The home page of the similar lecture in Linz:
WS 2016 may give you an idea about the contents
and the homeworks, although the current lecture will not be exactly the same.
Tudor.Jebelean@jku.at