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.

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.
• 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
• 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