We will mainly refer to the following course notes:

*Formal systems, logic and semantics*

by Daniel Richardson

(Last edition: September 2006)

Occasionally, I might provide other references.

*2.10.06*No tutorials this week, they will start on the second week. I have distributed copies of the course notes in class, and I still have spare copies: please collect one at my office (room 1W2.33), if you didn't get a copy yet.

*13.10.06 *I have distributed some complementary notes on Substitutions and Propositional Logic, available as pdf files. You find them below, in the section Complementary Course Notes.

*14.10.06 *Courseworks are now available on the web. Some copies are available also at the Computer Science Department, Office 1W2.23.

*16.10.06 *A typo in coursework 1 has been detected. Please find the amended version below, and apologies for any inconvenience.

*18.10.06 *Tom and Mark have announced their office hours (see below): Tom's one is for tomorrow. I've added a Worksheet in the Exercises section: I haven't completed lecturing on the topic, yet, but I might, by end of this week.

*23.10.06 *Mark has changed his office hours and location: see below the amended version. Tom has his regular office hour on Thursday, for this semester.

*29.10.06 *I've added Worksheet 2 in the Exercise section: I haven't completed lecturing on all the topics you will find there.

*2.11.06 *I've added some complementary course notes (Sheet 3) on predicate logic (semantics, normal forms, logical entailment, Herbrand interpretations). You find them below, in the appropriate section as pdf file.

*10.11.06 *I've added a complementary course notes on Prolog Programming: both as PowerPoint presentation and PDF.

*13.11.06 *I've added on the web the following files: examples of small progarms in Prolog (section complementary course notes) and some small exercises for the laboratories (4 sheets, in the exercise section). Copies of them will be distributed today during the lecture.

*14.11.06 *I've booked a room for presenting the correction of coursework 1 and discussing the most common and recurrent mistakes, following your indications about time: Thursday 16/11/2006, from 13:15 to 14:05, room 8W 3.22. If you like to see the corrections on your individual script, please contact your tutor and arrange for an appointment.

*15.11.06 *A sample solution for coursework 1 is available as pdf in the Courseworks section. I will discuss it in detail tomorrow at the public correction, as previously announced.

*20.11.06 *I need to CANCEL the lecture on 1st December because of a clash with a research meeting out of Bath. The lecture will be recovered on Wednesday 6 December, at 13:15 in room 3E 3.8.

*4.12.06 *I have distributed a sheet with Gentzen system LK (sequent calculus) for classical logic. You may find a pdf below.

*6.12.06 *Today's extra lecture will be used to present a public correction of coursework 2 and discuss common and frequent mistakes. A print-out of a sample solution will be distributed; this will be made available on the web soon, for download.

*8.1.07 *Today's there is a revision lecture. I will also distribute a sample solution of Coursework 3, and this is available below, in the Courseworks section, as PDF file. No information about the marking will be provided, though. This week, revision tutorials and lectures will run as usual.

*11.1.07 *After the request of some students, I've uploaded: 1) a magnified and better readable version of system LK; 2) the slide used in lectures with the rule for building semantic tableaux (it is the same as in Richardson's notes, but more compact); 3) a slide which resumes the axioms in HIlbert-Frege calculi, propositional case. You find them as PDF among the Complementary Course Notes.

In the following, I will link some material distributed or used in the past for this course. Please disregard any information related to the organisation of the course: it is possibly not valid any more. Also, keep in mind that I might change the presentation, sometimes substantially, of the textbook we will use. It is anyway a good idea to try and solve the problems listed at the end of several sections in the course notes. The material we cover is clearly indicated below. Sometimes I will provide Complementary Course Notes, available as pdf, below.

*2.10.06—Lecture 1*Introduction to the course and notions of *formal system,* *string rewriting systems* and *generating grammar*.

- Before the next lecture, please recall the following notions and terminology you have seen during the courses Computation I and Computation II: grammars and languages, Church-Rosser confluence, propositional classical logic, proofs by induction and contradiction.
- Do all the examples and exercises that you find in Richardson's notes, sections 1 and 2.

