nireEHU 
Subject
Automated Reasoning
General details of the subject
- Mode
- Face-to-face degree course
- Language
- English
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
| Name | Institution | Category | Doctor | Teaching profile | Area | |
|---|---|---|---|---|---|---|
| HERMO HUGUET, MONTSERRAT | University of the Basque Country | Profesorado Titular De Universidad | Doctor | Not bilingual | Computer Languages and Systems | montserrat.hermo@ehu.eus |
Competencies
| Name | Weight |
|---|---|
| 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
| Type | Face-to-face hours | Non face-to-face hours | Total hours |
|---|---|---|---|
| Lecture-based | 10 | 15 | 25 |
| Applied computer-based groups | 20 | 30 | 50 |
Training activities
| Name | Hours | Percentage of classroom teaching |
|---|---|---|
| Computer work practice, laboratory, site visits, field trips, external visits | 50.0 | 40 % |
| Lectures | 25.0 | 40 % |
Assessment systems
| Name | Minimum weighting | Maximum weighting |
|---|---|---|
| Practical tasks | 40.0 % | 40.0 % |
| Written examination | 60.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.
Temary
- Introduction.- Mathematical representation of knowledge.
- Deductive methods: Tableaux and Resolution.
- Tools for automated reasoning.
Bibliography
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),
2001.