Brief description of contents: The objective of this subject is to present the fundamental techniques of automated reasoning, as well as the languages of representation of knowledge, with the aim of using them in automatic reasoning tools. We will make emphasis in the relationship between the expressiveness of different languages and the efficiency of automated reasoning. We will also provide the student with some experience in the use of various formalisms and associated automatic tools, in particular, within the framework of one of the most advanced applications of automatic reasoning: the semantic web. The broad contents are mathematical logic and its usefulness in representing knowledge; deductive methods of automatic reasoning on which automatic reasoning tools are based; and logic of descriptions, automatic tools and their applications.
Introduction.
Mathematical representation of knowledge.
Automated deductive methods: Tableaux and Resolution.
