42033 - Computational Logics for Artificial Intelligence (LCIA) [UPC]

The use of mathematical logic as formalism for Artificial Intelligence has been recognized since the beggining of AI (John McCarthy, 1959) and materialized in different ways:
- as a foundation for knowledge representation and reasoning
- as a tool for analyzing and comparing AI systems
- as programming language for AI applications

The general goal of this course is the study of computational logics useful as formal framework for AI systems.

The specific goals arise from the need of reasoning about concepts that are central in various AI systems, particularly Multi-Agent Systems, which include ontologies, change, action, time, beliefs and norms and committments.

To address these representational and reasoning requirements several logical systems have been put forward which are the object of study in the following table of contents.



Classical Logic:
- Propositional Logic, Resolution and SAT solvers.
- First-Order Logic: Syntax, Model Theory and Proof theory (Resolution, Tableaux).
- Many-sorted Logic.
Logic Programming:
- Classic Logic Programming.
- Negation.
- Disjuntive Logic Programming.
- Answer-Set Programming
Description Logics
- Structure Descriptions.
- Inheritance.
- Description Logic Systems.
Non-monotonic logics
- Close-World assumption.
- Circumscription.
- Default Logics.
- Auto-epistemic logics.
Modal Logic
- Sintax, Semantics and Properties.
- Proof theory: Tableaux..
Temporal Logics
- CTL
- Model checking
Auto-Epistemic Logics for MAS.