Computational Logic
Code: 106569 ECTS Credits: 6| Degree | Type | Year |
|---|---|---|
| 2504392 Artificial Intelligence | FB | 1 |
Contact
- Name:
- Vicente Costa Bueno
- Email:
- vicente.costa@uab.cat
Teaching groups languages
You can view this information at the end of this document.
Prerequisites
There are no prerequisites.
Objectives and Contextualisation
As a knowledge representation formalism, a reasoning system, an analytical tool, or even a programming language, the function of logic in artificial intelligence (AI) has been prominent since the inception of the discipline. The objective of this course is, therefore, to delve into the role of logic within AI, by providing students with an understanding of its fundamental concepts, techniques, and methods. This will enable them to proficiently apply logic across these varying facets of AI.
Competences
- Analyse and solve problems effectively, generating innovative and creative proposals to achieve objectives.
- Develop critical thinking to analyse alternatives and proposals, both one's own and those of others, in a well-founded and argued manner.
- Identify, understand and apply the fundamental concepts and techniques of knowledge representation, reasoning and computational learning for the solution of artificial intelligence problems.
- Know, understand, use and apply appropriately the mathematical foundations necessary to develop systems for reasoning, learning and data manipulation.
- Students must have and understand knowledge of an area of study built on the basis of general secondary education, and while it relies on some advanced textbooks it also includes some aspects coming from the forefront of its field of study.
- Work independently, with responsibility and initiative, planning and managing time and available resources, and adapting to unforeseen situations.
Learning Outcomes
- Analyse and solve problems effectively, generating innovative and creative proposals to achieve objectives.
- Develop critical thinking to analyse alternatives and proposals, both one's own and those of others, in a well-founded and argued manner.
- Students must have and understand knowledge of an area of study built on the basis of general secondary education, and while it relies on some advanced textbooks it also includes some aspects coming from the forefront of its field of study.
- Understand problem modelling for logic programming languages and how to resolve them using satisfiability-based algorithm.
- Understand the basic notions and mathematical foundations of classical logical formalisms, automatic reasoning techniques and argumentation in AI.
- Understand the usefulness of theorem provers for solving problems represented in a logical language.
- Work independently, with responsibility and initiative, planning and managing time and available resources, and adapting to unforeseen situations.
Content
Part I. Propositional Logic (Truth-functional Logic, TFL)
I.1 Syntax of TFL (alphabet, connectives, sentences...).
I.2 Semantics of TFL (truth-functional connectives, characteristic truth tables, complete truth tables, partial truth tables...).
I.3 Natural language formalization in TFL (and its limitations).
I.4 Reasoning in TFL (e.g., rules, tree-search algorithms...).
I.5 Normal Forms and Logic Data Structures.
Part II. First-Order Logic (FOL)
II.1 Syntax of FOL (quantifiers, formulas, sentences...).
II.2 Semantics of FOL (extensionality, interpretations...).
II.3 Natural language formalization in FOL (and its limitations).
II.4 Resolution for TFL (transform formulas into normal forms).
II.5 FOL and Databases
Activities and Methodology
| Title | Hours | ECTS | Learning Outcomes |
|---|---|---|---|
| Type: Directed | |||
| Exercise in class | 30 | 1.2 | 2, 3, 6 |
| Introduction and discussion of the main theoretical concepts | 12 | 0.48 | 5 |
| Type: Supervised | |||
| Assimilation of theoretical concepts | 10 | 0.4 | 1, 6 |
| Reinforcement and follow-up in the resolution of exercises | 12 | 0.48 | 2 |
| Type: Autonomous | |||
| Autonomous work and readings | 38 | 1.52 | 7 |
| Preparing and solving exercises | 42 | 1.68 | 2, 3, 6, 7 |
The course methodology is based on short lectures by the professor, problem-solving during class time (specifically, students will engage in individual or group practices to reinforce their learning of the lesson and do evaluative exercises), and flipped learning (that is, students will complete the lectures with readings and work at home). In some classes, time will be kept for reviewing and correcting the evaluative practices.
Annotation: Within the schedule set by the centre or degree programme, 15 minutes of one class will be reserved for students to evaluate their lecturers and their courses or modules through questionnaires.
Assessment
Continous Assessment Activities
| Title | Weighting | Hours | ECTS | Learning Outcomes |
|---|---|---|---|---|
| Evaluative tests | 50% | 4 | 0.16 | 1, 4, 5, 7 |
| Exam | 50% | 2 | 0.08 | 1, 2, 3, 6, 7 |
The assessment can be carried out in the two ways described below.
Continuous Assessment.
On one hand, students must take two evaluative tests (ET1 and ET2) in the classroom and during class hours; ET1 is expected to be held at the end of October, while ET2 will take place at the end of November. On the other hand, an individual final exam (FE) will be done, covering the content of parts I and II. The date of the FE will be determined by the exam schedule set by the Faculty.
To be eligible for continuous assessment, the student must have completed at least one ET and the EF. The final grade for the course in this modality will be determined as follows (all grades are out of 10).
If FE_grade < 4, then the student will not have passed the continuous assessment and, if meeting the pertinent conditions, will be able to take the recovery (see the Recovery section).
Otherwise, the final grade for the course will be determined using the following formula: final_grade = max{0.5 * FE_grade + 0.25 * ET1_grade + 0.25 * ET2_grade, FE_grade}.
Single Assessment.
The student will take the FE and two additional exercises (E1 and E2), one for each corresponding test in the other assessment modality. The final grade for the course in this modality will be determined as follows.
If FE_grade < 5 or E1_grade < 5 or E2_grade < 5, then the student will not have passed the single assessment and, if meeting the pertinent conditions, will be able to take the recovery (see the Recovery section).
Otherwise, the final grade for the course will be determined using the following formula: final_grade = 0.5 * FE_grade + 0.25 * E1_grade + 0.25 * E2_grade.
Recovery.
To be eligible for the recovery, students must have completed the FE and at least one evaluative test (continuous assessment) or one additional exercise (single assessment). Only an individual final recovery exam(FRE) will be done. To pass the course in this modality, the FRE_grade must be equal or greater than 5. Regarding the final grade, final_grade = FRE_grade.
On carrying out each evaluation activity, lecturers will inform students (on Moodle) of the procedures to be followed for reviewing all grades awarded, and the date on which such a review will take place.
In the event of a student committing any irregularity that may lead to a significant variation in the grade awarded to an assessment activity, the student will be given a zero for this activity, regardless of any disciplinary process that may take place. In the event of several irregularities in assessment activities of thesame subject, the student will be given a zero as the final grade for this subject.
In the event that tests or exams cannot be taken onsite, they will be adapted to an online format made available through the UAB’s virtual tools (original weighting will be maintained). Homework, activities, and class participation will be carried out through forums, wikis, and/or discussions on Teams, etc. Lecturers will ensure that students are able to access these virtual tools, or will offer them feasible alternatives.
Bibliography
Basic bibliography:
Teacher's notes (available at the Campus Virtual and updated throughout the course).
Complementary bibliography:
P. D. Magnus, Forallx, University at Albany. With additions under a Creative Commons License by T. Button, J. R. Loftis, and R.Trueman, 2021, http://forallx.openlogicproject.org/.
M. Ben-Ari: Mathematical Logic for Computer Science. Springer, 2012.
J. van Benthem, H. van Ditmarsch, J. van Eijck, J. Jaspars. Logic in Action. Open Course Project, 2016, https://www.logicinaction.org/.
D. Barker-Plummer, J. Barwise, J. Etchemendy. Language, Proof and Logic. CSLI Publications, 2011, second edition.
Software
To be determined.
Language list
| Name | Group | Language | Semester | Turn |
|---|---|---|---|---|
| (PAUL) Classroom practices | 711 | English | first semester | afternoon |
| (TE) Theory | 71 | English | first semester | afternoon |