Symbolic Reasoning

Code:

M.IA033

Acronym:

RS

Keywords
Classification	Keyword
OFICIAL	Informatics Engineering
OFICIAL	Computer Science

Instance: 2024/2025 - 1S

Active?	No
Responsible unit:	Department of Computer Science
Course/CS Responsible:	Master in Artificial Intelligence

Cycles of Study/Courses

Acronym	No. of Students	Study Plan	Curricular Years	Credits UCN	Credits ECTS	Contact hours	Total Time
M.IA	0	Syllabus	1	-	6	42	162
			2

Teaching language

Suitable for English-speaking students

Objectives

The aim is to give basic knowledge of several areas of symbolic AI and in particular of automated reasoning, knowledge representation, search and planning.
Obtaining insight how various problems can be transformed to formulas, and can be solved automatically by computer programs manipulating these formulas.
The UC will be organised into modules which will address important complementary topics of a theoretical, research, empirical experimentation or development and application nature.

Learning outcomes and competences

As a result of this UC, students should be able to:
O1. Understand the fundamentals of computational logic, as a basis for symbolic reasoning in AI.
O2. Understand the fundamentals and main programming practices in the logic programming paradigm.
O3. Understand the fundamentals and main algorithms for applying symbolic reasoning concepts in AI.
O4. Understand the fundamentals and practices of programming in various extensions within the logic programming paradigm.

Working method

Presencial

Pre-requirements (prior knowledge) and co-requirements (common knowledge)

Conceitos básicos de Lógica Computacional e Programação em Lógica.

Program

1. Algorithms for establishing satisfiability (SAT):
- Propositional logic.
- SAT solvers; Davis–Putnam–Logemann–Loveland (DPLL) framework based on conflict driven clause learning. - Decision heuristics.
- Solvers for first-order logic decidable theories.
- DPLL algorithm for arbitrary theories.
- Satisfiability Modulo Theories library (SMT-LIB) and the Z3 Theorem Prover.
2. Logic programming:
- Selective Linear Definite clause resolution.
- Minimal models of definite logic programs.
- Negation-by-failure; stratified and locally stratified logic programs.
- Prolog with applications to Knowledge Representation and Natural Language Processing.
3. Applications:
- Methods for Searching Solutions (time and space complexity).
- Uninformed and Informed Search Strategies.
- Adversarial Search.
- Heuristic Functions.

Mandatory literature

Stuart Jonathan Russell; Artificial intelligence. ISBN: 978-1-292-40113-3
Armin Biere; Handbook of satisfiability. ISBN: 978-1-58603-929-5
Daniel Kroening; Decision procedures. ISBN: 978-3-662-50497-0
C. J. Hogger; Essentials of logic programming. ISBN: 0-19-853832-4

Complementary Bibliography

Jean Goubault-Larrecq; Proof theory and automated deduction. ISBN: 978-0-7923-4593-0

Teaching methods and learning activities

Partially expository classes with the presentation of concepts, algorithms and application examples. The remaining classes will be used for proposed practical exercises and for monitoring the development of projects throughout the UC. Projects will be completed outside of class. There will be an individual final exam. One or more individual tests may be performed throughout the semester.

Software

Python
Prolog
Z3 solver
SAT solvers

Evaluation Type

Distributed evaluation with final exam

Assessment Components

designation	Weight (%)
Participação presencial	10,00
Exame	50,00
Trabalho laboratorial	40,00
Total:	100,00

Amount of time allocated to each course unit

designation	Time (hours)
Elaboração de projeto	40,00
Estudo autónomo	80,00
Frequência das aulas	42,00
Total:	162,00

Eligibility for exams

Enrolled students qualify for the final exam if they attend at least 3/4 of the classes

Calculation formula of final grade

Evaluation formula:
Final Grade =
10% * Participation in Classes + 40% * Practical projects +
50% * Individual tests and final exam

The minimal grade of the final exam/Tests is 6 over 20.

Examinations or Special Assignments

Internship work/project

Special assessment (TE, DA, ...)

Classification improvement

Observations