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.