XSL Content

Automated Reasoning

General details of the subject

Face-to-face degree course

Description and contextualization of the subject

The overall aim of the course is to describe how reasoning can be modeled using computers. Its more specific aim is to provide a route into more advanced uses of theorem proving in order to solve problems.

Major emphases are on: how knowledge can be represented using propositional and first-order logic; how these representations can be used as the basis for reasoning; what are the main mechanisms that allow reasoning in propositional and first-order logic; and how these reasoning processes can be guided to a successful conclusion through a variety of automated tools.

Teaching staff

NameInstitutionCategoryDoctorTeaching profileAreaE-mail
HERMO HUGUET, MONTSERRATUniversity of the Basque CountryProfesorado Titular De UniversidadDoctorNot bilingualComputer Languages and


Ability to manage and adapt the most relevant symbolic methods for research in language technologies.20.0 %
Ability to establish how to design and use computer applications of automatic reasoning.20.0 %
Identify and apply knowledge representation techniques.30.0 %
Understanding the basic strategies of automatic reasoning and further their application in specific applications.30.0 %

Study types

TypeFace-to-face hoursNon face-to-face hoursTotal hours
Applied computer-based groups203050

Training activities

NameHoursPercentage of classroom teaching
Computer work practice, laboratory, site visits, field trips, external visits50.040 %
Lectures25.040 %

Assessment systems

NameMinimum weightingMaximum weighting
Practical tasks40.0 % 40.0 %
Written examination60.0 % 60.0 %

Learning outcomes of the subject

Identify problems that require mathematical representation of knowledge.

Ability to represent knowledge in propositional and first-order logic.

Knowledge of the basic deduction methods used in automatic reasoning tools.

Ability to handle automated reasoning tools and understand the results they produce.

Implementation of specific tasks that require automated reasoning.


- Introduction.

- Mathematical representation of knowledge.

- Deductive methods: Tableaux and Resolution.

- Tools for automated reasoning.


Basic bibliography

- Logic for Computer Scientists. Uwe Schöning. "Progress in Mathematics". Springer, 2008.

- V. Sperschneider, G. Antoniou, Logic: a foundation for computer science, Addison-Wesley, 1991.

- M. Anthony and N, Biggs. Computational Learning Theory. An Introduction, Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1992.

- Handbook of Automated Reasoning. Alan Robinson and Andrei Voronkov. The MIT Press (North-Holland),