"Automated Reasoning" is a second-year mandatory course of the Bachelor's Degree in Artificial Intelligence, taught in the second term.



In this course, we introduce the formal basis of:

A) Logical reasoning: reasoning is the ability to make inferences about some given knowledge, and automated reasoning is concerned with the building and use of computing systems that automate this process.

B) Knowledge representation: we consider the two most widely used logical formalisms, propositional logic and first-order logic.

Additionally, we use state-of-the-art software in a practical way and analyze some of the most important applications in Artificial Intelligence.



In this manner, we enhance and complete the knowledge introduced in some first-year subjects. More specifically:

1) "Discrete Mathematics", where some deductive reasoning systems for propositional and first-order logics are presented.

2) "Programming Methodology", where first-order logic is used as formal specification language.



Along with this subject, the problem of knowledge representation is also addressed in two other second-year courses of the second term, although from different viewpoints: "Databases" and "Artificial Intelligence". Further, some other reasoning methods are studied in the course "Artificial Intelligence", such as rule-based systems.



The knowledge presented in this course serves as a basis or is completed in higher courses of the degree, like "Database Design" (third year) , "Development of Big Data Applications" (third year), "Knowledge-Based Systems" (fourth year) and "Advanced Techniques in Artificial Intelligence" (fourth year).

* Knowledge representation using formal logic languages.

* Proving a conclusion from the given assumptions by the application of mechanical formal system.

* Model and counter-model generation for logical statements.

* Understanding some algorithms and strategies involved for automated deduction.

* Using automated reasoning tools and understanding their outcomes.

1. Mathematical representation of knowledge.

2. Deductive methods and tools for propositional logic.

3. Deductive methods and tools for first-order logic.

4. Applications of automated reasoning in Artificial Intelligence: Prolog.

In the master classes, we describe the theoretical subjects of the course and resolve some practical exercises.



Likewise, in the practical group classes, we resolve some additional exercises by means of using state-of-the-art automated tools.



In both cases, we use active methodologies that encourage students to acquire skills by working, both autonomously and in teams, in order to solve the different proposed objectives. In addition, we encourage the formulation of questions and their discussion, so that students acquire skills related to oral communication, synthesis capacity and teamwork.



In order to facilitate and ensure learning, we monitor and provide feedback on the basis of previously established evaluation criteria, providing students with the opportunity to become aware of their progress.

• Continuous Assessment System
• Final Assessment System
• Tools and qualification percentages:
  • Written test to be taken (%): 70
  • Realization of Practical Work (exercises, cases or problems) (%): 30

The criteria established in the current regulations are applied for the choice of assessment system (continuous or final), and also for changes to the assessment system (from continuous to final). The default assessment mode is continuous. Actually, the subject is oriented to the continuous assessment modality.



=== Continuous evaluation ===



The assessment of the acquired knowledge and skills consists in mid-course exams (70%) and practical exercises (30%).



More concretely, there are 3 mid-course exams. Next, we state the subjects and percentages of the final grade that respectively correspond to each exam:

* First mid-course exam: Propositional logic, 20%.

* Second mid-course exam: First-order logic, 25%.

* Third mid-course exam: Practical applications - Prolog, 25%.



All the tests are marked out of 10 points.



The final grade is obtained by calculating the weighted average of the marks in the mid-course exams and practical exercises.



In any case, in order to pass the course it is compulsory to satisfy the following conditions:

a) Exceed the minimum mark (3 of 10 points) in all the mid-course exams

b) Exceed the minimum mark (5 of 10 points) in the final grade.



=== End-of-course evaluation ===



Changes from continuous assessment to final assessment can be requested as long as a percentage equal to or higher than 80% of the final grade has not been assessed.



Final assessment is made through a written exam, which is marked out of 10 points and gives the final grade of the course.



It is compulsory to exceed the minimum mark (5 of 10 points) in the final grade in order to pass the course.



In order to resign from the evaluation, it is necessary not to take the final written exam.

We apply the criteria stablished for the end-of-course evaluation method of the ordinary examination period.



That is, the assessment is made through a final written exam, which is marked out of 10 points and gives the final grade of the course.



It is compulsory to exceed the minimum mark (5 of 10 points) in the final grade in order to pass the course.



In order to resign from the evaluation, it is necessary not to take the final written exam.

All the resources that are available at the virtual classroom in eGela.

Basic bibliography

"Logic for Computer Scientists". Uwe Schöning. Volume 8 in the series "Progress in Computer Science and Applied Logic". 166 pages. Birkhäuser, 1989. ISBN: 9780817647629. e-ISBN: 13:978-0-8176-4763-6. DOI: 10.1007/978-0-8176-4763-6. Springer, 2008 (reprint).



"Introduction to Logic, Third Edition". Michael Genesereth and Eric J. Kao. Volume 5(1) in the series "Synthesis Lectures on Computer Science". 177 pages. Morgan & Claypool, 2016.ISSN: 1932-1228 (print) 1932-1686 (electronic). DOI:10.2200/S00734ED2V01Y201609CSL008. Online resources available at: http://intrologic.stanford.edu/

In-depth bibliography

"Handbook of Automated Reasoning". Alan Robinson and Andrei Voronkov (editors). 981 pages (Volume I), 1185 (Volume II). The MIT Press (North-Holland), 2001. ISBN: 9780262182218 (Volume I), ISBN: 9780262182225 (Volume II), ISBN: 9780262182232 (Volumes I and II).

Journals

* Journal of Automated Reasoning (https://www.springer.com/journal/10817/)
* Journal of Logic and Computation (https://academic.oup.com/logcom)
* ACM Transactions on Computational Logic (https://dl.acm.org/journal/tocl)
* The Journal of Logic and Algebraic Programming (https://www.sciencedirect.com/journal/the-journal-of-logic-and-algebraic-programming)

Web addresses

The TPTP Problem Library for Automated Theorem Proving: https://tptp.org/
System on TPTP: https://www.tptp.org/cgi-bin/SystemOnTPTP
The CADE ATP System Competition: https://tptp.org/CASC/
Logic Tools: https://logictools.org/