*6.10.06—Lecture 2**More on Grammars*: *Terminal, Non-terminal symbols, Problem 2.2.
Term languages: definition of term, interpretation*

- Before the next lecture, please read about substitutions and unification.
- Do all the examples that you find in Richardson's notes, section 3, up to page 22.

*9.10.06—Lecture 3**Substitutions: definition of substitution and basic notions (domain, range of a substitution, variables in the codomain, substitution restricted to a set of variables, binding). Renaming; Application of a substitution to a term; some properties (Problem 3.2). Valuations vs substitutions.*

- Before the next lecture, please read about unification and most general unifiers.
- Complete reading chapter 3 in Richardson's notes.

*13.10.06—Lecture 4**Substitutions: Composition of substitutions, Unifiers, Most General Unifiers. Unification Algorithm. Introduction to Propositional Logic (Syntax) *

- Before the next lecture, please read about Propositional Logic, in the complementary sheet I've distributed today (available below).
- Do all examples of unifiers in Richardson's notes.

*16.10.06—Lecture 5 **Syntax of Propositional Logic (cont'd): a grammar generating the language of propositional logic formulae. Principles of structural induction and of structural recursion. Semantics of Propositional Logic: Interpretations and truth tabling. *

- Before the next lecture, please read about Propositional Logic, in the complementary sheet already distributed (available below).
- Invent some propositional logic formula and practice the construction of truth tables.

*20.10.06—Lecture 6**Semantics of Propositional Logic (cont'd): notions of validity, satisfiability, falsifiability, unsatisfiability, tautology, logical consequence, theory. Some logical equivalences. Deduction Theorem. Relation between validity and unsatisfiability of dual formulae. Replacement Theorem. Normal forms: CNF, DNF, Clausal Form. An algorithm to return CNF and DNF based on equivalent formulae.*

- Before the next lecture, please read Chapter 4 in the course notes, sections 4.1 up to 4.11 included and 4.14 (conjunctive and disjunctive normal forms only): this latter gives you an alternative algorithm you may apply to propositional logic formulae to find CNF and DNF based on analysis of truth tables.
- Practice the concepts covered up to now with exercises you may find in the Worksheet 1 (see below, among the Exercises).

*23.10.06—Lecture 7**CNF and DNF obtained from the truth table. Syntax of first order predicate logic: formulae, bound and free occurrences of variables, scope of a quantifier, application of a substitution to a formula. Example of translations from informal language to formulae in propositional and in first order predicate logic.*

- Before the next lecture, please read about the semantics of first order predicate logic (sections 4.8 4.9, 4.10).
- Practice the concepts covered up to now with examples and exercises in the course notes. Consider problem 4.4 page 53 (translation into first order language of some statement in natural language).

*27.10.06—Lecture 8**Semantics of first order predicate logic: evaluation, interpretation of function and predicate symbols, satisfiability of a formula given an interpretation and an evaluation. Typed variables.*

- Before the next lecture, please complete reading chapter 4; in particular in the section on Normal Forms, read about Prenex Form and Skolem Form.
- Practice the concepts covered up to now with examples and exercises in the course notes. Consider also the example 1 in 4.19.

*30.10.06—Lecture 9**Semantics of first order predicate logic: model of a formula and of a set of formulae, some logical equivalences, Skolemisation transformation and its properties. An algorithm to produce CNF preserving unsatisfiability.*

- Before the next lecture, please read about Logical Entailment and Herbrand Models in the complementary course note n.3 you'll find below.
- Practice the Skolemisation process, referring to the examples in the note n.3 or inventing some formula yourself. You might also like to consider some of the exercises in the Worksheet 2 below.

*3.11.06—Lecture 10**Prenex Normal Form and examples of transformations. Notions of Herbrand Universe, Herbrand Base and Herbrand Model and examples. Statement of Herbrand Theorem. *

- Before the next lecture, please read in the course notes about the Semantic Tableaux, Chapter 5, up to page 67 (section 5.4 excluded).
- Practice the construction of Herbrand universe and base for some first order formula of your choice, and try to find Herbrand models for your formula, or Herbrand interpretations that falsify your formula.

*6.11.06—Lecture 11**Method of Semantic Tableaux: the propositional case. Correctness and Completeness (only the statement). Examples and strategies in rules' application.*

- Before the next lecture, please complete reading in the course notes Chapter 5 (correctness and completeness of the method), and read Chapter 6 only the section 6.1 (Resolution and Unification).
- Practice the construction of Tableaux, in the propositional case, following different strategies (e.g. following the chronologically order in which formulae are produced, or by applying, as far as possible, non-branching rules before any branching ones).

*10.11.06—Lecture 12**Semantic Tableaux: rules for quantifiers and notion of parameter. Strategies in rules' application. Examples of usage of the method. Main results. The method of Resolution in propositional and first order case (with Unification) and examples.*

- Before the next lecture, please complete reading in the course notes Chapter 6.
- Practice the construction of Tableaux, in the first order case, to prove that a formula is a tautology, or that a formula is logical consequence of a given set of formulae, or to show that a formula is not valid. Practice the method of resolution, in propositional and first order case.

*13.11.06—Lecture 13**Introduction to Prolog Programming: preliminary concepts (procedure definition and call, computation, success computations, finite failure, infinite computations, multiple answers, answers as logical consequences, variable arguments and unification), Prolog Terms, deterministic evaluations.*

- Before the next lecture, please read in the Prolog slide presentation about non-deterministic evaluations, influencing efficiency, unification, list processing, type checking, primitives for comparing terms (up to p. 48)
- Consolidate understanding of the concepts covered so far with the small examples of Prolog programs provided as complementary course notes. Practice some programming referring to the lists of laboratories exercises available in the Exercise section.

*17.11.06—Lecture 14**Prolog Programming: non-deterministic evaluations, influencing efficiency (tail recursive programming), unification, list processing, type checking, some primitives for comparing terms and for comparing arithmetic expressions.*

- Before the next lecture, please read in the Prolog slide presentation about disjunction, negation, generate-and-test, call terms, aggregation,controlling search by means of cut,influencing efficiency, unification, list processing, type checking, primitives for comparing terms (up to p. 84)
- Consolidate understanding of the concepts covered so far with the small examples of Prolog programs provided as complementary course notes. Practice some programming referring to the lists of laboratories exercises available in the Exercise section.

*20.11.06—Lecture 15**Prolog Programming: disjunction, negation, generate-and-test, call terms, aggregation, controlling search with cut.*

- Before the next lecture, please complete reading the Prolog slide presentation on Meta-programming.
- Consolidate understanding of the concepts covered so far with the small examples of Prolog programs provided as complementary course notes. Practice some programming referring to the lists of laboratories exercises available in the Exercise section.

*24.11.06—Lecture 16**Prolog Programming: Meta-Programming, Built-In Meta-predicates, Meta-Variables, Meta-Interpreters. Language Recognisers.*

- Before the next lecture, please read section 9 on Prolog in Richardson's course notes, especially the examples of programs for treating Equivalence Relations (paragraph 9.15), Language Recognisers (paragraph 9.17), Theorem Provers (paragraph 9.18).
- Consolidate understanding of the concepts covered so far with the small examples of Prolog programs provided as complementary course notes. Practice some programming referring to the lists of laboratories exercises available in the Exercise section. You may also refer to the problems listed in paragraph 9.19 of Richardson's course notes.

*27.11.06—Lecture 17**Other deductive systems for classical logic: Axiomatic systems (Hilbert-Frege calculus), in the propositional case. Examples.*

- Before the next lecture, please read section 6 on other deductive systems in Richardson's course notes.
- Practice deriving some propositional tautology in the Hilbert-Frege calculus.

*4.12.06—Lecture 18**Other deductive systems for classical logic: Sequent Calculus, Gentzen's system LK. Top down and bottom up reading of rules. Example of derivations of tautologies, in propositional and first order case.*

- Before the next lecture, please read chapter 5.4 about Gödel completeness theorem and correctness of the tableau method.
- Practice deriving some tautology in system LK.

*6.12.06—(Extra) Lecture 19**Public correction of coursework 2 and discussions.*

- PDF of a sample solution is available below in the Coursework section. Some copies have been made available in class.

*8.12.06—Lecture 20**Correctness theorem for tableaux.*

- Before the next lecture, read again the proof explained today (based on Richardson's notes section 5.4.1).
- Please complete the proof of the lemma, by completing the case analysis with the other rules of construction for the tableau as suggested during the lecture.

*11.12.06—Lecture 21**Gödel completeness theorem (on tableaux).*

- Before the next lecture, please read in Dan Richardson's course notes the following parts: Peano Axiomatisation of arithmetic (language L_N at p. 41), ZF set theory (chapter 7), Gödel incompleteness theorems (chapter 8).
- Please complete the proof of the internal lemma presented today, by completing the case analysis for formulae that may occur on an infinite branch (section 5.4.1 in Richardson's notes).

*15.12.06—Lecture 22**Gödel incompleteness theorems: general discussion on the aims, Peano axiomatisation of Arithmetics, Gödel encodings, hints on how to build a Turing machine to recognise numbers that are Gödel numbers. First incompleteness theorem: sketched proof (there is a statement in formal arithmetic which is true and representable, but not provable in formal arithmetic). 2nd incompletenss theorem: only the statement.*

- The incompleteness theorem will not be part of the final examination.
- You may find detailed presentations of Gödel incompleteness theorem in any book and textbook in mathematical logic. A less formal presentation that closely meets the purposes of this lecture is in: "J.N Crossley et al. - What is Mathematical Logic ? Dover publication (Paperback) 1990. ISBN 0486264041."

*8.1.07—Lecture 23**REVISION LECTURE -- Correction of coursework 3, discussion. Q&A in preparation for the exam.*

- I've distributed a sample solution for te coursework 3, available as PDF file, below. Grades unfortunately cannot be released at this time, so please do not ask for them.

*12.1.07—Lecture 24**REVISION LECTURE *

- In principle, all what has been covered and is listed in Lectures and topics.

Three courseworks will contribute globally for the 25% of the final assessment. Please read carefully the information at the first page of each coursework (submission process, deadlines, and general information on the single coursework), as it differs in the three cases.

- Coursework 1 (due on 26.10.06) and a sample solution (added on 15.11.06)

- Coursework 2 (due on 16.11.06) and a sample solution (added on 7.12.06)

- Coursework 3 (due on 14.12.06) and a sample solution (added on 8.1.07)

Some sheets distributed as Complementary Course Notes are available here:

- Substitutions (13.10.06)
- Propositional Logic (13.10.06)
- Semantics of Predicate Logic (2.11.06)
- Prolog Programming as PowerPoint presentation (1.4MBytes) or Colour PDF (10.11.06)
- Small Examples of programs in Prolog, to consolidate understanding (13.11.06)

- System LK (4.12.06, replaced with a magnified version on 11.1.07 )

- A slide used in lectures, with the rules for building Semantic Tableaux (11.1.07)

- A slide on propositional Hilbert-Frege calculi, example of Axiomatic systems (11.1.07)

In addition to those in the course notes, consider looking into these exercises: they can be discussed in tutorials.

- Worksheet 1 (added on 18.10.06): Terms, Substitutions, Unification, Propositional Logic
- Worksheet 2 (added on 29.10.06): Predicate Logic: Syntax, Semantics, Normal Forms
- Exercises for Prolog Laboratories (added on 13.11.06): Part 1, Part 2, Part 3, Part 4.

Tom Gundersen (replace AT by @), Carina Murman (replace AT by @), Jonty Needham and Mark Price.

- Tom's office hour: Thursdays 1:15 - 2:05pm, in 8W 2.4.
- Mark's office hour: Mondays 10:15-11:05am, in 4E 2.61.

When you want to talk to me, just drop me an email and we'll arrange for an appointment.

15.1.07Paola Bruscoliemail (replace AT by @)