Computational Logic

Damiano Zanardini

Facultad de Informática.
Universidad Politécnica de Madrid.

Compulsory subject of the European Master in Computational Logic.

Last review: February 2011.

Logic Port, from Damiano Zanardini.

REQUIREMENTS AND PRIOR KNOWLEDGE

The student is supposed to dominate basic concepts about logic, usually adquired in a Formal Logic course (which is offered in the same EMCL). In particular, familiarity with the syntax and semantics of propositional and first-order logic is assumed, as well as acquaintance with some proof method (axiomatic, natural deduction, etc.).

An acceptable skill level in mathematics is also welcome, especially as regards the manipulation of symbolic languages, as well as some background in computer science (theory, programming, formal methods).

GENERAL DESCRIPTION OF THE SUBJECT

This course is about the computational part of Mathematical Logic. Here, "computational" refers to what is amenable to be computed by means of an automatic process. In this sense, the goal of Computational Logic is to automatize the operation of proving a fact as a theorem given some prior knowledge (axioms or premises).

OBJECTIVES: KNOWLEDGE AND SKILLS

The student will get in touch with the essential, underlying ideas of computational logic, and methods for automatically proving theorems (semantic trees, Davis-Putnam method, resolution). The course also serves as an introduction to Logic Programming and to state-of-the-art ideas in Automated Theorem Proving.

TEACHING MATERIAL

The teaching material includes class slides, together with some exercises about the whole content.

EVALUATION ACTIVITIES OR PRACTICAL TASKS

The evaluation consists of a written exam which includes a series of exercises.