This module focuses on the deductive and algorithmic aspects of both classical and non-classical logics. It introduces logic as a means for specifying and reasoning about a wide spectrum of problems. It emphasizes, in contrast to other similar logic courses, on how logic can be used to represent computational problems and how they can be executed on a computer. Topics covered include classical logic theories, logic programming, modal logic, and

an introduction to non-standard logics. Treatments of propositional and predicate calculus, and temporal logic are fully covered with emphasis on their specification, deductive and algorithmic aspects.

Método de evaluación

A través de las prácticas (50%) y un examen final (50%). El examen será teórico. La prácticas consistirán en resolver un número de problemas usando los diferentes técnicas presentadas en clase.

Temario

Tema1: Lógica proposicional

Sentencias declarativas

Deducción natural

Lógica proposicional como lenguaje formal

Semántica

Normal forms

Tema2: Lógica de predicados

Lógica de predicados como lenguaje formal

Deducción natural

Semántica

Tema 3: Programación Lógica

Clausulas

Modelos de Herbrand

Sustitución, Unificación

Resolucion, resolucion SLD

Tema4: Lógica Temporal

Sintaxis y semántica

Modelos de tiempo

Tableaux Semánticos

Sistemas deductivos

Bibliografía

Logic in Computer Science: Modelling and reasoning about systems
by Michael Huth and Mark Ryan. 2003; Cambridge University Press

Mathematical Logic for Computer Science

by M. Ben-Ari. 2003, Springer-Verlag