MC213 Applied Logic

Next: MC222 Optimisation Up: Year 2 Previous: MC211 Automata, Languages and

MC213 Applied Logic

Credits: 20

Convenor: Dr. S. Ambler

Semester: 2

Prerequisites:	essential: MC111	desirable: MC103, MC104, MC208
Assessment:	Continual assessment: 30%	Three hour exam in May/June: 70%

Lectures:	36	Classes:	none
Tutorials:	12	Private Study:	96
Labs:	6	Seminars:	none
Project:	none	Other:	none
Total:	150

Explanation of Pre-requisites

The course requires a knowledge of basic discrete mathematics, in particular, the properties of sets, functions, relations and trees. In addition, students should already have had an introduction to logic and be familiar with propositional logic, truth tables, tableaux, and with the language of the predicate calculus.

A knowledge of functional programming is also desirable because some of the software to be used is written in Haskell.

Course Description

Logic is the science of reasoning. The principles of deduction have long been studied by philosophers and mathematicians. It is interesting to see how their ideas have become important in Computer Science. One of the main fields of application is in formal specification. If we wish to reason about the behaviour of a computer system before it has been fully implemented then we must try to infer its properties on the basis of a system specification. To be sure that our predictions are correct we must make certain that each step of reasoning is sound. The permissible steps in a logical deduction can be coded as a series of rules written in the formal language of the predicate calculus. What we need to do is to make sure that we follow the rules; in fact, this can be checked on a computer using a proof assistance package. A second field of application is in Artificial Intelligence. If logical deduction can be expressed as a series of rules then it opens the way for us to write programs which can reason for themselves automatically. This is a far more difficult goal. Nevertheless, the idea of logic programming stems from this and has gained widespread industrial use. Both of these are very active areas of research.

There are two main aspects to the study of formal logic. The first is concerned with the syntax of the language and the rules which are used for deduction. This is the proof theory of the logic and provides the basis for machine implementation. The second is concerned with the meaning of the language. We would like to know that the rules are sound and adequate to the task. This is achieved by looking at the model theory of the logic. This module covers the essential core of these ideas and lays the foundation of knowledge which any computer scientist using formal logic should have.

Aims

The course aims to present the concepts of formal logic from a computational point of view. The use of the predicate calculus as a tool for reasoning about computer systems is illustrated through a number of examples. The concepts are then developed in methodical way. The student will see how the basic notions of `truth in a model' and semantic consequence lead to proof methods given by tableaux and sequent calculus. The correctness of these methods is established by proving soundness and completeness theorems. A proof assistance package is then used to support the development of formal proofs, and the student will learn about the basic algorithms that underlie the package. These ideas are developed further with the introduction of logic programming. The course ends with some elementary programming exercises in Prolog.

Objectives

To be able to translate an English description into sentences of the predicate calculus and vice versa;
to understand the concept of `truth in a model' and be able to construct a model in which particular sentences are true;
to understand the notion of semantic consequence: to be able to show when it holds and use counter-models to show when it does not;
to learn the inductive proof techniques required to show standard results about terms, formulae and proofs;
to be able to prove a sequent valid using the tableau method or sequent calculus (in either the basic or meta-variable version);
to gain experience with the proof assistance package Verity;
to understand the key steps in proving the soundness and completeness theorems;
to understand the techniques of unification and linear resolution and to be able to apply this in logic programming to derive SLD-trees;
to be able to write simple programs in pure Prolog.

Transferable Skills

The logical background which is essential to appreciate much of the work in formal specification (see MC301 and MC302);
a secure understanding of the principles of logic programming and the ability to write simple Prolog programs;
further inductive proof techniques;
an important grounding for anyone who wants to go on and do research in the applications of formal logic.

Syllabus

Predicate logic: examples; review of the syntax; free and bound variables; term substitution. Models and validity; semantic consequence; counter models; the tableau method (basic and meta-variable versions). Proof theory: sequent calculus (basic and meta-variable); derived rules and admissible rules. Machine assisted proof. Soundness and completeness: Herbrand models, Hintikka sets and the algorithm Search. Proof search: first order unification; linear resolution; search strategies. Pure Prolog: definite clauses, SLD trees, simple logic programming.

Reading list

Background:

A. Galton, Logic for Information Technology, John Wiley and Sons, 1990 (out of print).

M. Fitting, First-order Logic and Automated Theorem Proving, Springer-Verlag, 1990.

M. Ben-Ari, Mathematical Logic for Computer Science, Prentice Hall, 1993.

Details of Assessment

There is a series of nine worksheets, which are all assessed. These include pen and paper exercises, but also computer work using the proof assistant Verity and logic programming in Prolog.

The written Midsummer examination has six questions and candidates can obtain full marks for good answers to four questions. The examination is intended to cover all aspects of the course except for the laboratory work.

Next: MC222 Optimisation Up: Year 2 Previous: MC211 Automata, Languages and

Roy L. Crole
10/22/1998