Master Degree in Computer Science
Course on Formal Methods (academic year 2020-2021)

Some notes and exercises

• Introduction to the course, its contents, aims, lecture notes and bibliography, examination and assessment.


• Introduction to equational reasoning and rewriting. Examples of equational theories: concatenation of lists, summation on natural numbers, group theory.


• Abstract reduction systems, normal forms, convertibility, reduction graphs. Confluence and Church-Rosser (CR) property and their equivalence (proof). Uniqueness of normal form (UN). Examples.


• Local confluence (WCR), weak normalization (WN), strong normalization (SN) (or termination and noetherianity) . Principle of noetherian induction (proof).


• Newman Lemma and its proof. Canonicity. Exercises on abstract reduction systems and their properties.


• First order terms: signature, constants, variables, definition of (finite) first order terms. Subterms, positions, contexts. Examples.


• Substitution, matching substitution (match), subsumption ordering, unifying substitution (unifier), syntactic unification of terms. Examples.


• Most general unifier (mgu). Syntactic unification algorithm of the solved form by Martelli and Montanari. Some exercises (Italian version, English version).


• Equational Calculus. Identities and equations, equational deduction, closure properties. Syntactic characterization of the convertibility relation, inference system, proof trees. Equational theories.


• Term rewriting systems, rewrite rules, rewrite relation. Rewriting step, redex, normal form.


• Termination of rewrite systems. Reduction ordering, Lankford theorem, simplification ordering, subterm property.


• Multiset ordering, recursive path ordering (rpo), generalized rpo. Some exercises on termination (Italian version, English version).


• Some midterm written exams of the past few years:
  some questions, December 2010, May 2012, November 2013 (do not consider the questions on critical pairs).


• Midterm written exam 22/04/2016 (exercises and solutions).


• Convertibility of terms in a TRS, its decidability and a decision procedure. Overlapping of rewrite rules, spectrum of rules of a TRS, notion of critical pairs.


• Critical pairs, examples and their convergence (Italian version, English version).
  Huet Lemma (no full proof, just hints and examples of the three cases).


• The word problem in an equational theory and its decidability. Knuth-Bendix theorem and completion of equational theories.


• Inference rules for the completion of equational theories (abstract completion). Completion procedures, termination (success/failure) and divergence. Strategies for completion.
  An example of completion: a fragment of group theory (Italian version, English version).


• Divergence of completion of equational theories. Examples of divergence and divergence patterns (Italian version, English version).


• Semantic unification of terms modulo an equational theory E (E-unification). Solving equations modulo E, E-unifiers, minimal and complete set of E-unifiers. Narrowing relation in a TRS R. E-unification algorithm based on narrowing. Normal narrowing. Basic positions and basic narrowing. Examples (Italian version, English version).


• Propositional logic: boolean formulae, syntax and semantics, truth table. Satisfiability, unsatisfiability, tautology. An example of expressivity of propositional logic: the problem of the N queens.


• Equivalence of formulae, equational axioms, CNF and DNF, transformation of boolean formulae into CNF/DNF. The satisfiability problem and the Davis-Putnam algorithm (introduced through an example).


• Introduction to Natural Deduction for propositional logic: introduction rules and elimination rules. Examples of natural deduction proofs. Comparison between semantic, axiomatic (equational) and proof-theoretic approaches.


• Predicate logic (or predicate calculus or first-order logic, FOL): predicates, functions, variables, quantifiers. Natural deduction for predicate logic and proofs. Prenex DNF. Examples.


• Introduction to higher-order logics and lambda-calculus. Untyped lambda-calculus, lambda-terms syntax, substitution, beta-reduction, beta-normal form, properties and standard conventions. Examples.


• Simple type theory: typed lambda-calculus, signature, context, type judgement. Inference rules for deriving the type of typed lambda-terms (type assignment calculus). Examples. Polymorphism and polymorphic types. Exercises.