CM20019—Computation III: Formal Logic and Semantics

1Textbook

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.

2News

2.10.06No 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.

3Course Info

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.

Lectures and topics

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

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

9.10.06—Lecture 3Substitutions: 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.

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

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.

20.10.06—Lecture 6Semantics 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.

23.10.06—Lecture 7CNF 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.

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

30.10.06—Lecture 9Semantics 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.

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

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

10.11.06—Lecture 12Semantic 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.

13.11.06—Lecture 13Introduction 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.

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

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

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

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

4.12.06—Lecture 18Other 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.

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

8.12.06—Lecture 20Correctness theorem for tableaux.

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

15.12.06—Lecture 22Gö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.

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

12.1.07—Lecture 24REVISION LECTURE

Material covered and to be prepared for the exam

Courseworks

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.

Complementary Course Notes

Some sheets distributed as Complementary Course Notes are available here:

Exercises

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

4Tutors and Office Hours

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

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 @)